P7: Algebraická špecifikácia

Zhrnutie prednášky

Prednáška sa po organizačnom úvode (budúci test bude bez tejto témy, na skúške sa však môže objaviť; otázky sú prakticky orientované) venuje úvodu do algebraickej špecifikácie. Motivuje ju problémom implementácie zásobníka (LIFO, stack). Porovnáva implementáciu poľom a spájaným zoznamom z hľadiska efektivity, alokácie pamäte a réžie ukazovateľov a upozorňuje, že implementácia zvyčajne umožňuje aj operácie, ktoré zásobník nepripúšťa. Skúma, či by zásobník zachytilo UML: diagram tried núti myslieť v štruktúre zoznamu, kým stavový diagram by modeloval vlastnosti. Nakoniec predstavuje matematický a formálny prístup, napríklad jazyk Z, ktorý umožňuje presné vyjadrenie špecifikácie na rozdiel od nejednoznačného prirodzeného jazyka.

• - Zásobník (stack) funguje na princípe LIFO: posledný vložený prvok sa vyberá prvý.
• - Zásobník sa typicky implementuje poľom alebo spájaným zoznamom; pole je rýchlejšie vďaka súvislej pamäti, zoznam vyžaduje alokáciu, uvoľňovanie a ukazovatele.
• - Implementácia je všeobecnejšia než abstraktný zásobník a umožňuje aj operácie, ktoré zásobník nepripúšťa.
• - UML diagram tried vedie k modelovaniu štruktúry spájaného zoznamu, stavový diagram by zachytil skôr vlastnosti zásobníka.
• - Matematika ako všeobecný jazyk umožňuje zásobník opísať abstraktne, napríklad ako postupnosť, bez väzby na implementáciu.
• - Formálne špecifikačné jazyky, napríklad Z, riešia nepresnosť prirodzeného jazyka, no obmedzujú vyjadrovacie možnosti.
• - Test na budúcej prednáške sa tejto témy netýka, na skúške sa však objaviť môže.

Zhrnutie pripravené s pomocou AI z prepisu videa.