1.Function definition [亚]id(arg){Body}[亚']，that is[亚]StmtList[亚')，where the StmtList is the StmtList in the Body production. 2.Statement List ·sp(Stmt StmtList,业)=sp(StmtList,sp(Stmt,业) ·sp(e,亚)=亚.If e forms the StmtList of a function,.then VC=亚p亚'(see 1 for亚will be generated.. 3.Statement ·assignment:sp(lval=Exp,亚)=亚'，亚'can be calculated using亚according to the assignment rules in the pointer logic. ·condition:sp(if(Bexp){StmtList}else{StmtList2},平)=sp(StmtList1,BexpAΨ)Vsp(StmtList2,一BexpA平) loop:sp(while(Bexp){StmtList,)=-BexpA I,where Iis the loop invariant for pointer-type data. VC1=I and VC2 sp(StmtList,Bexp A DI should be generated at the entry point and the exit of StmtList respectively. 。allocation:sp(Ival=alloc(Type),亚)=亚'，亚can be calculated using亚according to the allocation rules in the pointer logic. 。deallocation:sp(free(Exp),亚)=亚'，亚'can be calculated using亚according to the deallocation rule in the pointer logic. .function call:If the pre-and postconditions of function id are farg)[lvalA and A Qrespectively,then sp(Ival id(Exp),)=(A Q)[arg-Exp][res-Ivall,where Q and Qarg are assertions that have nothing to do with pointers,arg is the formal parameter,and res is the return value (see Figure 1). VC=(farg}A [Ival)A Qn)[arg-Exp]should be generated at the entry point of this statement. ·return:sp(return res,.亚)=亚 Figure 2.The Strongest postcondition calculus and the VC generation of pointer-type data 2.One difficulty of strongest postcondition calculus is the assignment axiom.Instead,different assignment rules need to find a fixpoint for a recursive equation in a loop are used in different cases in our pointer logic.Since statement.The solutions to such equations are usually the pointer analysis is precise,it is easy to determine undecidable,and it is also the primary reason why the which rule to use in a certain case and it is clear how correctness of a program can not be proved automat- to compute 'using in the sp rule for assignment. ically.The loop invariant provided by programmers Please refer to [2]for some details skipped in Figure 2. is used to avoid the difficulty.However,in order to prove the validity of the loop invariant,two VCs must 5.At the entry point of a function,the pointer logic be generated at the entry point and the exit of the loop should check the initial values of the pointer-type for- respectively. mal parameters and local variables.And at the exit of the function,their effectiveness should also be checked 3.The pre-and postconditions of each function have also to avoid memory leaks.But for the space limit,the VC deeply simplified the computation of sp for function generation in Figure 2 does not reflect this. call statement.Briefly speaking,the before the call statement should imply the precondition of the callee, For integer-type data,we adopt a complemented ap- and the callee's postcondition should be used as the proach of Hoare logic-weakest precondition calculus strongest postcondition after the call statement.Cer- (wp)[5]to generate assertions or VCs at each program tainly,we also need to consider the substitution of ac- point.And we only introduce its distinctions from the ap- tual parameters for formal parameters as well as the proach for pointer-type data as follows. substitution of the variable Ival for the variable res(see function call in Figure 2). 1.Since the assertions in a function are calculated back- ward using the postcondition Q of the function,a VC 4.One remarkable distinction of our pointer logic from Pwp(StmtList,Q)is generated at the entry point of Hoare logic is that the pointer logic has no uniform the function,where P is the precondition of the func-1. Function definition {{Ψ}} id(arg){Body} {{Ψ
}}, that is {{Ψ}} StmtList {{Ψ
}}, where the StmtList is the StmtList in the Body production. 2. Statement List • sp(Stmt StmtList, Ψ) = sp(StmtList, sp(Stmt, Ψ)) • sp(
, Ψ) = Ψ. If
forms the StmtList of a function, then VC = Ψ ⊃ Ψ
(see 1 for Ψ
) will be generated. 3. Statement • assignment: sp(lval = Exp, Ψ) = Ψ
, Ψ
can be calculated using Ψ according to the assignment rules in the pointer logic. • condition: sp(if (Bexp) {StmtList1} else {StmtList2}, Ψ) = sp(StmtList1, Bexp∧Ψ)∨sp(StmtList2, ¬Bexp∧Ψ) • loop: sp(while (Bexp) {StmtList}, Ψ) = ¬Bexp ∧ I, where I is the loop invariant for pointer-type data. VC1 = Ψ ⊃ I and VC2 = sp(StmtList, Bexp ∧ I) ⊃ I should be generated at the entry point and the exit of StmtList respectively. • allocation: sp(lval = alloc(Type), Ψ) = Ψ
, Ψ
can be calculated using Ψ according to the allocation rules in the pointer logic. • deallocation: sp(free(Exp), Ψ) = Ψ
, Ψ
can be calculated using Ψ according to the deallocation rule in the pointer logic. • function call: If the pre- and postconditions of function id are {arg}∧{lval}N ∧Qarg and Ψ
∧Q respectively, then sp(lval = id(Exp), Ψ) = (Ψ
∧ Q)[arg ← Exp][res ← lval], where Q and Qarg are assertions that have nothing to do with pointers, arg is the formal parameter, and res is the return value (see Figure 1). VC = Ψ ⊃ ({arg}∧{lval}N ∧ Qarg)[arg ← Exp] should be generated at the entry point of this statement. • return: sp(return res, Ψ) = Ψ Figure 2. The Strongest postcondition calculus and the VC generation of pointer-type data 2. One difficulty of strongest postcondition calculus is the need to find a fixpoint for a recursive equation in a loop statement. The solutions to such equations are usually undecidable, and it is also the primary reason why the correctness of a program can not be proved automat￾ically. The loop invariant provided by programmers is used to avoid the difficulty. However, in order to prove the validity of the loop invariant, two VCs must be generated at the entry point and the exit of the loop respectively. 3. The pre- and postconditions of each function have also deeply simplified the computation of sp for function call statement. Briefly speaking, the Ψ before the call statement should imply the precondition of the callee, and the callee’s postcondition should be used as the strongest postcondition after the call statement. Cer￾tainly, we also need to consider the substitution of ac￾tual parameters for formal parameters as well as the substitution of the variable lval for the variable res (see function call in Figure 2). 4. One remarkable distinction of our pointer logic from Hoare logic is that the pointer logic has no uniform assignment axiom. Instead, different assignment rules are used in different cases in our pointer logic. Since the pointer analysis is precise, it is easy to determine which rule to use in a certain case and it is clear how to compute Ψ
using Ψ in the sp rule for assignment. Please refer to [2] for some details skipped in Figure 2. 5. At the entry point of a function, the pointer logic should check the initial values of the pointer-type for￾mal parameters and local variables. And at the exit of the function, their effectiveness should also be checked to avoid memory leaks. But for the space limit, the VC generation in Figure 2 does not reflect this. For integer-type data, we adopt a complemented ap￾proach of Hoare logic—weakest precondition calculus (wp) [5] to generate assertions or VCs at each program point. And we only introduce its distinctions from the ap￾proach for pointer-type data as follows. 1. Since the assertions in a function are calculated back￾ward using the postcondition Q of the function, a VC P ⊃ wp(StmtList, Q) is generated at the entry point of the function, where P is the precondition of the func-