More simple examples (x=Xo Ay=yo]x :=y;y:=x[x=yoAy=xo This says that x:=y;y:=x exchanges the values of x and y This is not valid [true)c(q) This says that whenever c terminates,then g holds 21/197
More simple examples I {x = x0 ∧ y = y0} x := y ; y := x {x = y0 ∧ y = x0} I This says that x := y ; y := x exchanges the values of x and y I This is not valid I {true}c{q} I This says that whenever c terminates, then q holds I [true]c[q] I This says that c always terminates and ends in a state where q holds I {p}c{true} I This is valid for every condition p and every command c I [p]c[true] I This says that c terminates if initially p holds I It says nothing about the final state 21 / 197
More simple examples x Xo Ay yo]x :=y;y:=x[x=yoAy=Xo This says that x:=y;y:=x exchanges the values of x and y This is not valid (true)c(q) This says that whenever c terminates,then q holds true c[q] This says that c always terminates and ends in a state where q holds 22/197
More simple examples I {x = x0 ∧ y = y0} x := y ; y := x {x = y0 ∧ y = x0} I This says that x := y ; y := x exchanges the values of x and y I This is not valid I {true}c{q} I This says that whenever c terminates, then q holds I [true]c[q] I This says that c always terminates and ends in a state where q holds I {p}c{true} I This is valid for every condition p and every command c I [p]c[true] I This says that c terminates if initially p holds I It says nothing about the final state 22 / 197
More simple examples (x=Xo Ay=yo]x :=y;y:=x[x=yoAy=xo This says that x:=y;y:=x exchanges the values of x and y This is not valid [true)c(q) This says that whenever c terminates,then g holds [true]c[q] This says that c always terminates and ends in a state where q holds [p)cltrue) This is valid for every condition p and every command c 23/197
More simple examples I {x = x0 ∧ y = y0} x := y ; y := x {x = y0 ∧ y = x0} I This says that x := y ; y := x exchanges the values of x and y I This is not valid I {true}c{q} I This says that whenever c terminates, then q holds I [true]c[q] I This says that c always terminates and ends in a state where q holds I {p}c{true} I This is valid for every condition p and every command c I [p]c[true] I This says that c terminates if initially p holds I It says nothing about the final state 23 / 197
More simple examples x Xo Ay yo]x :=y;y:=x[x=yoAy=Xo This says that x:=y;y:=x exchanges the values of x and y This is not valid (true)c(q) This says that whenever c terminates,then q holds true]c[q] This says that c always terminates and ends in a state where q holds [p)c(true) This is valid for every condition p and every command c [p]c[true] This says that c terminates if initially p holds It says nothing about the final state 24/197
More simple examples I {x = x0 ∧ y = y0} x := y ; y := x {x = y0 ∧ y = x0} I This says that x := y ; y := x exchanges the values of x and y I This is not valid I {true}c{q} I This says that whenever c terminates, then q holds I [true]c[q] I This says that c always terminates and ends in a state where q holds I {p}c{true} I This is valid for every condition p and every command c I [p]c[true] I This says that c terminates if initially p holds I It says nothing about the final state 24 / 197
Specification can be tricky "The program must set y to the maximum of x and y" 25/197
Specification can be tricky “The program must set y to the maximum of x and y” [true]c[y = max(x, y)] I A suitable program: I if x ≥ y then y := x else skip I Another? I if x ≥ y then x := y else skip I Or even? I y := x Later you will be able to prove that these programs are all “correct”... The postcondition y = max(x, y) says “y is the maximum of x and y in the final state” 25 / 197