tion and StmtList is the statement sequence of the func- 4.Code and assertion generation tion. 2.The side condition in a typing rule should be combined In our framework,specifications and the proof of code satisfying the specifications are carried in the assembly with the assertion which is at the entry point of the code.The assembly code is divided into basic blocks.Basic corresponding statement.For pointer-type data,such a problem does not exist.Because a pointer-related side block,which is a concept in code optimization and gener- ation,is a sequence of instruction;and in our design,the condition is consistent with the premise of the corre- instruction sequence ends with a control transfer instruction sponding inference rule in the pointer logic,and should have been checked before the rule is chosen. such as jmp or call.Each basic block B has its precon dition P,postcondition Q,and the proof or proof hint of 3.When we compute pointer-related assertions,we need [P}B {Q}.The proof can be checked by a proof checker. According to the principle that the postcondition of a basic to decide which assignment rule to use according to the block should imply the precondition of the succeeding ba- assertion before the assignment.However,there is no need to do that about integer-related assertions using sic block in the control flow.Q can be omitted since we can just take the precondition of the succeeding basic block as wp. In fact,the computations of assertions and VCs for In order to make sure that each basic block has perti- integer-type data and pointer-type data interact with each nent pre-and postconditions,assertions should be gener- other. ated at proper program points during code generation.In this section,we introduce a scheme for generating interme- 1.Both of them should be performed together with type diate code and the corresponding assertions.For the lack checking,since they both need side conditions in the of space,we only consider pointer-related assertions.Us- typing rules.But the backward calculus for integer- ing the calculi in section 3,we can get a proper assertion related assertions will reduce the efficiency of the per- at each program point.Figure 3 shows the scheme for the formance,because the calculus direction does not con- main syntactic structures.The first parameter of the recur- sist with the direction of type checking. sive function Code is a syntactic structure.and the second parameter is the precondition of the structure.The function 2.The pre-and postconditions of functions,loop invari- Code generates intermediate code and assertions at some ants and the Bexps of while and if statements may program points.The generated assertion is at the right side contain both integers and pointers.Such an assertion of the code.The assertion which follows"--"should be should be divided into two parts,each of which con- inserted before the line of the code,and which follows"++" cerns only one kind of data and participates one calcu- should be inserted after the line of the code;and the as- lus. sertion led by "**"is the VC to be proved.The function Code calls function code which uses syntactic structure as 3.The variable p->data makes sense only when p is an the only parameter.The function code only generates in- effective pointer,but in Hoare logic,there is no such a termediate code for the syntactic structure.The function consideration.Therefore.rules in Hoare logic can not Code does not generate assertions between the intermediate be used in the case where pointers are concerned.The code which will obviously be translated into the same ba- pointer logic collects pointer equality information,and sic block,such as the code for assignment statements and this information can help us check whether p->data Boolean expressions (Boolean expression calculation does makes sense.Moreover,when using assignment ax- not use short-circuit here).The description in Figure 3 actu- iom,we can perform alias substitution [2]according ally covers some assertion and VC generations in Figure 2, to the equality information of pointers. hence all of these can be done via a one-pass inspection of source programs during compilation. Using the pointer logic,it is easy to prove the correct- When considering the generation of integer-related as- ness of the VC generation,i.e.,if all of the VCs are proved. sertions and VCs,it is difficult to do all the work about the Hoare triple [P}id(arg){Body}[Q}holds.The VC pointers and integers in one pass,because they are based generator is removed from the TCB,since there is a proof on the calculi in different directions.The compiler can checker at assembly level in our framework.Specifications, do type checking,pointer-related assertion generation,VC VCs and the proofs of VCs at source level will be trans- generation,integer side-condition annotation and interme- lated into equivalent assembly-level counterparts.And the diate code generation in the first pass and generate integer- translated counterparts will be used in the verification at as- related assertions and VCs using the annotation of integer sembly level. side conditions in the second pass.tion and StmtList is the statement sequence of the func￾tion. 2. The side condition in a typing rule should be combined with the assertion which is at the entry point of the corresponding statement. For pointer-type data, such a problem does not exist. Because a pointer-related side condition is consistent with the premise of the corre￾sponding inference rule in the pointer logic, and should have been checked before the rule is chosen. 3. When we compute pointer-related assertions, we need to decide which assignment rule to use according to the assertion before the assignment. However, there is no need to do that about integer-related assertions using wp. In fact, the computations of assertions and VCs for integer-type data and pointer-type data interact with each other. 1. Both of them should be performed together with type checking, since they both need side conditions in the typing rules. But the backward calculus for integer￾related assertions will reduce the efficiency of the per￾formance, because the calculus direction does not con￾sist with the direction of type checking. 2. The pre- and postconditions of functions, loop invari￾ants and the Bexps of while and if statements may contain both integers and pointers. Such an assertion should be divided into two parts, each of which con￾cerns only one kind of data and participates one calcu￾lus. 3. The variable p->data makes sense only when p is an effective pointer, but in Hoare logic, there is no such a consideration. Therefore, rules in Hoare logic can not be used in the case where pointers are concerned. The pointer logic collects pointer equality information, and this information can help us check whether p->data makes sense. Moreover, when using assignment ax￾iom, we can perform alias substitution [2] according to the equality information of pointers. Using the pointer logic, it is easy to prove the correct￾ness of the VC generation, i.e., if all of the VCs are proved, the Hoare triple {{P}} id(arg){Body} {{Q}} holds. The VC generator is removed from the TCB, since there is a proof checker at assembly level in our framework. Specifications, VCs and the proofs of VCs at source level will be trans￾lated into equivalent assembly-level counterparts. And the translated counterparts will be used in the verification at as￾sembly level. 4. Code and assertion generation In our framework, specifications and the proof of code satisfying the specifications are carried in the assembly code. The assembly code is divided into basic blocks. Basic block, which is a concept in code optimization and gener￾ation, is a sequence of instruction; and in our design, the instruction sequence ends with a control transfer instruction such as jmp or call. Each basic block B has its precon￾dition P, postcondition Q, and the proof or proof hint of {{P}} B {{Q}}. The proof can be checked by a proof checker. According to the principle that the postcondition of a basic block should imply the precondition of the succeeding ba￾sic block in the control flow, Q can be omitted since we can just take the precondition of the succeeding basic block as Q. In order to make sure that each basic block has perti￾nent pre- and postconditions, assertions should be gener￾ated at proper program points during code generation. In this section, we introduce a scheme for generating interme￾diate code and the corresponding assertions. For the lack of space, we only consider pointer-related assertions. Us￾ing the calculi in section 3, we can get a proper assertion at each program point. Figure 3 shows the scheme for the main syntactic structures. The first parameter of the recur￾sive function Code is a syntactic structure, and the second parameter is the precondition of the structure. The function Code generates intermediate code and assertions at some program points. The generated assertion is at the right side of the code. The assertion which follows “--” should be inserted before the line of the code, and which follows “++” should be inserted after the line of the code; and the as￾sertion led by “∗∗” is the VC to be proved. The function Code calls function code which uses syntactic structure as the only parameter. The function code only generates in￾termediate code for the syntactic structure. The function Code does not generate assertions between the intermediate code which will obviously be translated into the same ba￾sic block, such as the code for assignment statements and Boolean expressions (Boolean expression calculation does not use short-circuit here). The description in Figure 3 actu￾ally covers some assertion and VC generations in Figure 2, hence all of these can be done via a one-pass inspection of source programs during compilation. When considering the generation of integer-related as￾sertions and VCs, it is difficult to do all the work about pointers and integers in one pass, because they are based on the calculi in different directions. The compiler can do type checking, pointer-related assertion generation, VC generation, integer side-condition annotation and interme￾diate code generation in the first pass and generate integer￾related assertions and VCs using the annotation of integer side conditions in the second pass