Boogie documentation WhereClause

Oct 30, 2012 at 2:55 PM


In the document "This is Boogie 2", I think that the grammar at the end refers to (in IdsTypeWhere) but does not define WhereClause. What should it be?



Oct 30, 2012 at 6:46 PM

Good eye.  It was accidentally omitted from the document.  It is defined as:

WhereClause ::= "where" Expr


PS.  The "This is Boogie 2" manual also talks about "finite" types.  That was the initial design, but the "finite" keyword is neither needed nor allowed.  That is, you can declare a finite type without that keyword (but all types do need to be nonempty).