Apr 23, 2013 at 11:33 PM
Edited Apr 23, 2013 at 11: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)
}



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



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

