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/197Hoare’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