Logika Algorytmiczna: Różnice pomiędzy wersjami
Linia 6: | Linia 6: | ||
Rozpatrzmy prosty program | Rozpatrzmy prosty program | ||
q:=n; r:=m; | q:=n; r:=m; | ||
− | '''while''' r < | + | '''while''' r < n '''do''' |
q:=q+1: | q:=q+1: | ||
r:=r-n | r:=r-n | ||
Linia 12: | Linia 12: | ||
Co robi ten program? Czy to jest pytanie dobrze postawione? | Co robi ten program? Czy to jest pytanie dobrze postawione? | ||
Czy obliczenie tego programu jest skończone dla każdych danych n i m? | Czy obliczenie tego programu jest skończone dla każdych danych n i m? | ||
− | + | Czym są te dane? Jakie znaczenie mają operacje - i + oraz stała 1? Jakie znaczenie ma predykat <? | |
Wersja z 17:41, 28 lip 2014
Logika algorytmiczna jest rachunkiem logicznym. Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. Formuły tworzą algebrę z działaniami: konkatenacji, alternatywy, negacji i implikacji oraz z działaniami nieskończonymi tj kwantyfikatorami, ponadto programy są modalnościami. Programy też tworzą algebrę: działaniami tej algebry są iteracja, rozgałęzienie i złożenie programów. Mamy więc do czynienia ze splotem dwu algebr. Możemy go nazwać rachunkiem programów. Zadaniem logiki algorytmicznej jest poszukiwanie praw rachunku programów.
Celem jest zebranie praw i reguł wnioskowania, które umożliwią analizę algorytmów i wydawanie opinii o ich własnościach semantycznych, bez wykonywania obliczeń, na podstawie samego tekstu algorytmu i aksjomatów struktury danych w jakiej dany program ma byc interpretowany.
Przykład Rozpatrzmy prosty program
q:=n; r:=m; while r < n do q:=q+1: r:=r-n od
Co robi ten program? Czy to jest pytanie dobrze postawione? Czy obliczenie tego programu jest skończone dla każdych danych n i m? Czym są te dane? Jakie znaczenie mają operacje - i + oraz stała 1? Jakie znaczenie ma predykat <?
Podręczniki
- Grażyna Mirkowska, Andrzej Salwicki, Algorithmic Logic -- monografia -- większy nacisk położono na badania systemu AL
- Grażyna Mirkowska, Andrzej Salwicki, Logika Algorytmiczna dla programistów cz.1
- Grażyna Mirkowska, Andrzej Salwicki, Logika Algorytmiczna dla programistów cz.2
- Algorithmic Logic for Software Construction and Verification
Program logiki algorytmicznej
Zadaniem logiki algorytmicznej jest dostarczenie narzędzi do analizowania semantycznych własności programów takich jak: własność stopu, poprawność programu, etc. Znaczeniem programu [math]P[/math] jest funkcja ze zbioru [math]W[/math] wartościowań zmiennych w ten sam zbiór. Zazwyczaj funkcję tę określa się przy pomocy pojęcia obliczenia programu.
Bibliografia
- [AlgoLog] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa: PWN, 1987, s. 345.
- [LogProg] Grażyna Mirkowska, Andrzej Salwicki: Logika Algorytmiczna dla Programistów. Warszawa: WNT, 1992, s. 294.
- [AL4software]Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.