An intricate look at the Dafny reads and modifies concepts?

[lancejpollard]

In reading about reads and modifies, the essence of the docs (which is the same text used in multiple articles/references) is this:

The reading frame of a function (or predicate) is all the memory locations that the function is allowed to read. The reason we might limit what a function can read is so that when we write to memory, we can be sure that functions that did not read that part of memory have the same value they did before. For example, we might have two arrays, one of which we know is sorted. If we did not put a reads annotation on the sorted predicate, then when we modify the unsorted array, we cannot determine whether the other array stopped being sorted. While we might be able to give invariants to preserve it in this case, it gets even more complex when manipulating data structures. In this case, framing is essential to making the verification process feasible.... Dafny will check that you do not read any memory location that is not stated in the reading frame. This means that function calls within a function must have reading frames that are a subset of the calling function’s reading frame.... Methods are allowed to read whatever memory they like, but they are required to list which parts of memory they modify, with a modifies annotation.... In combination with reads, modification restrictions allow Dafny to prove properties of code that would otherwise be very difficult or impossible. reads and modifies are one of the tools that allow Dafny to work on one method at a time, because they restrict what would otherwise be arbitrary modifications of memory to something that Dafny can reason about.

So basically:

1. The reads frames say what memory you are allowed to access.
2. The modifies frames are what memory you can write to.
3. Framing is essential to making the verification process feasible.
4. The modifies allows Dafny to prove properties of code that would otherwise be very difficult or impossible.

So basically, it is for some reason necessary for proving properties of code. Why is it infeasible without them? What infeasible things do these make feasible? What properties are traditionally difficult/impossible to prove, and how does modifies solve them?

Also, how does this compare to other programming languages/concepts? How does it relate to, for example, Rust's immutable/mutable variable declarations, or the borrowing system?

I am having difficulty understanding the need for the reads and modifies frames idea, why it was necessary, what it is solving, and how it is solving the issues.

Thank you very much for the help.

[atomb]

Your summary is exactly right. The short and more general answer to your question, applicable to many verification tools, is that it's primarily for efficiency: to make a difficult problem feasible. Due to one of Dafny's key design decisions (also made for efficiency, of both human mental resources and computational resources), it turns out to be necessary in the Dafny case to make verification possible at all.

The key reason for this is that Dafny (like many similar tools) verifies each method independently. When analyzing the body of a method, Dafny assumes that the preconditions (requires clauses) hold before execution and tries to prove that the postconditions (ensures clauses) will therefore always hold after execution. When encountering a call to another method, Dafny ignores the actual implementation of that method. Instead, it attempts to prove that the precondition of the method being called is satisfied and then, if so, assumes that its postcondition holds when it returns.

This process interacts with memory in a somewhat complex way. Typically, an executing program has many objects in memory, only a few of which are of interest to any given method. It's important for program modularity that a single method can be called from many contexts, each of which may have different memory contents. The reads and modifies clauses indicate which parts of memory the method will access. From the point of view of verifying a calling method, this means that any portion of memory that has already been established to have certain properties before the called method executes, and that isn't mentioned in a modifies clause, will still have those properties after the method has been called. Without this, it might arbitrarily modify memory, which would make it almost impossible to prove anything after it returned.

The alternative to this would be to look inside the body of the called method to see what it actually does in the context of the specific caller being analyzed. That would require the verification process to consider much more code at once, and would require each method to be re-analyzed in every place where it gets called, which in practice is typically so expensive as to be infeasible.

Rust's type system is another approach at solving a similar problem in a more constrained context. Giving a reference parameter the mut annotation is essentially equivalent to putting it in a modifies clause. And Rust's type system is constrained enough that reads clauses are unnecessary because they're directly apparent from a type signature. Dafny has no concept equivalent to Rust's borrowing system, which has the consequence that Dafny programs will typically require a garbage collector at runtime.

[lancejpollard]

When a method has a modifies clause, what does the system do in relation to what it modifies? Does it need to know anything about how it is modified? If things can be modified in arbitrary ways, I don't see how saying modifies will accomplish anything. Maybe an example would help.

[atomb]

The key need for modifies comes from the fact that the postcondition of a method can be as precise or imprecise as desired, relative to what the code within actually does. When verifying the body of a method, modifications are only allowed to be made to variables listed in a modifies clause. When verifying code that calls that method, the verifier first assumes that any variable specified in the modifies clause for that method has some new, completely unknown value and then also assumes any ensures clause from the method, which may provide some information about the value of that variable.

As and example, consider a sorting method that makes in-place updates to an array a. You could give it the postcondition ensures a == ReferenceSortFunction(old(a)). In that case, you could make the case that a modifies a clause shouldn't be necessary because the specification says exactly what a will be. In practice, Dafny still does require a modifies clause here.

However, you could also give a looser specification, such as ensures Sorted(a), saying that, when the method returns, a will be sorted (but perhaps might have no relation to its initial value). In this case, it's not at all straightforward to say, just from looking at the specification, whether the method modifies a at all. Maybe something about the precondition of the sort method implies that a will be sorted when it returns, without needing to modify it.

You could imagine Dafny doing an analysis of the program in advance to figure out what methods modify what variables and inserting these modifies clauses automatically, so Dafny programmers wouldn't need to. However, it turns out that, in the general case, that sort of analysis is undecidable. Dafny could probably do it for you in many cases, but in practice it tends to be helpful to have it written down explicitly.