Predicate definition unrolling

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 type-instantiated body that is inlined.

(The problem only had to do with generic types, not allocation states as I alluded to above.)

Rustan