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