Similar to the use of old to refer to distinct execution states, it is possible to store current state in specification variables and even pass states in function calls:

#include <vcc.h>

struct S {
    int a;
    int b;
};

void swap(struct S *p)
    writes(extent(p))
{
    spec(state_t s0 = current_state();)
    spec(state_t s1;)
    int tmp = p->a;
    p->a = p->b;
    p->b = tmp;
    spec(s1 = current_state();)
    assert(in_state(s0, p->a) == in_state(s1, p->b));
    assert(in_state(s0, p->b) == in_state(s1, p->a));
}


In this example, we use an explicit state variables to achieve what could equally be achieved by using old and expressions without referring to a specific state.

With the same mechanism, we can now move this comparison into a specification function:

spec(bool ispure swapped(struct S *p, state_t s0, state_t s1)
  returns (in_state(s0, p->a) == in_state(s1, p->b) && in_state(s1, p->a) == in_state(s0, p->b));
)


and then, in foo add the following assertion in the end:

assert(swapped(p, s0, s1));

Last edited Feb 11, 2011 at 8:01 PM by MarkHillebrand, version 5

Comments

No comments yet.