Assignment 5: Verification with Dafny

Due Sunday, December 16 at 11:59 PM

Goals for This Assignment

By the time you have completed this work, you should be able to:

• Prove given implementations correct with Dafny

Step-by-Step Instructions

Step 1: Prove Factorial Correct

Download the template code here. This code contains a recursive factorial function method, which has been proven correct. This code also contains a factorial_iterative method, which computes factorial via a loop.

factorial_iterative has a postcondition which expresses that it behaves the same as factorial. While the implementation is correct, Dafny is unable to prove that the implementation satisfies the postcondition fully automatically. For this part of the assignment, you'll need to add loop invariants nad possibly assertions to prove the code correct. You should not change the preconditions, postconditions, or signature of factorial_iterative or factorial. If you wish, you can change the implementation.

Hints

• When adding loop invariants, you intuitively want to say that each iteration gets you closer to the postcondition you're trying to satisfy. For factorial, this means that each iteration gets you closer to showing that result == factorial(n).
• Unlike the version of factorial we worked on in class, this version specifically starts with a low number and then goes high. Related to the prior point, this enables you to effectively start with a statement like “the factorial of this low number is equal to my result so far”, and then incrementally increase this number until you're at the end target of n.

• Loop invariants must hold for the entirety of loop execution. This can occasionally lead to surprises, for example:

  method blah() {
    var index := 0;
    var top := 10;
    while (index < top)
      invariant index < top; // does NOT hold
    {
      index := index + 1;
    }
  }
  

  Counterintuitively, index < top is not a loop invariant, despite the guard of the loop. To understand why, consider the last iteration of the loop. There is a brief instant where index == top after the increment to index is performed, but before we check the index < top condition. As such, index <= top is a valid invariant, but not index < top. If you specifically want to talk about invariants that hold while the loop will continue executing, you can use an implication on the invariant, like so: invariant index < top ==> desired_property.

• It is possible to prove this correct using only two loop invariants.
• assert statements are a great way to debug your proofs, and they similarly can become part of the proof. You can start by asserting something you really want to prove, but may not know how (e.g., a postcondition). If Dafny can prove it, great! If not, you can then add further assertions and invariants before the assertion, which attempt to prove simpler things. This process will usually go in one of four directions, which aren't necessarily mutually-exclusive:
  1. You assert something that is simple enough that you know how to prove it, but Dafny still can't prove it. This usually means there is some additional information you know about your problem, but Dafny doesn't know it. It might even be information that is implied by information you provided. Adding the extra information will usually fix the problem.
  2. Occasionally, you'll assert just the right sequence of things, and suddenly verification as a whole succeeds. In this case, you've effectively held Dafny's hand while it tried to prove something, and incrementally worked from simpler to harder proofs. In this situation, it can be nice to refactor the proof to turn some assert statements into invariant statements, though we won't require this.
  3. You assert something that Dafny cannot prove, but it makes other errors go away. This is an artifact of how Dafny works when errors occur. Dafny will first fail to prove the assertion, giving you the error. However, Dafny will then do a sort of hypothetical reasoning, asking “what would happen if this assertion is true?”. If other errors go away, it means that while Dafny cannot prove the assertion, it can show that if the assertion is true, then everything else follows from it. This can lead to a reprioritization of efforts (I really just need to prove this assertion, and then everything else comes for free).

  4. You hit a wall. Dafny is unable to prove even the simplest of things, and you can't make progress on the proof. This usually means there is a deeper problem with your proof, perhaps even in your implementation. For example, when showing factorial in class, the implementation initially started with a high number, and then incrementally went to a low number. This made it impossible to satisfy the idea of “getting closer to the postcondition on each iteration”, since we were trying to prove equivalence to an implementation that started with a low number and then went high. In this situation, it can be required to provide a different implementation, or to otherwise add a signficiant amount of extra code to walk Dafny through the code.

     By giving you an implementation which I know can be proven with minimal additional invariants and assertions, I'm intentionally trying to keep you from completely hitting a wall. If you get stuck, let me know, and we can go through it together.

Step 2: Prove Array Splicing Correct

Download the template code here. This code contains a splice_in method, which is used to stitch one array into another, returning the result. Like the previous step, the implementation you've been provided is correct, though Dafny cannot automatically prove it. You'll need to add in invariant and assert statements to get this code working. You may change the implementation if you desire, but you may not change the signature of splice_in, or the preconditions and postconditions of splice_in.

Recommended Approach

Many of the hints in the prior step are applicable here. The provided implementation can be divided into three parts:

1. Copy elements from a until index into the result array.
2. Copy the contents of add_these into the result array.
3. Copy the remaining elements in a into the result array.

Each one of these parts has its own corresponding postcondition on splice_in. With this in mind, there are two major things you need to do for each of the three parts:

1. Show that the given part satisfies its given postcondition. You'll need to show that the part's loop incrementally gets closer to the part's postcondition. It's recommended to put an assert statement immediately after the part which simply asserts the corresponding postcondition, which will give you a quick indication of whether or not you've actually satisfied the postcondition (this assertion will be true if you satisfied the postcondition, and it will be false if you didn't).
2. Show that the given part doesn't jeopardize the postconditions from any previous parts. Related to the previous point, you should start with assert statements which merely repeat the other postconditions. If these fail, you'll need to provide Dafny further information that you haven't broken another postcondition. You may need to add prior proven postconditions as loop invariants later (i.e., it's invariant that this loop doesn't break a previously-proven postcondition.

Step 3: Submit Everything

Submit your factorial.dfy and splice.dfy files to the corresponding box on Canvas. In the comments for the submission, list everyone you worked with, if applicable.