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;
}
```

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 :

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

1 Like