1

Closed

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
Closed Today at 12:14 AM by erniecohen
By design

comments

erniecohen wrote Today at 12:12 AM

This is correct. VCC tacitly uses a reduction theorem to pretend that a thread is interrupted only just before an atomic action or at a function call. Since this code body has neither, we can safely "pretend" that foo() executes without interruption.

Remember that an assertion in VCC that mentions data not in the ownership domain of the thread under consideration doesn't mean quite what it means in standard concurrent program logics.