Verification : If statement with no alternative branch

Is such program considered valid for the verifier? i.e

int f(int x){
_Assume(x==y);
y=x;
if(x<0) 
    y=0-x;
_Assert(y>0)
return x;
}

No, the program does not type, since y is not declared anywhere.
If we add it as a second parameter, the the program is valid for the verifier. It is, however, not correct, since x (and thus y) may be 0. If you change your postcondition to y >= 0, it is.

The semantics of if without else are as if you had an empty block in the else.

I just mistyped its declaration, thanks for the clarification. Could the declaration happen before the _Assume or every function should start with the _Assume if there is any?

_Assume and _Assert can in occur anywhere any other statement can occur. Due to some confusion early on (Verification only one assume meaningful - #4 by johannes), we said that we do not test the case of more than one _Assume(), but it’s easier to just implement the given rules, which already allow _Assume() and _Assert() anywhere, than to come up with your own (likely wrong) variant of them.

1 Like

Do you think that the generated Formula for the following program with 2 assume statement is sound? notice that I have used the suggested rule as far as I understood

int f(int x, int y){
      _Assume(x==y);
      y=x;
      if(x<0) 
          {y=0-x;
          _Assume(y ==x && y>0);} // updated
      else {}
      _Assert(y>0)
      return x;
}

Formula :
ass2

I don’t know, your program is not syntactically valid… Are you sure that you piped exactly this program into your compiler?

you are right, I just re-typed it and missed the bracket, will update it.

Alright. The generated formula seems sensible for that approach.

I would still recommend that you write a lot of own tests, where your have programs with specifications for which you know the program should be correct, and invalid specifications/programs, just to catch any mistake.

Debugging programs by staring at formulas is not fun, as you might have realized by now :slightly_smiling_face:

1 Like