1
Vote

Unsoundness?

description

Hi,

Consider the following code:
int x;
 void foo()
   _(ensures x == \old(x))
 {
 }
This code verifies... but should not? Shouldn't x be able to obtain any value during the execution of foo?
It might be that the post-condition won't be able to be used to infer other properties, and thus, this will not really lead to any issues. Nonetheless, it doesn't seem correct to me.

/Jonas

comments