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/197Meanings 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