Examples of program specs {x=1} X=X+1 {x=21 valid {x=10 X=X+1 {X=3} invalid {x-y>3} x :=x-y {x>2} valid 11/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 11 / 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 12/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 12 / 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≠10dox:=x+1 {x=10} valid 13/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 13 / 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≠10dox:=x+1 {x=10} valid [x≤10] while x#10 do x :=x+1 [x =10] valid 14/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 14 / 197
Examples of program specs {x=1 X=X+1 {x=21 valid {x=10 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+1 x =10} valid 15/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 15 / 197