Spis treści
Logika algorytmiczna
Logika algorytmiczna – rachunek logiczny, ale także rachunek programów. Każdy program możemy rozpatrywać jako modalność. Jeśli jest programem, a jest formułą, to wyrażenie postaci jest formułą algorytmiczną. W ten sposób mamy do czynienia ze splotem dwu algebr: algebry Boole’a i algebry programów. Znaczenie formuły jest wyznaczone gdy znamy znaczenie (tj. semantykę) programu i znaczenie formuły 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 możemy opisać w następujący sposób: dla danego wartościowania zmiennych należy najpierw wyznaczyć wynik obliczenia programu i z kolei obliczyć wartość formuły dla wartościowania W przypadku gdy obliczenie programu dla wartościowania nie daje wyniku, przyjmujemy, że wartością formuły 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 jest poprawny względem warunku początkowego i warunku końcowego Formuła taka ma postać implikacji
Zastosowania AL
[edytuj | edytuj kod]- w inżynierii oprogramowania możemy zapisywać specyfikacje oprogramowania i dokonywać weryfikacji poprzez dowody [Mirkowska i Salwicki 1987 ↓ ],
- 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
[edytuj | edytuj kod]- Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa: PWN, 1987, s. 345.
- Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów cz. 1. Warszawa: WNT, 1992, s. 294.
- Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów cz. 2. Warszawa: WNT, 1992, s. 294.
- Lech Banachowski, Antoni Kreczmar, Grażyna Mirkowska, Helena Rasiowa, Andrzej Salwicki: An introduction to Algorithmic Logic – Metamathematical Investigations of Theory of Programs. T. 2: Banach Center Publications. Warszawa: PWN, 1977, s. 7–99, seria: Banach Center Publications. ISBN 123.
- Helena Rasiowa: Algorithmic Logic – Notes from Seminar in Simon Fraser University. T. 281. Warsaw: 1975, seria: Reports of Institute of Computer Science Polish Academy of Sciences.
- repozytorium logiki algorytmicznej. 2013. [dostęp 2018-10-07].