1673068210

10.2 Semantyka operacyjna

Język który w całości opisano semantyką operacyjną to SML.

Definicja. S.O.S. - Strukturalna Semantyka Operacyjna (Gordon Plotkin, ok. 1970)

„Sądy”, które będziemy wypowiadać będą troszkę „skażone” naszym meta-językiem (nie będą one do końca formalne).

10.2.1 Semantyka Dużych Kroków

1.    (a, 7r) -»■ n (7r: X -*■ Z, n 6 II, n € N),

2.    {b,v)-*T,FeB,

3.    (c, 7T) -» 7r' € II,

Definicja. Dowód to ciąg wypowiedzi w języku, o takiej własności, że każda wypowiedź jest aksjomatem, albo konkluzją z poprzednich aksjomatów (i konkluzji) na podstawie reguł wnioskowania. Informatycy lubią patrzeć na dowód jak na drzewo w którego liściach są aksjomaty, a jego wierzchołkach - reguły. W korzeniu jest formuła ip, która jest tezą tego dowodu.

Chcemy mieć narzędzie, którym udowonimy, że jeśli jakiś program c jest uruchomiony w pamięci n to da jakąś pamięć ir' ((c,n) -* ir').

Taki system (narzędzie) będzie zdefiniowany indukcyjnie (to będzie indukcja strukturalna -system sterowany składnią).

Rozważmy sobie język:

a ::= n | X \ a ® a © ::= + | - | x | div | mod b ::= fli © 02 | -■& | 6i @ &2 © ::= A | V | => | <=>

© "=< | > | ś | > | = | *

c ::= skip | abort | X ■■= a \ if b then c\ else C2 | if b then c | while b do c \ C\; C2

14