Two Dafny functions that may come in handy are these:
function MinOfTwo(x: int, y: int): int
{ if x < y then x else y }
|
function MaxOfTwo(x: int, y: int): int
{ if x > y then x else y }
|
ghost function h(n: int): int
{
if n < 2 then n else h(n-2) - h(n-1)
}
method Compute_h(N: nat) returns (y: int)
ensures y == h(N)
{
// to be completed
}
|
2. Here we revisit Problem 2 from HW #6. Complete the NumSignChanges() function and the ComputeNumSignChanges() method in Dafny (so that it verifies).
/* S(k) is the sum of the first k elements of array b[].
*/
ghost function S(b: array< int >, k: nat): int
reads b
requires k <= b.Length
{
if k == 0 then 0 else S(b, k-1) + b[k-1]
}
/* To use Gries/Schneider notation:
** NumSignChanges(b,n) = (#i | 1 <= i <= n : S(b,i-1) * S(b,i) < 0)
*/
ghost function NumSignChanges(b: array< int >, n: nat): nat
reads b
requires n <= b.Length
{
if n == 0 then 0
else 12345
// above line needs correction
}
method ComputeNumSignChanges(b: array< int >) returns (r: nat)
requires b.Length != 0
ensures r == NumSignChanges(b, b.Length)
{
// to be completed
}
|
3. Here we revisit Problem 3 from HW #6. This is the most difficult problem in this homework, in part because the translation between the postcondition as expressed as a MAX-quantification with two dummies (as in HW #6) and as expressed in terms that Dafny "understands" is nontrivial.
/* Returns (MAX p,q | 0 <= p <= q < b.Length :: b[q] - b[p])
*/
ghost function MaxDiff(b: array< int >): int
reads b
requires b.Length != 0
{
MaxDiffAux(b, b.Length)
}
/* Returns (MAX p,q | 0 <= p <= q < n :: b[q] - b[p])
*/
ghost function MaxDiffAux(b: array< int >, n: nat): int
reads b
requires b.Length != 0
requires 0 < n <= b.Length
{
-99 // to be completed
}
/* True iff b[q] - b[p] = (MAX i,j | 0 <= i <= j < b.Length : b[j] - b[i]).
** That is, the maximum difference between any two elements of b[], where the
** smaller occurs at a non-higher numbered location than the larger, is
** b[q] - b[p].
*/
ghost predicate AreMaxDiffLocs(b: array< int >, p: nat, q: nat)
reads b
requires b.Length != 0
requires p <= q < b.Length
{
AreMaxDiffLocsAux(b, p, q, b.Length)
}
* True iff b[q] - b[p] = (MAX i,j | 0 <= i <= j < n : b[j] - b[i]).
** That is, the maximum difference between any two elements of b[0..n),
** where the smaller occurs at a non-higher numbered location than the
** larger, is b[q] - b[p].
*/
ghost predicate AreMaxDiffLocsAux(b: array< int >, p: nat, q: nat, n: nat)
reads b
requires b.Length != 0
requires p <= q < n <= b.Length
{
forall i,j | 0 <= i <= j < n :: b[q] - b[p] >= b[j] - b[i]
}
* Lemma that draws a connection between the MaxDiffAux() function
** and the AreMaxDiffLocsAux() predicate.
** Supplying a proof would be outstanding.
** Making use of it as an axiom would be good, too, in order to
** verify the preferred postcondition of method below.
*/
lemma Lemma1(a: array< int >, p: nat, q: nat, n: nat)
requires a.Length != 0
requires p <= q < n <= a.Length
ensures AreMaxDiffLocsAux(a, p, q, n) <==> (a[q] - a[p] == MaxDiffAux(a, n))
method ComputeMaxDiffLocs(b: array< int >) returns (p: nat, q: nat)
requires b.Length != 0
ensures p <= q < b.Length
ensures b[q] - b[p] == MaxDiff(b)
// Postcondition on next line is preferred, but harder to verify. Try!
//ensures AreMaxDiffLocs(b, p, q)
{
// to be completed
}
|
4. Here we revisit Problem 4 from HW #6. Complete the ComputeH() method in Dafny (so that it verifies).
ghost function H(m: nat, n: nat): nat
{
if m == 0 then n else H(m-1, 2*n)
}
method ComputeH(M: nat, N: nat) returns (k: nat)
ensures k == H(M, N)
{
// to be completed
}
|
5. Here we revisit Problem 5 from HW #6. Complete the ComputeG() method in Dafny (so that it verifies).
ghost function G(n: nat): nat
{
if n == 0 then 0 else n + G(n-1)
}
method ComputeG(N: nat) returns (k: nat)
ensures k == G(N)
{
// to be completed
}
|
6. Here we revisit Problem 2 from HW #7. Complete the Prob_7_2() method in Dafny (so that it verifies). Notice that the specification uses expressions such as old(b[i]), which refers to whatever value occupied location i of array b[] when the method started. Be warned that the old() construct cannot be used in compilable code.
/* Modifies the given array so that each element (except for the last, which
** remains unchanged) is equal to the minimum of its original value and the
** original value of its successor.
*/
method Prob_7_2(b: array< int >)
modifies b
requires b.Length != 0
ensures forall i | 1 <= i < b.Length :: b[i-1] == MinOfTwo(old(b[i-1]), old(b[i]))
ensures b[b.Length-1] == old(b[b.Length-1])
{
// to be completed
}
|
As an alternative (or in addition), you are invited to complete the method Prob_7_2_WithSeq(). This version of the method makes use of a ghost parameter (rather than the old() construct) for the purpose of referring to the original contents of array b[]. (Notice that the precondition says that the ghost parameter bOrig must be equal to the sequence b[..].) Like the old() construct, a ghost parameter cannot be mentioned in a line of compilable code.
Regarding Dafny sequences: If b is of type array<T>, the expression b[lo..hi] is of type seq<T> and contains the same values as are in the indicated segment of array b. If lo is omitted (as in b[..hi]), zero is understood; if hi is omitted (as in b[lo..], b.Length is understood. The length of a sequence s is denoted by |s|. To refer to the i-th element of sequence s, use s[i], just as with an array.
method Prob_7_2_WithSeq(b: array< int >, ghost bOrig: seq< int >)
modifies b
requires b.Length != 0
requires bOrig == b[..]
ensures forall i | 1 <= i < b.Length :: b[i-1] == MinOfTwo(bOrig[i-1], bOrig[i])
ensures b[b.Length-1] == bOrig[b.Length-1]
{
// to be completed
}
|
7. Here we revisit Problem 3 from HW #7. Complete the Prob_7_3() method in Dafny (so that it verifies). As in the previous problem, Dafny's old() construct is employed. As an alternative (or in addition), you could verify a version of the method having a ghost parameter of type seq<int> (as in the previous problem).
/* Modifies the given array so that each element (except for the first,
** which remains unchanged) is equal to the difference between its
** original value and the original value of its predecessor.
*/
method Prob_7_3(b: array< int >)
modifies b
requires b.Length != 0
ensures forall i | 1 <= i < b.Length :: b[i] == old(b[i]) - old(b[i-1])
ensures b[0] == old(b[0])
{
// to be completed
}
|
8. Here we revisit Problem 4 from HW #7.
/* True iff the elements in a[low..high) are in ascending order.
*/
ghost predicate Ascending(a: array< int >, low: nat, high: nat)
reads a
requires low <= high <= a.Length
{
forall i,j | low <= i <= j < high :: a[i] <= a[j]
}
/* True iff every value in a[..p) is <= every value in a[p..]
*/
ghost predicate Boundary(a: array< int >, p: nat)
reads a
requires p <= a.Length
{
forall i,j | 0 <= i < p && p <= j < a.Length :: a[i] <= a[j]
}
/* Returns the index of a maximum element in a[low..high).
*/
method ComputeLocOfMax(a: array< int >, low: nat, high: nat) returns (k: nat)
requires low < high <= a.Length
ensures low <= k < high
ensures forall j | low <= j < high :: a[j] <= a[k]
{
// to be completed
}
/* Rearranges the elements of the given array so that they are
** in ascending order.
*/
method SelectionSort(b: array< int >, ghost bOrig: array< int >)
modifies b
requires b.Length == bOrig.Length
requires multiset(b[..]) == multiset(bOrig[..])
ensures Ascending(b, 0, b.Length)
ensures multiset(b[..]) == multiset(bOrig[..])
{
var m: nat := b.Length;
while m != 0
// loop invariant and bound function information missing
{
var k: nat := ComputeLocOfMax(b, 0, m);
b[k], b[m-1] := b[m-1], b[k];
m := m-1;
}
}
|