Description
Maximum tail sum problem
Problem 1 (30 points)
An implementation of a special case of a search routine with the precondition and postcondition encoded is
given in the file search.dfy accompanying this assignment. Give a proof of correctness in Dafny for this
search routine. Do not change the preconditions or postconditions. Only add annotations to the body of
the method.
Problem 2 (40 points)
The accompanying Dafny code mts.dfy gives an implementation of the maximum tail sum problem. That
is, given an array a of integers (both positive and negative values), it returns the sum of the maximum array
interval beginning anywhere and ending at the end of the array. If all such sums are empty, it return 0 to
reflect that an empty array interval (with a sum of 0) is optimal.
This program is something that is known
as a programming pearl. It is easy to implement this function in quadratic time, by enumerating all such
intervals and computing their sums. But, this code is doing it in a single pass linear time. Your task is to
prove that it does it correctly.
For grading purposes, we divide the full functional specification into two parts:
(a) (20 points) Prove that the first postcondition labeled as (a) in the file.
(b) (20 points) Prove the postcondition labeled as (b) in the file.
Problem 3 (40 points)
Consider the following game single player game. Initially, you are given a single stack of n boxes. In each
turn of the game, you must perform exactly one of two moves:
1. Pick a stack of a + b boxes and split it into two non-empty stacks of a and b boxes (i.e. a, b > 0). This
move scores a × b points.
2. Pick a stack containing only one box and remove it. This actions scores no points.
The game is finished when no more moves are possible. No matter what moves you make, you will eventually
run out of turns, and somewhat surprisingly, you will always finish the game scoring exactly n(n−1)
2
points.
Try out a few runs of the game for some specific games to observe this.
Your task is to prove this outcome for the game. A Dafny encoding of the game is given in the accompanying file stacking.dfy. The program is simulating the game. Add the annotations necessary to prove
to Dafny that the program (hence the game) terminates and that the postcondition holds. For grading
purposes, we divide this assignment into the following two tasks:
Note: Dafny currently complains about line 14 of the code. This is intentional. You need to add a loop
invariant that makes this complaint go away, and then be on your way about proving the problem correct.
(a) (20 points) Prove that the postcondition as specified in stacking.dfy and outlined above holds.
(b) (20 points) Prove that the loop terminates by providing the appropriate decreases clause for the
loop and any argument that may be required to support it so that Dafny has no complaints about
termination.
Problem 4 (30 points)
This problem is based on a known puzzle, “catch a spy”.
A spy is located somewhere on a one-dimensional line, and he moves. He starts at location a. Every
second, he moves b units to the right. Therefore, the location of the spy at time t is given by the expression
a + t ∗ b. But, the catch is that a, b ∈ N are constants that are unknown to us. We can only know check if
the spy is at a particular location by querying that location, and we can only query one location at every
second.
We can catch the spy as follows. The set N × N of pairs of natural numbers is countable 1
. Therefore,
there exists a function unpair : N → N × N that covers all pairs of natural numbers.
Our strategy is to check the location x + t × y at time t, where (x, y) = unpair (t). There exists some t0
such that (a, b) = unpair (t0). This means that at time t0 we will check the location a + t0 ∗ b, where the spy
shall be at time t0 as well! Therefore, we are guaranteed to catch the spy.
Now, you take the high level argument above and the sketch of an implementation that is given to you in
file spy.dfy and turn it into a complete formal argument in Dafny. Complete the implementation of method
unpair according to our strategy above, and prove that the while loop terminates (i.e. that we eventually
catch the spy).
Hint: You should think about defining unpair recursively, instead of as a closed form function.
Note: The purpose is for us to practice using a theorem prover, like Dafny, to do a formal proof that is
not related to a program. The puzzle and its solution are effectively provided to you (and you may consult
resources online for this as well). We are not asking you to find a solution for the puzzle. We are only asking
you to use Dafny to formally prove that the provided solution for the puzzle is indeed correct.
1
If you do not know what countable means, then look it up.
3
