Test testAssignIf in verification

I am failing the test testAssignIf, from the name of the test, one might suggest it might be if statement with assignment in both case. I have tried to write some simple test to check the verification condition for assignment and if statement.

for example consider the following program
prog_if
the generated verification condition as per the below:
verf2

According to the if statement, it seems that the generated condition is as expected. what otherwise could go wrong in the test?

Many things could go wrong. When we look at your IfStatement::pc, we can see that your test does not even have branch coverage for that method. I’m pretty sure you will catch the bug once you write enough of your own tests :slightly_smiling_face:

Apart from this, you are handling your condition conversion in a rather weird way. I’m pretty sure that your current approach will not work. But it’s not the issue here.

let me write here the program with the Hoare Triple for each component of the program written annotated in the program for the sake of easier writing.

void f(int x, int y, int z){
 (1) {{ True }} // P
 if (x<=y) 
 (2) {{ True && x<=y }} =>

 (3){{ y=x + (y-x)}}

  {z=y-x;} 

  (4) {{ y=x+z  }} //Q
  
else 
 (5) {{True && x>y  }} =>

 (6) {{ x+z = x+z }}

  {y=x+z}

(7) {{ y=x+z  }} //Q

So for the if statement to be logically consistent in term of precondition P and postcondition Q, I should have at the end of each branch Q also having at the start of consequence branch P & cond and at the beginning of the alternative branch P && (not cond). According to the annotated program this I guess can be satisfied by having 2 implications 2 => 3 and 5=>6 which I guess should be the verification condition that should be proven, right?

Now coming back to the automatic verification rule pc and vc, applying vc[{Assume(true);if_else;Assert(y=x+z)}] would yield as below if I get it right

(x<=z && y= x+(y-z)) || (x>z && x+z=x+z ) which is not consistent with the above reasoning using the Hoare statement, I am not sure where my reasoning does go wrong?

I’m not completely sure I can follow your reasoning. Your merging of Hoare Triples and program code certainly does not improve clarity.

Our program s is (after removing redundant blocks)

if (x <= z)
  z = y - x;
else
  y = x + z;

Our postcondition Q is y == x + z.

Now, we can compute

pc (y = x + z;) Q = Q[x + z / y] = x + z == x + z
pc (z = y - x;) Q = Q[y - x / z] = y == x + (y - x)
pc s Q = (x <= z && pc (z = y - x;) Q) || (!(x <= z) && pc (y = x + z;) Q)
       = (x <= z && y == x + (y - x)) || (!(x <= z) && x + z == x + z)
     <=> (x <= z && y == x + y - x) || (x > z && x + z == x + z)

Now, since pc s Q is valid, the program is correct. Note that there are no side conditions (i.e. vc s Q is empty). You best stick to the rules for pc / vc presented in the script.

Where do your implications (2) \Rightarrow (3) and (5) \Rightarrow (6) come from? Why would you expect that vc generates them?

Using the consequence rule, actually it was used in similar way in the lecture handwritten note
pic1

What we have in the script (3) (4) (6) :
(1) P := true
(2) Q := y==x+z
(3) {true}{assume(p);S;assert(q)}{true} <=> {P}S{Q} Lemma 7.4.13
(4) vc {s1,..,sn}] Q= vc s1 (pc {s2,...,sn}Q) U vc {s2,...} Q
(5) c = {assume(true),ifStatement,Assert(Q)} where ifstatement as you have defined it up and here in a block since in the project the body of the function definition is a block according to rule in the grammar.
(6) vc[assume(e)]Q ={e=>Q} . first definition in the script before the last update which is valid as mentioned in previous post

To prove : {true}c{true} according to (3) <=> {P}{ifstatement}{Q}
vc c true = vc [Assume(true)](pc {ifstatement,assert(Q)} true) U ... using (4).

pc[{ifstatement:assert(Q)}] true = (x<=z && y= x+(y-x)) || (x>z && x+z=x+z) Side calculation.

vc c true = vc [Assume(true)]((x<=z && y= x+(y-x)) || (x>z && x+z=x+z)) U … according to (6) also vc remaining = {}

vc c true = true =>(x<=z && y= x+(y-x)) || (x>z && x+z=x+z)

Edit: detailed calc removed

I assume your question is “How does the pc/vc rule for if connect to the Hoare triple?”

The rule for if is that

{e && P} s_1 {Q}      {!e && P} s_2 {Q}
---------------------------------------
      {P} if (e) s_1 else s_2 {Q}

Now, vc just recurses into the subexpressions. pc of that if is (e && pc s_1 Q) || (!e && pc s_2 Q).

Our correctness statement of pc is

If vc s Q is valid, then {pc s Q} s {Q}.

We prove this by induction on s with Q quantified. The case for if looks as follows:

We are given

  • If vc s_1 Q is valid, then {pc s_1 Q} s_1 {Q} (by induction)
  • If vc s_2 Q is valid, then {pc s_2 Q} s_2 {Q} (by induction)
  • that vc (if (e) s_1 else s_2) Q is valid (an assumption)

Since vc (if (e) s_1 else s_2) Q=vc s_1 Q\cupvc s_2 Q, we can get proofs {pc s_1 Q} s_1 {Q} and similarly for s_2 from the induction hypotheses.

Our goal still is that {pc (if ..) Q} if .. {Q}. We apply the [If] rule, and get two new subgoals:

  1. {e && pc (if ..) Q} s_1 {Q} needs to be shown. We apply [Consequence] with the fact that {pc s_1 Q} s_1 {Q} (which we got from induction). For this to work, the side condition needs to be valid. It is:

        e && pc (if (e) s_1 else s_2) Q
     =  e && ((e && pc (s_1) q) || (!e && pc s_2 Q))
    <=> (e && e && pc (s_1) q) || (e && !e && pc s_2 Q)   | Distributivity
    <=> (e && pc (s_1) q) || (e && !e && pc s_2 Q)        | Idempotence
    <=> (e && pc (s_1) q) || (false && pc s_2 Q)          | Complement
    <=> (e && pc (s_1) q) || false                        | Annulment
    <=> e && pc (s_1) q                                   | Identity
     => pc s_1 q                                          | Monotonicity
    
  2. {!e && pc (if ..) Q} s_2 {Q} needs to be shown. We proceed similarly to case 1.


As you can see, we cleverly pick our pc rule for if such that there are no side remaining side conditions. Thus, this suffices.

Note that in your reasoning, your are mixing forwards and backwards reasoning. This works well on paper, for small examples, where you can pick a suitable spot where forwards and backwards reasoning meet. Your verifier needs to stick to one direction, and it turns out that doing backwards reasoning is much easier, so that’s what we are doing in the lecture.

1 Like

For the same explanation in other words:

2 Likes