Meaning of where keyword

Sep 19, 2014 at 2:24 PM

Sorry if I have missed it, but I have been unable to locate documentation on the meaning of the where keyword. For example the where keyword is used in the Dafny Boogie prelude:
function $IsGoodHeap(Heap): bool;
var $Heap: Heap where $IsGoodHeap($Heap);
What does where do? I guess it is some kind of invariant?


Sep 19, 2014 at 2:39 PM
Edited Nov 7, 2014 at 2:34 PM
Hi Tim,

In Boogie where is used to declare constraints on a variable. It is sort of documented in "This is Boogie 2" document. If I recall correctly that are some subtleties to using it.

Here's an exerpt
var volume:int where 0 <= volume && volume <= 10
volume := 11
sets volume to 11, despite the fact the where clauses suggests volume is intended to be between 0 and 10. where clauses apply only in places where a variable gets an arbitrary value; by not applying them at assignment statements, Boogie provides the ability to use a sequence of statement that (perhaps temporarily) violates where conditions
Sep 19, 2014 at 2:49 PM
Ahh, thanks Dan. And I now see some more documentation in section 9.4 about havoc. It seems like where is what I need to use, and also some assumes after each assignment.