
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 checkingwellformed forallexpressions:
1. Why do we check local variables in forallexpressions?
2. If we have to check them, should we add the ranges as an assumption in the green highlighted line?
Thanks
Yuyan Bao



[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 divisionbyzero error or a nulldereference 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 runtime, 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 wellformedness 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 wellformedness.
The whole purpose of the wellformedness 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 wellformedness check of the first conjunct ("n.index <= 3") always go throughthis is not sound, since a runtime evaluation of the the condition
"n.index <= 3 && n != null" could crash if n is null (since evaluation is lefttoright).
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 3:23 PM
Edited Oct 20, 2012 at 3: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



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 wellformedness checks are performed lefttoright, and when "n.index <= 3" is encountered, nothing is known about "n" other than that it's
a nonnull 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



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

