1673068214

•    h {ip} C {ip}, gdzie C to program, lewy nawias wąsaty oznacza, że coś zachodzi przed wykonaniem programu, a prawy nawias wąsaty oznacza, że coś zachodzi po wykonaniu programu,

•    termy to będą: t ::= n \ X \ /(ti,...,i₂), f e £ = {+,-, x,!,...},

•    formuły to: ip ■■= R(t\,...,t_n) \ ip v rp \ ->ip \ '/rap | 3mp,

•    jak u Tarskiego robimy sobie prawdziwy model (ale z pamięcią): 9Jt = (Z, -^OT) oraz rr,r)\=^m p,

•    ważne! Chcemy mieć tak:

wtedy dla każdej tt e II (pamięci), dla każdego 77 (wartościowania): jeśli 7T, rj \= p i 7r e Dom\C\, to [C]7r, 77 n rp

Ten system wnioskowania będzie troszkę „hybrydowy” - oprócz 1- {<p} C {rp} będziemy mieli jeszcze (chcemy móc zapytać, czy 2 + 2 = 4):

1= <p wtw 7T, 771= p dla każdej n e n i każdego 77

M skip {ip} ’

{1p] abort {rj;}'

W[X/e]} X :=e {ip}'

{jp}ci{rp} {rp} C2 {q}

Mci;c₂{p}

{bA<p}c\{rp} {-bf\ip} c₂ {rp}

{ip} if b then c\ else c₂ {rp}

{<pAb}c{rp} \=ipA^b=>rp {ip} if b then c {rp}

{b a ip} c {ip}

• -— -----, gdzie <7? jest niezmiennikiem pętli.

{ip} while b do c {ip a —.0}

•    reguły osłabiania¹:

_o M c M t=rp=> q M ^c {^}

I= W=>rp {rp}c{g}

M c M

18

1

a.k.a. „system pytania siekierki” (lub „wyroczni”) o to, czy jeśli a; = 2 + 2toa: = 4