1100p: {n>=0} cmpl %esi,%eax 2 ltrue int mult (m,n)f jg lfalse: 3 int x,y; 4 movl -16(%ebp),%eax x=0; lend 5 y=0; imp while (y n){x ==m *y A y <n} ltrue: 7 movl 16(%ebp),%eax XX m; 2 addl 8 y=y+1; -16(%ebp),%eax 9 3 movl %eax,-16(%ebp) 4 movl 10 $1,%eax return x; 11 5 addl -20(%ebp),%eax 12 6 movl fresult =m n} %eax,-20(%ebp) 7 jmp 1100p lend: Figure 4.The source code and corresponding assembly code of mult(m,n) Instruction: Operational semantics:upd(S,Precondition:gp(,Q) movlr1.r2 Sr2-→S(r1)I AS.Q(Sr2→S(r1) movlr1,z(r2) Sz+S(r2)→S(r1, λS.Q(Sz+S(r2)→S(r1) if(z+S(r2)∈Dom(S) movlz,r Sr→z, λS.Q(Sr→z) jmp 1 S addlz(r1),r2 Sr2→S(z+S(r1)+S(r2J λS.Q(Sr2→S(z+S(r1)+S(r2J if(z+S(r1)∈Dom(S) movl z(r1),r2 S[r2→S(z+S(r1)小， λS.Q(Sr2→S(z+S(r1)]) if(z+S(r1)∈Dom(S) Figure 5.Operational semantics and assertion generation of some instructions block.For example,from postcondition q.we can get the And the VC at the entry point of the basic block is: precondition of"jmp lloop"(the instruction labeled with 7): AS.S(S(ebp)-16)=S(S(ebp)+16)x S(S(ebp)-20)A S(S(ebp)-20)<S(S(ebp)+12)A S(S(ebp)-20)<S(S(ebp)+12) AS.S(S(ebp)-16)=S(S(ebp)+16)x S(S(ebp)-20)A (AS.S(S(ebp)-16)+S(S(ebp)+16) S(S(ebp)-20)<S(S(ebp)+12). =S(S(ebp)+16)×(S(S(ebp)-20)+1)A S(S(ebp)-20)+1<S(S(ebp)+12)) That is,the precondition of the basic block should imply the The preconditions of the rest instructions can be generated precondition of the first instruction in the basic block.And in a similar way.The precondition of the first instruction is: this VC is easy to prove obviously. When we get all the assertions between the instructions, there is no difficulty to generate the proof of PQ}for AS.S(S(ebp)-16)+S(S(ebp)+16) each instruction t in a basic block.And it is also easy to =S(S(ebp)+16)×(S(S(ebp)-20)+1)A generate a proof for the basic block if we have the proofs for all the instructions in the basic block and the proof for S(S(ebp)-20)+1≤S(S(ebp)+12). the VC of the basic block.1 {{n >= 0}} 2 int mult (m, n){ 3 int x, y; 4 x = 0; 5 y = 0; 6 while (y < n) { {{x == m * y ∧ y <= n}} 7 x = x + m; 8 y = y + 1; 9 } 10 return x; 11 } 12 {{result == m * n}} lloop: ··· cmpl %esi, %eax jg ltrue lfalse: movl -16(%ebp), %eax jmp lend ltrue: 1 movl 16(%ebp), %eax 2 addl -16(%ebp), %eax 3 movl %eax, -16(%ebp) 4 movl $1, %eax 5 addl -20(%ebp), %eax 6 movl %eax, -20(%ebp) 7 jmp lloop lend: ··· Figure 4. The source code and corresponding assembly code of mult (m, n) Instruction: ι Operational semantics: upd(S, ι) Precondition: gp(ι, Q) movl r1, r2 S[r2 → S(r1)] λS.Q (S[r2 → S(r1)]) movl r1, z(r2) S[z + S(r2) → S(r1)], λS.Q (S[z + S(r2) → S(r1)]) if (z + S(r2)) ∈ Dom(S) movl z, r S[r → z], λS.Q (S[r → z]) jmp l S Q addl z(r1), r2 S[r2 → S(z + S(r1)) + S(r2)], λS.Q (S[r2 → S(z + S(r1)) + S(r2)]) if (z + S(r1)) ∈ Dom(S) movl z(r1), r2 S[r2 → S(z + S(r1))], λS.Q (S[r2 → S(z + S(r1))]) if (z + S(r1)) ∈ Dom(S) Figure 5. Operational semantics and assertion generation of some instructions block. For example, from postcondition q, we can get the precondition of “jmp lloop” (the instruction labeled with 7): λS.S(S(ebp) − 16) = S(S(ebp) + 16) × S(S(ebp) − 20)∧ S(S(ebp) − 20) ≤ S(S(ebp) + 12). The preconditions of the rest instructions can be generated in a similar way. The precondition of the first instruction is: λS.S(S(ebp) − 16) + S(S(ebp) + 16) = S(S(ebp) + 16) × (S(S(ebp) − 20) + 1)∧ S(S(ebp) − 20) + 1 ≤ S(S(ebp) + 12). And the VC at the entry point of the basic block is: λS.S(S(ebp) − 16) = S(S(ebp) + 16) × S(S(ebp) − 20)∧ S(S(ebp) − 20) ≤ S(S(ebp) + 12)∧ S(S(ebp) − 20) < S(S(ebp) + 12) ⊃ (λS.S(S(ebp) − 16) + S(S(ebp) + 16) = S(S(ebp) + 16) × (S(S(ebp) − 20) + 1)∧ S(S(ebp) − 20) + 1 ≤ S(S(ebp) + 12)). That is, the precondition of the basic block should imply the precondition of the first instruction in the basic block. And this VC is easy to prove obviously. When we get all the assertions between the instructions, there is no difficulty to generate the proof of {{P}} ι {{Q}} for each instruction ι in a basic block. And it is also easy to generate a proof for the basic block if we have the proofs for all the instructions in the basic block and the proof for the VC of the basic block