1673068212

10.2.2 Semantyka Małych Kroków

(c,ir)-.(c',ir')

A co jak program się zakończy?

(c, 7r) -*■ n'

Rozważmy poprzedni język programowania i zadajmy mu reguły wnioskowania dla semantyki małych kroków:

(skip,7r) -»7r’

(a,7r) -> n

(X := a, 7r) -*■    /n] ’

(o,ir) - (a',ir)'

Zdefiniujmy

(a, 7r) -> n’

(a, 7r) -» n (a, 7r) -*• n

(a,ir)->(n^,,ir)    (a',ir) - n

(o,7r) -> n

Wyrażenia arytmetyczne:

' (X,n)^n(X)'

(n, 7r) -*■ n’

• -:-,n = m©n₂,

(ni ® n₂,7r/ -*• n

(ai,7r) -*■ (ai7r)

(ai ® a2,7r) -> (a'j ®a2,7r)’

(^Q2i tt) (n'₂,TT)

(ni ®a2,7r) -*■ (ni ®a'₂,7r)’

A jak to będzie ze złożeniem instrukcji?

(ci,7r) -> (c'i,7r')

(ci;C2,7T> -► (ej; 02,71-')’

(ci,7r) -* 7r'

(ci;C₂,7T> -► (C2,7T')’

16