This project is read-only.

Missing Axioms for Set Operations

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"

void foo(ptrset A, ptrset B, ptrset C, ptrset D)
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 ;)


Sep 29, 2009 at 6:25 PM

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 [workitem:2877].

On a related note, shouldn't we simply rewrite == for sets as set_eq? Or is there a separate use for set identity?