Is the following Hoare triple
(1) Yes
(2) No

*valid*— i.e., the claimed relation between P, c, and Q is true?
{{True}} X ::= 5 {{X = 5}}

Is the following Hoare triple *valid* — i.e., the
claimed relation between P, c, and Q is true?
(1) Yes
(2) No

{{True}} X ::= 5 {{X = 5}}

What about this one?
(1) Yes
(2) No

{{X = 2}} X ::= X + 1 {{X = 3}}

What about this one?
(1) Yes
(2) No

{{True}} X ::= 5; Y ::= 0 {{X = 5}}

What about this one?
(1) Yes
(2) No

{{X = 2 ∧ X = 3}} X ::= 5 {{X = 0}}

What about this one?
(1) Yes
(2) No

{{True}} SKIP {{False}}

What about this one?
(1) Yes
(2) No

{{False}} SKIP {{True}}

What about this one?
(1) Yes
(2) No

{{True}} WHILE True DO SKIP END {{False}}

What about this one?
(1) Yes
(2) No

{{X = 0}}

WHILE X == 0 DO X ::= X + 1 END

{{X = 1}}

WHILE X == 0 DO X ::= X + 1 END

{{X = 1}}

What about this one?
(1) Yes
(2) No

{{X = 1}}

WHILE X ≠ 0 DO X ::= X + 1 END

{{X = 100}}

WHILE X ≠ 0 DO X ::= X + 1 END

{{X = 100}}

- introduce one "proof rule" for each Imp syntactic form
- plus a couple of a "structural rule" that helps glue proofs together
- prove programs correct using these proof rules, without ever unfolding the definition of hoare

{{ Y = 1 }} X ::= Y {{ X = 1 }}

In English: if we start out in a state where the value of Y
is 1 and we assign Y to X, then we'll finish in a
state where X is 1. That is, the property of being equal
to 1 gets transferred from Y to X.
{{ Y + Z = 1 }} X ::= Y + Z {{ X = 1 }}

the same property (being equal to one) gets transferred to
X from the expression Y + Z on the right-hand side of
the assignment.
{{ a = 1 }} X ::= a {{ X = 1 }}

is a valid Hoare triple.
{{ Q [X ↦ a] }} X ::= a {{ Q }}

where "Q [X ↦ a]" is pronounced "Q where a is substituted
for X".
{{ (X ≤ 5) [X ↦ X + 1]

i.e., X + 1 ≤ 5 }}

X ::= X + 1

{{ X ≤ 5 }}

{{ (X = 3) [X ↦ 3]

i.e., 3 = 3}}

X ::= 3

{{ X = 3 }}

{{ (0 ≤ X ∧ X ≤ 5) [X ↦ 3]

i.e., (0 ≤ 3 ∧ 3 ≤ 5)}}

X ::= 3

{{ 0 ≤ X ∧ X ≤ 5 }}

Now we can give the precise proof rule for assignment:
i.e., X + 1 ≤ 5 }}

X ::= X + 1

{{ X ≤ 5 }}

{{ (X = 3) [X ↦ 3]

i.e., 3 = 3}}

X ::= 3

{{ X = 3 }}

{{ (0 ≤ X ∧ X ≤ 5) [X ↦ 3]

i.e., (0 ≤ 3 ∧ 3 ≤ 5)}}

X ::= 3

{{ 0 ≤ X ∧ X ≤ 5 }}

(hoare_assign) | |

{{Q [X ↦ a]}} X ::= a {{Q}} |

{{(X = 3) [X ↦ 3]}} X ::= 3 {{X = 3}},

follows directly from the assignment rule,
{{True}} X ::= 3 {{X = 3}}.

