Hi Rustan,
Thank you very much for your reply!
My example is indeed more complex than the one you have come up with. In particular, there is a further layer of indirection: this is of type 'StudentExtent', which keeps its 'StudentElement' instances in its 'elements' field. Via 'top' an instance of 'StudentExtent'
gets hold of a singleton instance 'StudentTop' that keeps all existing 'StudentExtent' instances in the set 'extents'. So the class structure looks like:
class StudentTop {
var extents: set<StudentExtent>;
}
class StudentExtent {
var elements: set<StudentElement>;
var top: StudentTop;
method createStudent(id: int) returns (element: StudentElement) ... {...} // see above
}
class StudentElement {
}
The invariant of 'StudentExtent' is actually trivial, the one for 'StudentElement' simple, and the one for 'StudentTop' a bit more involved. I am happy to provide the full code example if that's helpful for the discussion. Also note that in method 'createStudent()',
'this' is already contained in 'this.top.extents', i.e., it's added when it's created.
So I continued debugging my code using the 'parallel' construct (you meant PARALLEL rather than FORALL, correct?). Doing this, I was finally able to prove (5), but I came across a very strange, almost buggy behavior. Let me explain. Here is the new code excerpt
that verifies:
method createStudent(id: int) returns (element: StudentElement)
...
ensures forall ex :: ex in this.top.extents ==> ex.Inv() &&
forall e :: e in ex.elements ==> e.Inv(); // (1)
{
...
assume forall ex :: ex in this.top.extents ==> (ex != this ==> (ex.Inv() &&
forall e :: e in ex.elements ==> e.Inv())); // (2) NOTE DIFFERENCE!
assert forall ex :: ex in this.top.extents ==> ex.Inv(); // (3)
assert this in this.top.extents &&
forall e :: e in this.elements ==> e.Inv(); // (4)
parallel (ex  ex in this.top.extents) // (6)
ensures ex.Inv() && forall e :: e in ex.elements ==> e.Inv();
{
parallel (e  e in ex.elements)
ensures e.Inv();
{
if (ex == this) {
} else {
}
}
}
assert forall ex :: ex in this.top.extents ==>
forall e :: e in ex.elements ==> e.Inv(); // (5)
}
Basically it looks like the if statement in the parallel block (6) enables the verification of (5), i.e., if I uncomment block (6), I get a timeout. However, note that to make the above code verifiable, I had to change (2) from
assume forall ex :: ex in (this.top.extents  {this}) ==> (ex.Inv() && forall e :: e in ex.elements ==> e.Inv()); // (2)
to
assume forall ex :: ex in this.top.extents ==> (ex != this ==> (ex.Inv() && forall e :: e in ex.elements ==> e.Inv())); // (2)
If I use the former instead, the above code results in a timeout. Likewise, if I remove the if statement from the parallel block, a timepout occurs.
Do you have any idea what the problem is here? I am happy to provide the full program, if that would be helpful.
Thanks a lot,
Stephanie
