Dafny: "implicit let"

Dec 14, 2012 at 2:10 PM
Edited Dec 14, 2012 at 2:10 PM

I study ":|" statement. I wonder why predicate of this statement isn't treated as specification context (because it is a predicate, like assertion). F.e., in this program: http://rise4fun.com/Dafny/aGEV .

Dec 17, 2012 at 11:10 PM
Edited Dec 17, 2012 at 11:11 PM

Hi Kornevgen,

I come across a similar construct in the EventB language. It is called 'becomes such that substitution(i.e., assignment)', which is essentially a non-deterministic assignment. the grammar look like the following:

   ids :| predicates

which convincing the verifier of a fact:

   the value being assigned to 'ids' hold on the 'predicates'.

'Become such that assignment' is useful in refinement. You can use it to assign an abstract value to the variable, then in the later refinement, use a concrete assignment to describe how such value can be found. 

I would say the dafny program you gave also fit this refinement paradigm. 


Dec 18, 2012 at 7:26 AM

Hi, Zheng! Thank you for your reply. But my question was concerned with some technical details about implementation ":|" construct in Dafny. Do you know why "predicates" of this construction aren't treated as specification context ?