[Dafny]: Assertion failed in checking well formed local variables in forall-expressions.

Jul 1, 2012 at 6:41 PM

Hey everyone, 

I have the following dafny code:

class aux
{
	static function validSet (a: set<Node>, bar: int) : bool
	reads a;
	{
		(forall n : Node | n!= null && n.index <= 3 && n in a  :: n.d > bar)
	}
}

class Node{
	var index : int;
	var d : int;

	constructor Init(index: int, d: int)
	modifies this;
	{
		this.d := d;
		this.index := index;
	} 
}

class test
{
	var data : set<Node>;
	var bar : int;

	method Init()
	modifies this;
	ensures aux.validSet(data, 0);
	{
		var n1 := new Node.Init(0, 1);
		var n2 := new Node.Init(1, 2);
		var n3 := new Node.Init(3, 5);
		data := {n1, n2, n3};
	}
}

There are some translated code:

implementation CheckWellformed$$_default.aux.validSet(a#0: Set BoxType, bar#1: int)
{
  var $_Frame: <beta>[ref,Field beta]bool;
  var n#8: ref;

    if (*)
    {
        assume false;
    }
    else
    {
        $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> a#0[$Box($o)]);
        havoc n#8;
        assume n#8 == null || (read($Heap, n#8, alloc) && dtype(n#8) == class._default.Node);
        if (n#8 != null)
        {
            assert n#8 != null;
            assert $_Frame[n#8, _default.Node.index];
        }

        if (n#8 != null && read($Heap, n#8, _default.Node.index) <= 3)
        {
        }

        if (n#8 != null && read($Heap, n#8, _default.Node.index) <= 3 && a#0[$Box(n#8)])
        {
            assert n#8 != null;
            assert $_Frame[n#8, _default.Node.d];
        }

        assume _default.aux.validSet($Heap, a#0, bar#1) == (forall n#2: ref :: (n#2 == null || (read($Heap, n#2, alloc) && dtype(n#2) == class._default.Node)) && n#2 != null && read($Heap, n#2, _default.Node.index) <= 3 && a#0[$Box(n#2)] ==> read($Heap, n#2, _default.Node.d) > bar#1);
        assume (forall n#2: ref :: n#2 == null || (read($Heap, n#2, alloc) && dtype(n#2) == class._default.Node) ==> (n#2 != null ==> true) && (n#2 != null && read($Heap, n#2, _default.Node.index) <= 3 ==> true));
    }
}

The red highlighted assertion failed. 

I have two questions about checking-well-formed forall-expressions:

1. Why do we check local variables in forall-expressions?

2. If we have to check them, should we add the ranges as an assumption in the green highlighted line?

 

Thanks

Yuyan Bao

Coordinator
Oct 15, 2012 at 11:41 PM

[I'm noticing that this was never answered.  I don't know if the answer is still useful, but here goes.]

The purpose of the CheckWellformed$$...validSet procedure is to verify that the Dafny function validSet always makes sense.  In other words, it will check that the evaluation of validSet's body will never crash.  For example, this will check that evaluating the function body will not result in a division-by-zero error or a null-dereference error or a violated precondition of other functions that validSet may call.

In your example, the body of validSet consists solely of a universal quantifier. It may be helpful to think about how you would do the evaluation at run-time, because that also corresponds to what the Boogie translation looks like.  One would then first evaluate the expression "n != null", which never crashes and always produces a boolean.  If the boolean produced is "true", then the next conjunct, "n.index <= 3" is evaluated.  It can crash if n is null, and it also does not respect the "reads" clause unless "n" denotes something in the reads clause.  To prescribe these checks, the translation into Boogie lays down code that:

* introduces a local variable ("n#8") to represent the bound variable in the quantifier, and sets it to an arbitrary value (using the "havoc" statement)

* in the event that "n != null" holds, then it will check the well-formedness of "n.index <= 3", which is done by checking "n#8 != null" and checking that (n#8, index) denotes a heap location included in the "reads" clause.

Etc.

Note that the full range condition is assumed (in an "if" statement in the Boogie code) by the time the term of the quantifier (that is, the part after the "::") is checked for well-formedness.

The whole purpose of the well-formedness checking is to make sure that the expressions will evaluate without crashing.  Each piece of the expression must be checked before it is okay to assume anything about its value.  For example, suppose the Dafny code did include include "n != null", then your green assumption may be assuming something about "null.index", which is not defined in the Dafny program.  As another example, suppose the Dafny code instead listed "n.index <= 3 && n != null" (that is, reversing the order of the conjuncts from above), then adding the green assumption would make the well-formedness check of the first conjunct ("n.index <= 3") always go through--this is not sound, since a run-time evaluation of the the condition "n.index <= 3 && n != null" could crash if n is null (since evaluation is left-to-right).

For some reading about this, I suggest my Marktoberdorf 2008 lecture notes, which talk about the translation of Dafny into Boogie.

  Rustan

Oct 20, 2012 at 2:23 PM
Edited Oct 20, 2012 at 2:26 PM

Hey Rustan,

Thank you for replying. I do need to learn more about translations. I will read your lectures. Thanks for the suggestion.

I changed the quantifier to the following:

 

(forall n :: n in a ==>  n!= null && n.index <= 3 && n.d > bar)

 

And the translated code are changed to:

 

implementation CheckWellformed$$_module.aux.validSet(a#0: Set BoxType, bar#1: int)
{
  var $_Frame: [ref,Field beta]bool;
  var n#8: ref;

    if (*)
    {
        assume false;
    }
    else
    {
        $_Frame := (lambda $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> a#0[$Box($o)]);
        havoc n#8;
        assume n#8 == null || (read($Heap, n#8, alloc) && dtype(n#8) == class._module.Node);
        if (a#0[$Box(n#8)])
        {
            if (n#8 != null)
            {
                assert n#8 != null;
                assert $_Frame[n#8, _module.Node.index];
            }

            if (n#8 != null && read($Heap, n#8, _module.Node.index) <= 3)
            {
                assert n#8 != null;
                assert $_Frame[n#8, _module.Node.d];
            }
        }

       ...
    }
}

 

I notice that "if (a#0[$Box(n#8)])" is added into the translated code. That makes the failed assertion disappears. But the postcondition of method Init() still cannot be proved. I guess I may need more preconditions.

Thanks

Yuyan

Coordinator
Oct 21, 2012 at 9:45 PM

Hi Yuyan,

To get your program to verify, you need to do two things.

First, the expression "n.index <= 3" is not permissible in the definition of validSet.  Note that the well-formedness checks are performed left-to-right, and when "n.index <= 3" is encountered, nothing is known about "n" other than that it's a non-null Node.  This does not give validSet permission to read the field "n.index".  To fix the problem, the conjunct "n in a" must precede "n.index <= 3", because "n in a" and "reads a;" are what give validSet permission to read the fields of "n".

Second, to prove the postcondition of test.Init(), you must know something about the "d" field of the "n1", "n2", and "n3".  So, you need to strengthen the postcondition of Node.Init to say something about the value of the "d" field.

Here is a verifying version of your program:  http://rise4fun.com/Dafny/tHplc

  Rustan

Oct 21, 2012 at 11:52 PM

Hi Rustan,

YEAH! It is working. Thank you very much. I hope I could have a chance to talk with you in SPLASH :).

Yuyan