Logika algorytmiczna dla programistów

Logika algorytmiczna dla programistów - Grażyna Mirkowska

Logika algorytmiczna – rachunek logiczny, ale także rachunek programów. Każdy program możemy rozpatrywać jako modalność. Jeśli {\displaystyle K} jest programem, a {\displaystyle \alpha } jest formułą, to wyrażenie postaci {\displaystyle 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 {\displaystyle K\alpha } jest wyznaczone gdy znamy znaczenie (tj. semantykę) programu {\displaystyle K} i znaczenie formuły {\displaystyle \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 {\displaystyle K\alpha } możemy opisać w następujący sposób: dla danego wartościowania zmiennych {\displaystyle v} należy najpierw wyznaczyć wynik {\displaystyle v'} obliczenia programu {\displaystyle K} i z kolei obliczyć wartość formuły {\displaystyle \alpha } dla wartościowania {\displaystyle v'}. W przypadku gdy obliczenie programu {\displaystyle K} dla wartościowania {\displaystyle v} nie daje wyniku, przyjmujemy, że wartością formuły {\displaystyle 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 {\displaystyle P} jest poprawny względem warunku początkowego {\displaystyle \alpha } i warunku końcowego {\displaystyle \beta }. Formuła taka ma postać implikacji {\displaystyle (\alpha \Rightarrow P\,\beta )}.