1673068224

automatu. Znaczenie programu opisuje się podając, jakie operacje wykona maszyna realizująca program, stąd nazwa tego rodzaju semantyki. We współczesnej formie formalizm ten został rozwinięty przez Gordona Plotkina w latach 70-tych zeszłego wieku w postaci tzw. strukturalnej semantyki operacyjnej.

• Semantyka aksjomatyczna.

Definiuje się specjalny formalizm logiczny do wyrażania własności programów i system wnioskowania do dowodzenia tych własności. Język jest wówczas opisany przez zbiór odpowiednich aksjomatów i reguł wnioskowania, stąd nazwa tego rodzaju semantyki. Stworzyli ją w latach 60-tych zeszłego wieku R. W. Floyd i C. A. R. Hoare. Semantyka aksjomatyczna bywa też nazywana logiką Floyda-Hoare 'a.

8 Wykład 01.04.2008

8.1 Przypomnienie

Ostatnio sobie rozmawialiśmy o logice. To jeszcze parę słów przypomnienia. Zaczęliśmy opisania sobie rachunku predykatów formuł pierwszego rzędu.

Mamy jakby 2 kategorie gramatyczne. Termy budujemy tak:

t f(t\, ...,t_n), n > 0 |x - to jest algebra termów.

Na term patrzymy jak na drzewo.

Jak chcemy zobaczyć „co jest w języku” to patrzymy na jego składnię abstrakcyjną.

Mamy tu zasadę indukcyjną.

p ::= R(ti,...t_n) | -><p | tpi ® I | 3x<P © ::= v | A | => | <=>

ip,r/,f)Jl r]ł=^mip

t=^OT ip wtw. gdy dla każdego możliwego r/ zachodzi r/1=®¹ ip

W rachunku zdań „światy” to są możliwe wartościowania zmiennych.

Chcemy poznawać takie prawdy, które obowiązują w każdym możliwym rozważanym świecie (tautologia).

Tautologia - formula prawdziwa.

t= p wtw. gdy t=^OT <p dla każdego 971.

To była teoria modeli. A teraz możemy zostać w samym języku. Centralnym punktem naszego zainteresowania jest język. Chcemy mieć automatyczne narzędzia weryfikacji co jest prawdziwe, a co nie.

9