Examples of program specs {x=1} X:=X+1 {x=2} valid {x=1) X:=X+1 {X=3} invalid {x-y>3} X :=X-y {x>2} valid [x-y>3] X :=X-y [x>2] valid {x≤10 while x#10 do x:=x+1 x =10) valid [x≤10] while x#10 do x:=x+1 [x 10] valid (true) while x#10 do x:=x+1(x 10) valid [true] while x+10 do x:=x+1 [x 10] invalid 16/197
Examples of program specs {x = 1} x := x + 1 {x = 2} valid {x = 1} x := x + 1 {x = 3} invalid {x − y > 3} x := x − y {x > 2} valid [x − y > 3] x := x − y [x > 2] valid {x ≤ 10} while x , 10 do x := x + 1 {x = 10} valid [x ≤ 10] while x , 10 do x := x + 1 [x = 10] valid {true} while x , 10 do x := x + 1 {x = 10} valid [true] while x , 10 do x := x + 1 [x = 10] invalid {x = 1} while true do skip {x = 2} valid 16 / 197
Examples of program specs {x=1 X=X+1 {x=21 valid {x=1} X=X+1 {X=3} invalid {x-y>3} X :=X-y {x>2} valid [x-y>3] X :=X-y [x>2] valid {x≤10 while x≠10dox:=x+1 {x=10} valid [x≤10]while x≠10dox:=x+1 [x=10] valid (true) while x#10 do x:=x+1x =10) valid [true]while x+10 do x :=x+1 [x=10] invalid {x=1 while true do skip {x=21 valid 17/197
Examples of program specs {x = 1} x := x + 1 {x = 2} valid {x = 1} x := x + 1 {x = 3} invalid {x − y > 3} x := x − y {x > 2} valid [x − y > 3] x := x − y [x > 2] valid {x ≤ 10} while x , 10 do x := x + 1 {x = 10} valid [x ≤ 10] while x , 10 do x := x + 1 [x = 10] valid {true} while x , 10 do x := x + 1 {x = 10} valid [true] while x , 10 do x := x + 1 [x = 10] invalid {x = 1} while true do skip {x = 2} valid 17 / 197
Total correctness Informally:Total correctness Termination Partial correctness Total correctness is the ultimate goal it is usually easier to show partial correctness and termination separately Termination is usually straightforward to show,but there are examples where it is not:no one knows whether the program below terminates for all values of x while x>1 do if odd(x)then x :=(3*x)+1 else x:=x/2 18/197
Total correctness Informally: Total correctness = Termination + Partial correctness Total correctness is the ultimate goal I it is usually easier to show partial correctness and termination separately Termination is usually straightforward to show, but there are examples where it is not: no one knows whether the program below terminates for all values of x while x > 1 do if odd(x) then x := (3 ∗ x) + 1 else x := x/2 18 / 197
Logical variables ([x xoAy=yolr:=x;x:=y;y :=r[x=yoAy=xol This says that if the execution of r:=x;x:=y;y:=r terminates (which it does),then the values of x and y are exchanged. The variables xo and yo are used to name the initial values of program variables x and y. Used in assertions only.Not occur in the program. Have constant values. They are called logical variables.(Sometimes it is also called ghost variables.) 19/197
Logical variables {x = x0 ∧ y = y0} r := x ; x := y ; y := r {x = y0 ∧ y = x0} This says that if the execution of r := x ; x := y ; y := r terminates (which it does), then the values of x and y are exchanged. The variables x0 and y0 are used to name the initial values of program variables x and y. I Used in assertions only. Not occur in the program. I Have constant values. They are called logical variables. (Sometimes it is also called ghost variables.) 19 / 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 20/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 20 / 197