Specification can be tricky "The program must set y to the maximum of x and y" [true]c[y max(x,y)] 26/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” 26 / 197
Specification can be tricky "The program must set y to the maximum of x and y" true]c[y max(x,y)] A suitable program: if x z y then y:=x else skip 27/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” 27 / 197
Specification can be tricky "The program must set y to the maximum of x and y" true]c[y max(x,y)] A suitable program: if x y then y:=x else skip Another? if x>y then x:=y else skip 28/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” 28 / 197
Specification can be tricky "The program must set y to the maximum of x and y" [true]c[y max(x,y)] A suitable program: if x z y then y:=x else skip Another? if x y then x:=y else skip Or even? y :=X 29/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” 29 / 197
Specification can be tricky "The program must set y to the maximum of x and y" [true]c[y max(x,y)] A suitable program: if x y then y:=x else skip Another? if x y then x:=y else skip Or even? 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" 30/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” 30 / 197