CodePlexProject Hosting for Open Source Software

Now, let’s assume we don’t want to include points in the rectangle we want to point to them. The invariant now becomes not only slightly more involved:

First of all it now needs to say it is going to read not only the object pointed to by r, but also whatever r->ll and r->ur point to. Next the invariant needs to ensure validity of all those three objects (in the previous example we have just used SAL for validity, here it is not possible).

Next we need to make sure those pointers ll and ur are not identical, otherwise in some odd cases the move function could break the postcondition of the function move . In those cases, where both pointers were used as an*alias* to the same memory location, the first two assignments of move would be lost.

Finally we check the normal correctness condition, we have also checked previously. The move function didn’t change much, except for the writes(…) clause, that mimics the reads(…) on the invariant.

#include "vcc.h" struct point { int x; int y; }; struct rect { struct point *ll; struct point *ur; invariant(inv_rect(this)) invariant(keeps(ll)) invariant(keeps(ur)) invariant(ll != ur) }; spec(ispure bool inv_rect(struct rect * r) reads(r) returns(r->ll->x <= r->ur->x && r->ll->y <= r->ur->y);) spec(ispure bool within_bounds(struct rect* r, int dx, int dy) reads(r) returns( 0 <= r->ll->x + dx && r->ll->x + dx < 1024 && 0 <= r->ur->x + dx && r->ur->x + dx < 1024 && 0 <= r->ll->y + dy && r->ll->y + dy < 1024 && 0 <= r->ur->y + dy && r->ur->y + dy < 1024 ); ) void move(struct rect *r, int dx, int dy) maintains(wrapped(r)) writes(r) requires(within_bounds(r, dx, dy)) { unwrap(r); unwrap(r->ll); unwrap(r->ur); r->ll->x = unchecked(r->ll->x + dx); r->ll->y = unchecked(r->ll->y + dy); r->ur->x = unchecked(r->ur->x + dx); r->ur->y = unchecked(r->ur->y + dy); wrap(r->ur); wrap(r->ll); wrap(r); }

First of all it now needs to say it is going to read not only the object pointed to by r, but also whatever r->ll and r->ur point to. Next the invariant needs to ensure validity of all those three objects (in the previous example we have just used SAL for validity, here it is not possible).

Next we need to make sure those pointers ll and ur are not identical, otherwise in some odd cases the move function could break the postcondition of the function move . In those cases, where both pointers were used as an

Finally we check the normal correctness condition, we have also checked previously. The move function didn’t change much, except for the writes(…) clause, that mimics the reads(…) on the invariant.

Last edited Nov 13, 2009 at 12:01 PM by stobies, version 3