1.5.SPECIFICATIONS AND THEIR INFERENCE RULES 6 Finally,we give axiom schemata for the predicate.(Regrettably,these are far from complete.) e1一eAe2-÷e1-eAe1=e2Ae=e4 e1一e*e2一→e1卡e2 emp÷红.(x-) (ee)np→(ee)*(ee)*p) 1.5 Specifications and their Inference Rules While assertions describe states,specifications describe commands.In spec- ification logic,specifications are Hoare triples,which come in two flavors: (specification)::= {(assertion)}(command){(assertion)} (partial correctness) I[(assertion)](command)[(assertion)] (total correctness) In both flavors,the initial assertion is called the precondition (or sometimes the precedent),and the final assertion is called the postcondition (or some- times the consequent). The partial correctness specification (p)cq}is true iff,starting in any state in which p holds No execution of c aborts,and When some execution of c terminates in a final state,then q holds in the final state. The total correctness specification [p]c[](which we will use much less often)is true iff,starting in any state in which p holds, No execution of c aborts,and Every execution of c terminates,and When some execution of c terminates in a final state,then g holds in the final state.1.5. SPECIFICATIONS AND THEIR INFERENCE RULES 15 Finally, we give axiom schemata for the predicate 7→. (Regrettably, these are far from complete.) e1 7→ e 0 1 ∧ e2 7→ e 0 2 ⇔ e1 7→ e 0 1 ∧ e1 = e2 ∧ e 0 1 = e 0 2 e1 ,→ e 0 1 ∗ e2 ,→ e 0 2 ⇒ e1 6= e2 emp ⇔ ∀x. ¬(x ,→ −) (e ,→ e 0 ) ∧ p ⇒ (e 7→ e 0 ) ∗ ((e 7→ e 0 ) −∗ p). 1.5 Specifications and their Inference Rules While assertions describe states, specifications describe commands. In spec￾ification logic, specifications are Hoare triples, which come in two flavors: hspecificationi ::= {hassertioni} hcommandi {hassertioni} (partial correctness) | [ hassertioni ] hcommandi [ hassertioni ] (total correctness) In both flavors, the initial assertion is called the precondition (or sometimes the precedent), and the final assertion is called the postcondition (or some￾times the consequent). The partial correctness specification {p} c {q} is true iff, starting in any state in which p holds, • No execution of c aborts, and • When some execution of c terminates in a final state, then q holds in the final state. The total correctness specification [ p ] c [ q ] (which we will use much less often) is true iff, starting in any state in which p holds, • No execution of c aborts, and • Every execution of c terminates, and • When some execution of c terminates in a final state, then q holds in the final state