PVS assignments

After the choice of one of these assignments, first design an
algorithm with a complete hand-written proof. Only then, encode the
algorithm in PVS. Prove the correctness of your program with the
theory programs.pvs unless otherwise specified. Write a report about
the algorithm and your proof of it, and turn it in on paper. Also,
send a dump-file of the pvs proof to w.h.hesselink@rug.nl.

The assignments A, ..., E are presented in order of increasing
complexity. Their solutions should have linear complexity. The other
assignments have been added later in arbitrary order. The assignments
O, P, R, S, T, and U are relatively easy (and you can always ask for
assistance).

Most of the following assignments suppose that you use and import the
theory programs, and that you apply the ideas of the course in program
correctness as in binsearch.pvs. Exceptions are the assignments M, N, V.

-.-.-

Assignment A. Given are three ascending (weakly increasing) functions 
f, g, h: natural -> real, such that there exists a triple of natural 
numbers x, y, z with f(x) = g(y) = h(z). Write a program to determine 
such a triple (the first one). 
Time complexity: linear in x+y+z. 

Assignment B. Merge. Given are two ascending (i.e. weakly increasing)
arrays f and g of real numbers, say with lengths k and n. The state
space holds a variable h for an array with length k+n. The program
should fill array h with the elements of f and g in such a way that h
is also ascending. Also show that the contents of h as a set is the
union of the (initial) contents of f and g.  Time complexity: linear
in k+n.

Assignment C. Plateau. Given is one nonempty array f. A plateau of f
is a sequence of consecutive elements of f with the same value. The
program should determine the length of the longest plateau of f, as
well as an index where such a longest plateau starts.  Time complexity
linear in the size of f.

Assignment D. Dutch National Flag. Given is an array f of length N of
real numbers. Develop and prove a program that permutes the elements
of array f and yields two integers a and b such that, for all i with 0
<= i < N, we have f(i) < 0 if and only if i < a, and f(i) < 1 if and
only if i < b.  Also compute the permutation p with f = F o p where F
is the initial value of f. The time complexity must be linear in
N. It is allowed to swap array elements in one statement.

Assignment E. Incidence counting. Given are two increasing arrays f
and g of real numbers, say with lengths k and n. The program should
determine the number of pairs (i,j) with f(i) = g(j).  Time
complexity: linear in k+n.

Assignment F. Selection sort is a well-known in-situ sorting algorithm
of quadratic complexity. Prove its correctness, i.e., prove that the
program does not change the contents of the array (as a multiset), but
sorts it by changing the order of the elements. Note that the program
has a double loop.  First invent the invariant of the outer loop, then
the invariant of the inner loop, but note that the inner loop must
preserve the invariant of the outer loop also.

Assignment G. Let f be a function [nat, nat -> real] that is ascending 
in its first argument and descending in its second argument, and that is
0 some some unknown pair of arguments. Develop a program that determines 
a pair (i, j) such that f(i, j) = 0 and that we have i <= x and j <= y for 
all x, y with f(x, y) = 0. In this case, the invariant and the variant 
function may depend on the unknown existing pair. 

Assignment H.  Figure Six. Let T be a finite type and let x0: T and f:
[T->T] be given.  We use f^n to denote n-times repeated application of
f. Put N = card[fullset(T)], based on the definition of Card in the
prelude, and prove that there exist i < j <= N such that f^i(x0) =
f^j(x0). Give a while program to determine a pair i and j with i < j
and f^i(x0) = f^j(x0), and prove its correctness. The program must use
bounded memory (no arbitrarily large sets). It must not use the
unknown value of N, and also no auxiliary function for f^n.

Assignment I.  Slope search. Given are natural numbers m and n, a real
number w, and a function f: [nat, nat -> real], which is descending in
its first argument and increasing in its second argument. Design a
program to determine the set
   {(x,y): [nat, nat] | x < m & y < n & f(x,y) = w } .
The time complexity must be in the order of m+n.
You can use a program variable of type setof[[nat, nat]] and the prelude 
function add. 

Assignment J.  Floyd_Warshall. Let n be a positive natural number and
let R be a binary relation on below[n]. Floyd-Warshall's algorithm
determines the reflexive transitive closure star(R), in order n^3,
with a triply nested loop. Prove its correctness. Note that an inner
loop should preserve the invariant of any surounding loop.

Assignment K.  Graph search. Let R be a binary relation over a finite
nonempty type T, interpreted as a directed graph. Let x0: T be a given
vertex. Graph search is the common generalization of depth-first and
breadth-first dearch. The aim is to form a subrelation F of R, which
is a tree rooted at x0 that contains all nodes reachable from x0. The
algorithm uses a node x, and two sets of nodes: S, the wave front, and
U, the set of the unreached nodes.
  S := {x0} ; 
  U := T - {x0} ;
  F := empty ;
  while S is not empty do 
    extract some x from S ;
    W := {y in U | (x,y) in R} ;
    U := U - W ;
    S := S union W ;
    F := F union {(x,y) | y in W} ;
  end .
Formalize the postcondition sketched above. Prove that the algorithm
terminates and establishes this formalized postcondition.  From the
prelude, you will need is_finite to prove termination, and epsilon to
choose some element.  Comment. If S is treated as a stack, you get
depth-first search; if it is treated as a queue, you get breadth-first
search. If you would give the edges nonnegative weights and would
attach variable weights to the reached nodes, you could get Dijkstra's
shortest path algorithm (F can then be omitted).