does not. This triple is valid, but it is not an instance of
hoare_assign because True and (X = 3) [X ↦ 3] are not
syntactically equal assertions. However, they are logically
equivalent, so if one triple is valid, then the other must
certainly be as well. We might capture this observation with the
following rule:
{{P'}} c {{Q}} | |

P ⇿ P' | (hoare_consequence_pre_equiv) |

{{P}} c {{Q}} |

{{P'}} c {{Q}} | |

P ⇾ P' | (hoare_consequence_pre) |

{{P}} c {{Q}} |

{{P}} c {{Q'}} | |

Q' ⇾ Q | (hoare_consequence_post) |

{{P}} c {{Q}} |

For example, we might use the first consequence rule like this:

{{ True }} ⇾

{{ 1 = 1 }}

X ::= 1

{{ X = 1 }}

{{ 1 = 1 }}

X ::= 1

{{ X = 1 }}

Finally, for convenience in some proofs, we can state a "combined"
rule of consequence that allows us to vary both the precondition
and the postcondition.

{{P'}} c {{Q'}} | |

P ⇾ P' | |

Q' ⇾ Q | (hoare_consequence) |

{{P}} c {{Q}} |

(hoare_skip) | |

{{ P }} SKIP {{ P }} |

{{ P }} c1 {{ Q }} | |

{{ Q }} c2 {{ R }} | (hoare_seq) |

{{ P }} c1;;c2 {{ R }} |

Theorem hoare_seq : ∀P Q R c1 c2,

{{Q}} c2 {{R}} →

{{P}} c1 {{Q}} →

{{P}} c1;;c2 {{R}}.

Informally, a nice way of recording a proof using the sequencing
rule is as a "decorated program" where the intermediate assertion
Q is written between c1 and c2:

{{ a = n }}

X ::= a;;

{{ X = n }} <---- decoration for Q

SKIP

{{ X = n }}

X ::= a;;

{{ X = n }} <---- decoration for Q

SKIP

{{ X = n }}

{{P}} c1 {{Q}} | |

{{P}} c2 {{Q}} | |

{{P}} IFB b THEN c1 ELSE c2 {{Q}} |

{{ True }}

IFB X == 0

THEN Y ::= 2

ELSE Y ::= X + 1

FI

{{ X ≤ Y }}

since the rule tells us nothing about the state in which the
assignments take place in the "then" and "else" branches.
IFB X == 0

THEN Y ::= 2

ELSE Y ::= X + 1

FI

{{ X ≤ Y }}

{{P ∧ b}} c1 {{Q}} | |

{{P ∧ ~b}} c2 {{Q}} | (hoare_if) |

{{P}} IFB b THEN c1 ELSE c2 FI {{Q}} |

- This hides the low-level details of the semantics of the program
- Leads to a compositional reasoning process

{{P}} c {{Q}}

- P and Q are predicates about the state of the Imp program
- "If command c is started in a state satisfying assertion P, and if c eventually terminates in some final state, then this final state will satisfy the assertion Q."

(hoare_assign) | |

{{Q [X ↦ a]}} X::=a {{Q}} |

(hoare_skip) | |

{{ P }} SKIP {{ P }} |

{{ P }} c1 {{ Q }} | |

{{ Q }} c2 {{ R }} | (hoare_seq) |

{{ P }} c1;;c2 {{ R }} |

{{P ∧ b}} c1 {{Q}} | |

{{P ∧ ~b}} c2 {{Q}} | (hoare_if) |

{{P}} IFB b THEN c1 ELSE c2 FI {{Q}} |

{{P'}} c {{Q'}} | |

P ⇾ P' | |

Q' ⇾ Q | (hoare_consequence) |

{{P}} c {{Q}} |

{{fun st ⇒ True}}

IFB (BEq (AVar X) (AInt 0))

THEN (Y ::= (AInt 2))

ELSE (Y ::= APlus (AVar X) (AInt 1))

FI

{{fun st ⇒ st X ≤ st Y}}.

WHILE b DO c END

and we want to find a pre-condition P and a post-condition
Q such that
{{P}} WHILE b DO c END {{Q}}

is a valid triple.
{{P}} WHILE b DO c END {{P}}.

{{P}} WHILE b DO c END {{P ∧ ¬b}}

{{P}} c {{P}} | |

{{P}} WHILE b DO c END {{P ∧ ~b}} |

{{P ∧ b}} c {{P}} | (hoare_while) |

{{P}} WHILE b DO c END {{P ∧ ~b}} |

WHILE X = 2 DO X := 1 END

although it is clearly
Is the assertion
(1) Yes
(2) No

X = 0

an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END

Is the assertion
(1) Yes
(2) No

Y = 0

an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END

Is the assertion
(1) Yes
(2) No

X > 0

an invariant of the following loop?
WHILE X = 0 DO X ::= X+1 END

Is the assertion
(1) Yes
(2) No

X < 100

an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END

Is the assertion
(1) Yes
(2) No

X > 10

an invariant of the following loop?
WHILE X>10 DO X ::= X+1 END

Is the assertion
(2) No

X = Y + Z

an invariant of the following loop?
WHILE Y>10 DO Y := Y-1; Z ::= Z+1 END

(1) Yes
∀P Q,

{{P}} WHILE BTrue DO SKIP END {{Q}}.

(hoare_assign) | |

{{Q [X ↦ a]}} X::=a {{Q}} |

(hoare_skip) | |

{{ P }} SKIP {{ P }} |

{{ P }} c1 {{ Q }} | |

{{ Q }} c2 {{ R }} | (hoare_seq) |

{{ P }} c1;;c2 {{ R }} |

{{P ∧ b}} c1 {{Q}} | |

{{P ∧ ~b}} c2 {{Q}} | (hoare_if) |

{{P}} IFB b THEN c1 ELSE c2 FI {{Q}} |

{{P ∧ b}} c {{P}} | (hoare_while) |

{{P}} WHILE b DO c END {{P ∧ ~b}} |

{{P'}} c {{Q'}} | |

P ⇾ P' | |

Q' ⇾ Q | (hoare_consequence) |

{{P}} c {{Q}} |