usage of extends, unique, and complete

Jan 6, 2015 at 1:01 PM
Edited Jan 6, 2015 at 1:01 PM
I'm translating Java into Boogie and I don't seem to understand what Boogie is doing with extends, unique, and complete. Here is the generated Boogie program that I am wrongly able to verify:
type ref,  javaType, Field T;
type $heap_type = <T>[ref,Field T]T;
var $heap : $heap_type;

const  unique A : javaType extends  complete;
const  unique B : javaType extends  unique A complete;
const  unique C : javaType extends  unique B, unique A complete;

procedure foo($this:ref) {
  assert false;
}
I tried fiddling with the unique and complete but as long as these three constant declarations are in there, I can verify the assert false.
Mar 13, 2015 at 1:15 PM
Edited Mar 13, 2015 at 6:52 PM
I find [This is Boogie2 manual, Page 39 - 44] gives explanation on these keywords. The only thing I find in the manual that is out of date will be the extends keyword. I assume it means immediate parent.

I think snippet above introduces the following facts:
  1. A has exactly two immediate child B and C. (A has no immediate parent)
  2. B has only C as its immediate child.
  3. B has A as its immediate parent. (C is not immediate parent of B, since it is not mentioned in the declaration of B)
  4. C has no immediate child.
  5. C has A as its immediate parent.
  6. C has also B as its immediate parent ==> C <: B.
  7. child of B and C are disjoint. (since B and C have unique parent edge to A) ==> (forall t1,t2: javaType :: t1 <: B && t2<: C ==> t1!=t2).
fact 6 and 7 entails inconsistency (i.e. instantiate t1 and t2 with C).
Mar 13, 2015 at 5:26 PM
Ah ... Thanks. However, this only solves half the problem:
If you test this snippet on rise4fun, you can get rid of the problem by removing:
var $heap : $heap_type;
or even by changing its type to, e.g., javaType. Any idea what happens there?
Mar 13, 2015 at 6:44 PM
Edited Apr 25, 2015 at 2:00 PM
aha, that is exactly what I just did. I thought at first that was a bug (If I use Boogie v2.2, even I delete line3, it still verified). But actually it makes sense.

When I get rid of line3. it complains assertion might not hold. But I think it is because SMT solver doesn't know, not assertion failed.

I suspect after delete line3, certain axioms about partial order information will not instantiated, and SMT solver just simply stop trying. If I provide hints to instantiate these axioms I can still prove false, e.g. see here.

Moreover, I have a very similar example. I suspect the inconsistency is however caused by another reason - immediate parent. I thought might be of interest
type javaType;

const  unique A : javaType extends ;
const  unique B : javaType extends A;
const  unique C : javaType extends A,  B ;

procedure foo() {
  assert false;
}
It says that the immediate parent of C is A and B, which implies no element between A and C, yet since partial order operator is transitive, we have C<: B <: A, so that B is between A and C. So a contradiction is introduced.