Assignment L.  Tarjan's union algorithm. Let R: pred[[T,T]] be
finite. The aim of the union algorithm is to determine the smallest
equivalence relation E that contains R. It does so by means of a
program variable (an array of pointers)
   parent: [T -> lift[T]],
which must satisfy something like: forall x: exists n: parent^n(x) =
bottom.  Let this property be called toBottom. Construct a function
   ancestor: [T, (toBottom) -> T]
that satisfies
   ancestor(x, p) = IF up?(p(x)) THEN ancestor(down(p(x)), p) ELSE x ENDIF .
Now the algorithm should have the postcondition
   E = {(x,y) | ancestor(x, parent) = ancestor(y, parent) } .
It has the form:
   {PRE: forall x: parent(x) = bottom }
   while R is not empty do
      extract some pair (x,y) from R ;
      x := ancestor (x, parent) ; 
      y := ancestor (y, parent) ; 
      parent(x) := y OR parent(y) := x ; // not both!
   end .
Prove its correctness. 

Assignment M.  Merge-sort. Define merge-sort as a functional program
in Haskell and prove its correctness. Do not use the theory
"programs". Use finite sequences from the prelude. The correctness
should include that, for every value w, the number of occurrences of w
in the initial list equals the number of occurrences in the sorted
list. And, of course, the sorted list must be sorted.

Assignment N.  Search trees. Use a data type to define search
trees. Define and prove the correctness of the recursive function
"search", and of the function "insert". Now define AVL-trees and the
insert function for AVL-trees, and prove its correctness. Do not use
the theory "programs".

Assignment O.  The king's problem. There are N persons at a meeting,
numbered 0 through N-1.  One of them is the king, with an unknown
number X. Everybody (possibly except for the king) knows the king, but
the king knows nobody (except possibly himself). Predicate knows(i,j)
expresses that person i knows person j. So, it is given that 0 <= x <
N and that, for all i /= X, we have knows(i,X) and not knows(X,i).
Design a program with linear time complexity that determines X. Use
the theory "programs" to prove the correctness.

Assignment P. Given is a natural number N and for every natural number
i < N a set children(i), which consists of natural numbers < i. A
descendant of i is defined to be a child of i or a descendant of a
child of i. Give a recursive definition for a function descendants(i)
that formalizes this and that is accepted by PVS. Design a sequential
algorithm that determines descendants(i) for all i < N. The time
complexity of the algorithm should be proportional to N if set-union
can be done in constant time (here set-union stands both for the
binary operation and for the union of a set of sets of numbers).  Use
the theory "programs" to prove the correctness.

Assignment R. In the decimal system, a natural number n is represented
by a finite sequence s of digits (numbers < B) such that n = (sum i:
s(i)*B^i) where the base B = 10. At school we have learned to add two
numbers given in this representation by repeatedly adding digits in
the same position modulo B and transferring the carry to the next
position. Formulate this recipe as a while loop and prove that the
value represented by the resulting sequence equals the sum of the two
values of the argument sequences. Note that the "digits" s(i) must be
in the range 0 \leq s(i) < B, both for the summands and for the
resulting sum.  Do this for an arbitrary base B > 1.  You may use the
theory sum in the user guide and the finite_sequences in the
pvs-prelude. You will have to develop some elementary arithmetic.  Use
the theory "programs" to prove the correctness.

Assignment S. The value of a polynomial expression 
   S = (sum i: i < n : a(i)*m^i)
for a real argument m can be calculated by
   s := 0 ; k := n-1 ;
   while k >= 0 do s := s * m + a(k) ; k := k-1 ; end .
Prove the correctness using the theory "programs". The hint and remark
in the previous assignment are applicable here as well.

Assignment T. We consider finite sets of integers. Such a set is
represented by an increasing array of integers with some length.
Given are such sets X and Y, an integer m, and a boolean function p:
int * int -> bool. Construct a program to determine the subset Z of X
of the elements x in X such that m+x is in Y and that p(m, x) holds. Z
must again be represented as an increasing array. The time complexity
of the program must be linear in #X+#Y (where # means "number of
elements of"). [NB. Binary search in Y per element of X has complexity 
(#X)*log(#Y) and is therefore not efficient enough]

Assignment U. We use the same setting as assignment T. Construct a
program to determine the subset Z of X of the elements x in X such
that there is an element y in Y for which x+y = m and p(x, y) holds. Z
must again be represented as an increasing array. The time complexity
of the program must again be linear in #X+#Y (where # means "number of
elements of").

Assignment V. The mutual exclusion algorithm of Burns-Lamport for N 
concurrent threads. It uses a single shared variable:
bool cc[N] ; // initially all false

thread(p: 0 <= p < N) {
    int j ; // private
    while (true) {
10:     NCS ;
11:     cc[p] := true ;
12:     for (j := 0 ; j < p ; j++) {
13:         if (cc[j]) {
14:             cc[p] := false ;
15:             await ! cc[j] ; goto 11 ;
            }
        }
16:     for (j := p+1 ; j < N ; j++) {
            await ! cc[j] ;
        }
17:     CS ;
18:     cc[p] := false ;
    }
}
To prove: mutual exclusion: q at CS and r at CS implies q = r.
Optionally: prove progress in the form 
    box((exists q in [11..17]) implies diamond(exists r at CS)).
You may use weak fairness to prove this. 

Version 18 November 2010, Wim H. Hesselink