Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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. Show that the contents of h as a multiset 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 real numbers and an integer valued function g on the reals. The program should permute the elements of the array such that all elements x = f(i) of the array with g(x) < 0 to the left, all elements x of the array with g(x) > 0 to the right, and all elements x with g(x) = 0 in between. The program also yields the indices separating the three subranges. It is allowed to swap array elements in one statement. Show that the contents of the array as a multiset is unchanged. Time complexity linear: in the size of the array. 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. Use the definition of Card in the prelude to prove that there exist i < j <= card[fullset(T)] such that f^i(x0) = f^j(x0). Give a while program to determine some such pair i and j, for the given x0, and prove its correctness. 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 } . 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". PS. The first five of them are presented in order of increasing complexity. Their solutions should have linear complexity. Wim H. Hesselink