Dafny: what is "predicate" ?

Oct 1, 2012 at 10:43 AM

As I understand "predicate" is not the same as а "function which returns bool". F.e., Dafny is agreed with the following program: http://rise4fun.com/Dafny/LEIl which has a predicate and its refinement, has a method "f" and its refinement (which is equal to the initial version of "f", as I understand). But M2.f doesn't satisfied a contract of M1.f (because of difference between M1.V and M2.V). But Dafny says "all verified". As I understand M2.f shouldn't be correct in this program. Where am I wrong?

Coordinator
Oct 1, 2012 at 6:19 PM

Hi Eugene,

Except for two things, a predicate is indeed just a function that returns a boolean.

One difference is that, syntactically, parameter-less predicates don't need to use the parentheses.  I'd like to change that to require the parentheses even for such predicates.  The reason for this is that I would like to support passing functions as arguments, and I think the most natural syntax would then be to just name the function/predicate.  I'd be interested in hearing opinions about if allowing parentheses-less calls are a good idea.

The other difference relates to refinement.  A refining module is not allowed to change the body of a function in any way.  (Well, it's allowed to supply the function body if the function did not have a body at all in the refined module.)  In contrast, a predicate body is allowed to be changed in a refining module.  However, the effect of this is not to replace the body of the predicate, but to strengthen it.  (Currently, there is no syntactic indication that this is what's going on.  Of course, some documentation could cure that...)

So, in your example, the effective body of M2.V() is:

x < 200 &&
x > 10

And with that, Dafny does the right thing to verify your program.

By the way, although you don't see it from the outside, Dafny tries its hardest to avoid re-verifying things in a refining module.  So, in your example, when Dafny verifies M1.f(), it will check the postcondition x < 200.  When it verifies M2.f(), it will not re-check the postcondition x < 200, since that has already been checked in M1.  Instead, for M2.f(), Dafny will only verify the new postcondition x > 10.

  Rustan

Oct 2, 2012 at 12:07 AM

Oh, cool! Thanks, Rustan! I think parentheses-less calls are a good idea really because it could be seen as a property of the state (getter without setter).