Sep 29, 2009 at 4:35 PM
Edited Sep 29, 2009 at 4:39 PM

Hi all!
i recently played around a bit with pointer sets and operations working on them and i noticed that quite a lot of properties for these operation are missing. please look at the following examples:
#include "vcc.h"
spec( void foo(ptrset A, ptrset B, ptrset C, ptrset D) requires(set_subset(D,B)) requires(A == set_union(B,C)) requires(set_intersection(B,C) == set_empty()) { ptrset E = set_union(B,D); assume(forall(ptrset Y,Z; set_subset(Z,Y) ==> Y == set_union(Y,Z))); assert(E == B); ptrset F = set_difference(B,D); assume(forall(ptrset X,Y,Z; set_subset(Y,X) && (Z == set_difference(X,Y)) ==> X == set_union(Z,Y))); assert(B == set_union(F,D)); assert(A == set_union(set_union(F,D),C));
ptrset G = set_union(C,D); assume(forall(ptrset X,Y; set_union(X,Y) == set_union(Y,X))); assume(forall(ptrset W,X,Y,Z; set_subset(Z,X) && (set_intersection(X,Y) == set_empty()) && (W == set_difference(X,Z)) ==> set_union(set_union(W,Z),Y) == set_union(W,set_union(Z,Y)))); assert(set_union(set_union(F,D),C) == set_union(F,set_union(C,D))); assert(A == set_union(F,G)); } )
the assumed properties could not be asserted.
some more examples:
assume(forall(ptrset X,Y; set_intersection(X,Y) == set_empty() ==> X == set_difference(X,Y))); assume(forall(ptrset X,Y; set_intersection(X,Y) == set_intersection(Y,X))); assert(forall(ptrset X,Y; (set_intersection(Y,X) == set_empty()) ==> X == set_difference(X,Y)));
assume(forall(ptrset X; obj_t p; set_in(p,X) == 0 <==> set_intersection(set_singleton(p),X) == set_empty()));
assume(forall(ptrset W,X,Y,Z; (set_intersection(X,Y) == set_empty()) && (W == set_difference(X,Z)) ==> set_intersection(W,Y) == set_empty()));
assume(forall(ptrset X,Y,Z; (set_intersection(X,Y) == set_empty()) && (set_intersection(X,Z) == set_empty()) ==> set_intersection(X,set_union(Y,Z)) == set_empty()));
maybe i just used some awkward formulations but certain features above should be supported i think. Any suggestions/fixes concerning this issue? i would not like to use "assume" too much
By the way, a more concise set notation as suggested by Michal Moskal would be highly appreciated ;)



Hi Christoph,
you should use set_eq() for set equality, not ==. I don't understand the exact problems of using ==, though, Michal can you comment? Would it be feasible to let VCC insert an automatic translation or issue a warning?
I haven't checked through your examples, but at least the first assume() also works as an assert with set_eq():
assert(forall(ptrset Y,Z; set_subset(Z,Y) ==> set_eq(Y,set_union(Y,Z))));
Please feel free to report any remaining assertions for which that doesn't help.
Thanks, Mark


Sep 30, 2009 at 12:38 PM
Edited Sep 30, 2009 at 1:14 PM

thanks for clarifying!
i checked all the example and they work with set_eq, except for the following property:
assert(forall(ptrset X,Y; set_eq(set_intersection(X,Y),set_empty()) ==> set_eq(X,set_difference(X,Y))));
maybe someone can have a look at that?


Sep 30, 2009 at 12:42 PM
Edited Sep 30, 2009 at 1:24 PM

This is good to hear. We will look into this remaining inference and see if we can enable it easily (or maybe just add it as an extra axiom). See
On a related note, shouldn't we simply rewrite == for sets as set_eq? Or is there a separate use for set
identity?

