Rachunek programów: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 2: Linia 2:
 
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. <br />
 
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. <br />
 
Logikę algorytmiczną utożsamiać będziemy z rachunkiem programów.<br />
 
Logikę algorytmiczną utożsamiać będziemy z rachunkiem programów.<br />
<math>\qquad  \mbox{Rachunek zdań} \subset  \left [\begin{array} \mathrm{Rachunek\ predykatów} \\czyli \\ \mathrm{Logika\ pierwszego\ rzędu}\end{array}\right ]  \subset \left [\begin{array}\mathrm{Rachunek\ programów}\\czyli \\ \mbox{Logika algorytmiczna} \end{array}\right ] </math><br />
+
<math>\qquad  \mbox{Rachunek zdań} \subset  \left [\begin{array}{l} \mathrm{Rachunek\ predykatów} \\czyli \\ \mathrm{Logika\ pierwszego\ rzędu}\end{array}\right ]  \subset \left [\begin{array}{l}\mathrm{Rachunek\ programów}\\czyli \\ \mbox{Logika algorytmiczna} \end{array}\right ] </math><br />
  
 
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 />
 
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 20:30, 27 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]\qquad \mbox{Rachunek zdań} \subset \left [\begin{array}{l} \mathrm{Rachunek\ predykatów} \\czyli \\ \mathrm{Logika\ pierwszego\ rzędu}\end{array}\right ] \subset \left [\begin{array}{l}\mathrm{Rachunek\ programów}\\czyli \\ \mbox{Logika algorytmiczna} \end{array}\right ] [/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).