Specifications of imperative programs Acceptable Acceptable Initial State Final State “Xis “Y is the greater than square root Zero” Action ofX” of the Program 6/197
Specifications of imperative programs 6 / 197
Hoare's notation(Hoare triples) For a program c, partial correctness specification: (p)ciq) total correctness specification: [p]c[q] Here p and g are assertions,i.e.,conditions on the program variables used in c. p is called precondition,and q is called postcondition Hoare's original notation was plc)q not (p)c(q),but the latter form is now more widely used 7/197
Hoare’s notation (Hoare triples) For a program c, I partial correctness specification: {p}c{q} I total correctness specification: [p]c[q] Here p and q are assertions, i.e., conditions on the program variables used in c. I p is called precondition, and q is called postcondition Hoare’s original notation was p{c}q not {p}c{q}, but the latter form is now more widely used 7 / 197
Meanings of Hoare triples A partial correctness specification (p)c(g)is valid,iff if c is executed in a state initially satisfying p and if the execution of c terminates then the final state satisfies g It is "partial"because for (p)clg)to be true it is not necessary for the execution of c to terminate when started in a state satisfying p It is only required that if the execution terminates,then g holds 8/197
Meanings of Hoare triples A partial correctness specification {p}c{q} is valid, iff I if c is executed in a state initially satisfying p I and if the execution of c terminates I then the final state satisfies q It is “partial” because for {p}c{q} to be true it is not necessary for the execution of c to terminate when started in a state satisfying p It is only required that if the execution terminates, then q holds 8 / 197
Meanings of Hoare triples A partial correctness specification (p)clg)is valid,iff if c is executed in a state initially satisfying p and if the execution of c terminates then the final state satisfies q A total correctness specification [p]c[q]is valid,iff if c is executed in a state initially satisfying p then the execution of c terminates and the final state satisfies g Informally:Total correctness=Termination Partial correctness 9/197
Meanings of Hoare triples A partial correctness specification {p}c{q} is valid, iff I if c is executed in a state initially satisfying p I and if the execution of c terminates I then the final state satisfies q A total correctness specification [p]c[q] is valid, iff I if c is executed in a state initially satisfying p I then the execution of c terminates I and the final state satisfies q Informally: Total correctness = Termination + Partial correctness 9 / 197
Examples of program specs {x=1} X:=X+1 {x=2} valid {x=1 X:=X+1 {x=3} invalid 10/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 10 / 197