equal
deleted
inserted
replaced
18 translations "|- {P}c{Q}" == "(P,c,Q) : hoare" |
18 translations "|- {P}c{Q}" == "(P,c,Q) : hoare" |
19 |
19 |
20 inductive hoare |
20 inductive hoare |
21 intrs |
21 intrs |
22 skip "|- {P}SKIP{P}" |
22 skip "|- {P}SKIP{P}" |
23 ass "|- {%s.P(s[a s/x])} x:=a {P}" |
23 ass "|- {%s. P(s[a s/x])} x:=a {P}" |
24 semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}" |
24 semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}" |
25 If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==> |
25 If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==> |
26 |- {P} IF b THEN c ELSE d {Q}" |
26 |- {P} IF b THEN c ELSE d {Q}" |
27 While "|- {%s. P s & b s} c {P} ==> |
27 While "|- {%s. P s & b s} c {P} ==> |
28 |- {P} WHILE b DO c {%s. P s & ~b s}" |
28 |- {P} WHILE b DO c {%s. P s & ~b s}" |