ChristophBaumann 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 muchBy the way, a more concise set notation as suggested by Michal Moskal would be highly appreciated ;)` MarkHillebrand 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 ChristophBaumann 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? stobies 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?