Logika algorytmiczna

Z Wikipedii

Ten artykuł wymaga dodania linków wewnętrznych. Jeśli możesz, dodaj je teraz. Linki do innych haseł: hasło, hasłowy, hasłami zapisujemy jako [[hasło]], ''[[hasło]]wy'', '''[[hasło|hasłami]]'''.

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.

[edytuj] Bibliografia

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