Encapsulating array access

Oct 13, 2012 at 5:29 AM
Edited Oct 13, 2012 at 5:30 AM


I have a question of how to correctly encapsulate array access in Dafny classes.

This is a question related to http://boogie.codeplex.com/discussions/397325 . Thanks everyone in that discussion, but I appreciate if you can teach me a little bit more.

Here is an example program which Dafny complains about the modifies clause:


The discussion in http://boogie.codeplex.com/discussions/397325 suggests I should either (1) propagate the modifies clause of Add() for all callers, or (2) use dynamic frames to encapsulate it.

I looked through the test cases of Dafny a little bit but unfortunately I can't find an example. :-(

I appreciate if you help me out.

Thanks very much!

Oct 13, 2012 at 10:47 PM

It seems you still have trouble with modifies clauses.  One way out is to follow the standard dynamic-frames idiom.  But it would still be a good idea to understand what's going on.

In the example you gave, the immediate problem is pretty basic:  Method Test(), which has an empty modifies clause, is calling holder.Add(), whose modifies clause instantiates to holder, holder.Items.  In other words, Test() has no permission to modify anything, yet it's calling a method that may modify something.  To solve this particular problem, you could add a "modifies holder, holder.Items;" to Test().  To debug a situation like this, look at the caller's modifies and the callee's modifies clause and see if the latter is indeed a subset of the former.

Even with "modifies holder, holder.Items;" on Test(), your specifications will be insufficient to verify other interesting uses of class AHolder.  For example, if you let Test() call holder.Add(a); twice in a row, you will have a problem with the modifies clause of the second call.  This problem comes from the fact that AHolder.Add may change Items to point to a different array (the caller knows this because Add's modifies clause includes "Items"), but the caller of AHolder.Add may not have permission to change the state of the Items array that is being pointed to after the call to Add.  Thus, an attempt to make a second call to Add fails.  To solve this problem, you have to strengthen the postcondition of Add with something like:

Items == old(Items) || fresh(Items)

Note that "Items" is mentioned in the specifications of AHolder.  That suggests that clients of AHolder need to know about "Items"--it is not a private implementation decision.  Perhaps that's how you want it.  If so, then you're done.

If you also want to encapsulate the array, then follow the standard dynamic-frames idiom.  Here's a complete example that illustrates it:  http://rise4fun.com/Dafny/JOFU