Apr 23, 2013 at 10:33 PM
Edited Apr 23, 2013 at 10:36 PM

In the following, the step marked with *** does not go through, even though it is nothing more than an unrolling of predicate definition.
ghost method test_unrolling( )
{ var xs:= Cons(1,Cons(2, Nil));
var ys:= Cons(2,Cons(1, Cons(1, Nil)));
calc{
subset(xs,ys);
==
forall x:: elem(x,xs) ==> elem(x,ys); // *** Does not verify
}
}
Neither does the following go through
ghost method test_unrolling2( )
{ var xs:= Cons(1,Cons(2, Nil));
var ys:= Cons(2,Cons(1, Cons(1, Nil)));
assert forall x:: elem(x,Cons(1, Nil)) ==> x==1;
assert forall x:: elem(x,xs) ==> (x==1  x==2);
calc{
subset(xs,ys);
== { assert forall x:: elem(x,xs) ==> (x==1  x==2); }
elem(1,ys) && (elem(2,ys); // *** Does not verify
}
}
Here the predicate subset, defined through quantifiers
predicate subset<T>(xs: list<T>, ys: list<T>)
{
forall x :: elem(x, xs) ==> elem(x, ys)
}


Coordinator
Apr 24, 2013 at 12:23 AM

This annoying problem has to do with allocation states and integers and the generic type T. I shall think about a fix.


Coordinator
Apr 24, 2013 at 11:56 PM

Fixed in change set 8ad56e85c419. Now, when the body of a predicate is inlined (which is done in many places where the predicate is checked to hold), then it is now the typeinstantiated body that is inlined.
(The problem only had to do with generic types, not allocation states as I alluded to above.)
Rustan

