Logika algorytmiczna

Logika algorytmiczna – rachunek logiczny, ale także rachunek programów. Każdy program możemy rozpatrywać jako modalność. Jeśli $K$ jest programem, a $\alpha$ jest formułą, to wyrażenie postaci $K\alpha$ jest formułą algorytmiczną. W ten sposób mamy do czynienia ze splotem dwu algebr: algebry Boole’a i algebry programów. Znaczenie formuły $K\alpha$ jest wyznaczone gdy znamy znaczenie (tj. semantykę) programu $K$ i znaczenie formuły $\alpha .$ Przypomnijmy, że znaczeniem formuły (pierwszego rzędu) jest funkcja ze zbioru wartościowań zmiennych w zbiór {true, false} wartości logicznych. Znaczeniem programu jest funkcja (częściowa) ze zbioru wartościowań w ten sam zbiór. Teraz znaczenie formuły $K\alpha$ możemy opisać w następujący sposób: dla danego wartościowania zmiennych $v$ należy najpierw wyznaczyć wynik $v^{\prime }$ obliczenia programu $K$ i z kolei obliczyć wartość formuły $\alpha$ dla wartościowania $v^{\prime }.$ W przypadku gdy obliczenie programu $K$ dla wartościowania $v$ nie daje wyniku, przyjmujemy, że wartością formuły $K\alpha$ jest false.

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 $\alpha$ i warunku końcowego $\beta .$ Formuła taka ma postać implikacji $(\alpha \Rightarrow P\beta ).$

Zastosowania AL

• w inżynierii oprogramowania możemy zapisywać specyfikacje oprogramowania i dokonywać weryfikacji poprzez dowody [[[:Szablon:Odn]]],
• 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.

Język określa się, 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).

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

Bibliografia

• Szablon:Cytuj książkę
• Szablon:Cytuj książkę
• Szablon:Cytuj książkę
• Szablon:Cytuj książkę
• Szablon:Cytuj książkę
• Szablon:Cytuj stronę