Where program skeletons are shown, on the left is one expressed in Dijkstra's notation and on the right is one expressed (as far as possible) in Dafny.
1. (Recursive Function Evaluation)
Define function h : ℕ ⟶ ℤ as follows:
h(0) = 0, h(1) = 1, and
h(n+2) = h(n) - h(n+1) (for n≥0).
You should find the sequence ⟨h(0), h(1), h(2), ...⟩ to be an interesting variation of a familiar sequence.
Derive a solution (and provide an accompanying narrative) to the following programming problem. Not surprisingly, your program should include a loop, the invariant of which you should derive by employing the usual heuristics. During development, you should find it useful to strengthen the loop invariant by introducing a fresh variable.
Notice that the precondition says N>0. Try to weaken that to N≥0 without having to make your program more complicated (e.g., by using an if-else statement to treat N = 0 as a special case). Explain how you did it.
|
|
2. Derive a solution (and provide an accompanying narrative) to the following problem:
|[ con b : array of int; {{ #b > 0 }}
var r : int;
r := ?
{{Q: r = (#k | 0≤k<#b : S(k) × S(k+1) < 0)}}
]|
|
method ComputeNumSignChanges(b: array<int>)
returns (r: nat)
requires b.Length > 0
ensures r == (#k | 0≤k<b.Length : S(k) × S(k+1) < 0)
//Note that the line above is not legal Dafny
{
}
|
where S(k) = (+i | 0≤i<k : b[i]) is the sum of the elements in the segment b[0..k). Thus, the program computes the number of times that S(k) changes sign as k goes from 1 to #b. The expression S(k) × S(k+1) < 0 is equivalent to the less concise, but perhaps more helpful
The solution to the Negative-Positive Array Element Pair Counting problem (see relevant web page) may by helpful.
Recall that splitting off a term from a counting quantification works like this:
(+k | 0≤k<n+1 : Z) = < (8.23) (and assumption n≥0 guaranteeing a non-empty range) > (+k | 0≤k<n : Z) + if(Z[k:=n], 1, 0) |
Note: If the problem, as given, proves to be too difficult, try doing it with this different postcondition:
3. Derive a solution (and provide an accompanying narrative) to the following programming problem:
|
|
The methods used in deriving the program for the Maximum Segment Sum problem (see relevant web page) will be useful here. In particular, notice the step in the derivation of E in which either (8.16) or (8.18) (two versions of range split) is applied, followed by the (combined) step in which (8.20), (8.14), and (8.20) (again) are applied.
Also note that subtraction distributes over min in a particular way, producing a max. Specifically,
In terms of quantification, this can be stated as
Theorem (Subtraction Distributes over min to produce max):
Provided that x does not occur free in U, U - (MIN x | R : V) = (MAX x | R : U - V)
4. Consider this tail recursive definition of the (two-argument) function H : ℕ × ℕ → ℕ (where ℕ denotes the set of nonnegative integers):
| H(m,n) = { | n | if m = 0 |
| H(m−1, 2n) | otherwise (i.e., m ≠ 0) |
Using this definition, follow the standard procedure (as covered in lecture and on web page) by which to derive a program that satisfies the specification below (in which M and N are the inputs). (Make sure that your program is appropriately annotated to include a loop invariant and bound function.) That M and N are declared to be of type nat means that M≥0 ∧ N≥0 is an implicit precondition.
|
|
5. Consider this pseudo-tail recursive function definition, which describes a function having signature ℕ ⟶ ℕ
| G(n) = | { | 0 | if n = 0 |
| n + G(n−1) | otherwise (i.e., n ≠ 0) |
From this definition, use the procedure covered in class by which to derive a program that computes the function. That is, complete the program specified below, in which N is to be interpreted as being the input. (Make sure that your program is appropriately annotated to include a loop invariant and bound function.)
As an intermediate step, you could derive from the pseudo-tail recursive definition of G a (fully) tail recursive definition for function G' such that (for every positive integer n) G'(n,e) = G(n), where e is the appropriate identity element.
|
|