1673068207

2. Budujemy model 971:

• Typy:

O *-.x->z

O * = Z*

o [cj : ir-.tr o [c] 6 ir" o Je):*-Z

O [61: TT -» B, gdzie B = {T,F}

• Przykładowe funkcje semantyczne:

O |skip]](7r) = 7T

o [X:=el(7r) = 7r[X/[el(7r)]

o [if b then c]](7r) o |while b do cj(7r) =

gdy [6](7r) = F MOO, w p.p.

jeżeli [6J(tt) = F w p.p.

[while 6 do c]([c]7r),

9 Wykład 03.04.2008

9.1 Składnia

Ostatnio zaczęliśmy badać języki imperatywne¹.

•    a - wyrażenia arytmetyczne,

•    b - wyrażenia boolowskie,

•    c - instrukcje,

•    n - stałe całkowitoliczbowe,

•    X - identyfikatory,

a ::= n \ X \ a ® a ® ::= + | - | x | div | mod b ::= ai © 02 | ->b \ b\ © 62 © ::= a | V | =► | 4+

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

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

9.2 Semantyka Denotacyjna

1.    maszyna abstrakcyjna,

Bieżący stan pamięci można opisać jako II: X -* Z, a zbiór stanów pamięci to II = Z*.

2.    Denotacją (znaczeniem) programu jest funkcja zmiany zawartości pamięci [cj : II -*■ II (funkcja z pamięci w pamięć). Mamy tu funkcje częściowe.

11

1

z lekkim obrzydzeniem (w kontekście Haskella)