Instantiation in Boogie

May 7, 2013 at 3:54 AM
I have a question that I think is related to the way Z3 does the instantiation of quantified variables. The first example below verifies OK, while the second one is not verified correctly by Boogie, although they are very similar. The only difference is that for the second example, in the axiom related to the function Range(...) I quantify over the global variable "next" (representing the next field of a cell in a linked list). Although the procedure addModulo11 makes "next[this] := null;" and hence the axiom about Range(...) should help to prove the post-condition of addModulo11, this does not happen.

In the first example, "next[this]" is simply given as a parameter to the function Range(...), so there is no instantiation of "next". I think that's why the first example works.

Does anyone know why this instantiation of "next" doesn't work in the second example?
//First example
//it works
//type Ref is intended to represent object references
type Ref;
const null:Ref;
var val: [Ref]int;
var next: [Ref]Ref;

function Range(this: Ref, val:[Ref]int, next:[Ref]Ref, x:int, y:int) returns (bool);

axiom (forall this:Ref, x:int, y:int, val: [Ref]int, next: [Ref]Ref :: 
{Range(this,val,next,x,y)}
  ((this == null)  ==> Range(this,val,next,x,y) == true ) 
   && 
  ((this != null)==> Range(this,val,next,x,y) == false)  
 );
         
procedure addModulo11(this: Ref) 
modifies val, next;
requires  Range(this,val,next,0,8);
ensures  Range(next[this],val,next,0,8) ;
{ 
  next[this] := null;
}
//end of first example
//second example
//doesn't work
//type Ref is intended to represent object references
type Ref;
const null:Ref;
var val: [Ref]int;
var next: [Ref]Ref;

function Range(this: Ref, val:[Ref]int, next:[Ref]Ref, x:int, y:int) returns (bool);

axiom (forall this:Ref, x:int, y:int, val: [Ref]int, next: [Ref]Ref :: 
{Range(this,val,next,x,y)}
  (next[this] == null)  ==> 
     Range(this,val,next,x,y) == true  
   && 
    (next[this] != null)==> 
     Range(this,val,next,x,y) == false);
         

procedure addModulo11(this: Ref) 
modifies val, next;
requires  Range(this,val,next,0,8);
ensures  Range(this,val,next,0,8);
{ 
  next[this] := null;
}
May 28, 2013 at 10:10 AM
Edited May 28, 2013 at 12:58 PM
Hi,

Is this a precedence problem between 'implication' and 'logical and'? Some parentheses in the axiom of second example might do the trick.

Cheers,
Zheng