1673068211

I mamy kilka przykładowych jego reguł wnioskowania:

(n, 7r) -*■ n’

(ai,7r) -> ni (02,77) -

(di © 02,71") -> n

(61,77)->T    (6₂,tt) -

(6^62,77)^7    ’

(6l,7T)^r    (62, 7r) -» F

(61 v 62,77) -»■ T

(61,77) ->F    (62,77) -» r

(61 v 62,77) -*■ r

(61,77) -*■ F (62,77)-»F

(b\ v 62,tt) -* F

A jakby to wyglądało w C (albo Haskellu) - chodzi o kolejność wykonywania tych działań: (bi,n)-*T

-, xe{T,F},

(61 v 62,77) -*■ T'

(61,77) -» F (62,77)-

(61 v 62,77) -

Zmierzamy do opisania semantyki operacyjnej dla instrukcji:

(skip, 77) -*■ 77 ’

• —----— --, abort definiujemy przez brak jego definicji!,

(abort, 77) -* wybuchnij!

(a, 77) -*■ n

(X := a, 77) -*■ 77[A/n] ’

(ci,77) -> 77^;    (02, 7r') -» Tt"

(Ci;C2,77) -*•77"

(6,77) ^F (if 6 then 0,77) -* 77’

(6.77)    -* T (c, 77) -*■ 77^r (if 6 then c, 77) -* 77' ’

(6.77)    -*• T (c, 77) -*■ 77' (while 6 do c, 77') -*■ 77"

(while 6 do c, 77) -*■ 77"

(6,77) -»• F

(while 6 do c, 77) -> 77 ’

15