Logika algorytmiczna

Logika algorytmiczna jest rachunkiem logicznym, w którym występują formuły algorytmiczne. W języku logiki algorytmicznej można wyrażać semantyczne własności programów. Aksjomaty i reguły wnioskowania AL pozwalają na dowodzenie prawdziwych (semantycznie) formuł algorytmicznych. Oznacza to, że uzyskujemy możliwość dowodzenia faktów postaci: ten program P jest poprawny względem warunku początkowego α i warunku końcowego β. Formuła taka ma postać implikacji (α→Pβ).

Zastosowania AL:

• w inżynierii oprogramowania możemy zapisywać specyfikacje oprogramowania i dokonywać weryfikacji poprzez dowody,
• w projektowaniu języków programowania można opisać semantykę języka, podając odpowiednie aksjomaty i reguły wnioskowania,
• w opisie abstrakcyjnych struktur danych (co łączy się ze specyfikowaniem klas w językach programowania obiektowego) formuły algorytmiczne pozwalają w pełni scharakteryzować pewne struktury i klasy struktur.

Nieformalnie mówiąc, na (pewną) logikę algorytmiczną składają się jej język, aksjomaty i reguły wnioskowania.

Język określamy, podając jego alfabet i zbiór wyrażeń poprawnie zbudowanych WFF. W zbiorze wyrażeń poprawnie zbudowanych wyróżniamy trzy podzbiory: zbiór termów (albo zbiór wyrażeń nazwowych), zbiór formuł (zbiór wyrażeń logicznych) i zbiór programów (algorytmów).

Nieformalnie, język logiki algorytmicznej jest konwolucją języka logiki pierwszego rzędu i języka programów.

Bibliografia

• G. Mirkowska, A. Salwicki, Logika algorytmiczna dla programistów, WNT, 1994