Rachunek programów: Różnice pomiędzy wersjami
m |
|||
| Linia 3: | Linia 3: | ||
Logikę algorytmiczną utożsamiać będziemy z rachunkiem programów.<br /> | Logikę algorytmiczną utożsamiać będziemy z rachunkiem programów.<br /> | ||
<math>Rachunek\ zda\'{n} \subset Rachunek\ predykat\'{o}w \subset Rachunek program\'{o}w </math> | <math>Rachunek\ zda\'{n} \subset Rachunek\ predykat\'{o}w \subset Rachunek program\'{o}w </math> | ||
| + | Każdy program można traktować jako operator modalności: ''formułę P <math>\alpha</math>, czytamy program P zakończył obliczenie i jego wyniki spełniają formułę <math>\alph</math>. '' Rachunek programów jest splotem dwu algebr: algebry formuł i algebry programów. (zob. G. Mirkowska rozprawa doktorska 1972).<br /> | ||
Wersja z 21:15, 26 paź 2015
Termin rachunek programów wydaje się lepiej pasować do znanych pojęć: rachunek zdań i rachunek predykatów.
Rachunek programów zawiera w sobie oba rachunki i ponadto pozwala dokonywać "rachunków" na programach. Jak to zobaczymy często dowody semantycznych własności programów przybieraja postać rachunków na formułach algorytmicznych.
Logikę algorytmiczną utożsamiać będziemy z rachunkiem programów.
[math]Rachunek\ zda\'{n} \subset Rachunek\ predykat\'{o}w \subset Rachunek program\'{o}w [/math]
Każdy program można traktować jako operator modalności: formułę P [math]\alpha[/math], czytamy program P zakończył obliczenie i jego wyniki spełniają formułę [math]\alph[/math]. Rachunek programów jest splotem dwu algebr: algebry formuł i algebry programów. (zob. G. Mirkowska rozprawa doktorska 1972).
