Each of the problems here asks you to develop one or more methods/predicates in the Dafny programming language. Of course, the intent is for you to make use of the Dafny software tool for the purpose of verifying correctness. For grading purposes, I will subject your code to analysis by that tool.
Please put your code into a file named HW6_Smith.dfy, replacing "Smith" by your name, and submit it to the HW#6 dropbox in Brightspace.
1. During a recent lecture, we developed the Dafny code shown below, which is included in a .dfy file accessible to you via a Brightspace "content module" (titled "Some Dafny Code"). In order to make the code shown here display properly while also being amenable to copy-and-paste operations, what would normally appear as array<int> instead is shown as array< int > (with unnecessary spaces). You are encouraged to remove those spaces in your code.
/* Yields true iff 'val' is the maximum value in b[low..high)
*/
ghost predicate isMaxInArraySeg(b: array< int >, low: nat, high: nat, val: int)
reads b
requires 0 <= low <= high <= b.Length
{
(forall j | low <= j < high :: b[j] <= val) &&
(exists j | low <= j < high :: b[j] == val)
}
/* Returns the maximum value in the given array (in the output
** variable 'biggest').
*/
method ComputeArrayMax(b: array< int >) returns (biggest: int)
requires b.Length != 0
ensures isMaxInArraySeg(b, 0, b.Length, biggest)
// Alternatively, we could avoid using the isMaxInArraySeg()
// function by including the two "ensures" clauses below.
//ensures forall j | 0 <= j < b.Length :: b[j] <= biggest
//ensures exists j | 0 <= j < b.Length :: biggest == b[j]
{
var k: nat := 1;
biggest := b[0];
while k != b.Length
decreases b.Length - k
invariant 1 <= k <= b.Length
invariant isMaxInArraySeg(b, 0, k, biggest)
// Alternatively, we could use the two invariants below
// rather than using the isMaxInArraySeg() function
//invariant forall j | 0 <= j < k :: b[j] <= biggest
//invariant exists j | 0 <= j < k :: b[j] == biggest
{
if b[k] > biggest { biggest := b[k]; }
k := k+1;
}
}
|
Notice that the loop invariant was obtained from the postcondition by replacing the constant b.Length by the fresh variable k. (Of course, the loop guard was chosen so that the loop would terminate when the two were equal.)
Develop a modified version of the ComputeArrayMax() method (you can rename it if you like) so that instead the loop invariant is obtained from the postcondition by replacing constant 0 by fresh variable k.
2. Develop a modified version of the ComputeArrayMax() method (either the one given or the one you developed for Problem #1) that returns not only the maximum element in the given array but also its minimum element. The method's heading, along with its precondition and postcondition, should be
/* Returns the minimum and maximum values in the given array ** (in the output variables 'smallest' and 'biggest'). */ method ComputeArrayMinMax(b: array< int >) returns (smallest: int, biggest: int) requires b.Length != 0 ensures isMinInArraySeg(b, 0, b.Length, smallest) ensures isMaxInArraySeg(b, 0, b.Length, biggest) |
For this to work you must supply an isMinInArraySeg() predicate (which should be very easy, given that you have the analogous isMaxInArraySeg()).
3. Develop a modified version of the ComputeArrayMax() method that returns the lowest-numbered index/location at which the maximum value occurs (as opposed to the maximum value itself). Here is its specification:
/* Returns the lowest-numbered location/index in the given array ** containing the array's maximum value. */ method ComputeIndexOfMax(b: array< int >) returns (locOfMax: nat) requires b.Length != 0 ensures 0 <= locOfMax < b.Length ensures isMaxInArraySeg(b, 0, b.Length, b[locOfMax]) ensures forall j | 0 <= j < locOfMax :: b[j] < b[locOfMax] |
If you wish, you can replace the last two conjuncts in the given postcondition by referring to a predicate isIndexOfMax() that yields true in response to the application isIndexOfMax(b,k) precisely when b[k] is at least as big as every element in b[] and strictly larger than every element in b[0..k). (Such a predicate need not refer to the isMaxInArraySeg() predicate, although it could.)
4. Here are Dafny functions numOccurrencesInSeg() and numOccurrencesIn():
/* Yields the number of occurrences of 'key' within array segment b[low..high).
*/
ghost function numOccurrencesInSeg(b: array< int >, low: nat, high: nat, key: int): nat
reads b
requires low <= high <= b.Length
decreases high-low
{
if low == high then 0
else numOccurrencesInSeg(b,low,high-1,key) + (if b[high-1] == key then 1 else 0)
}
/* Yields the number of occurrences of 'key' within array b[].
*/
ghost function numOccurrencesIn(b: array< int >, key: int): nat
reads b
{
numOccurrencesInSeg(b, 0, b.Length, key)
}
|
Complete the development of the method having this specification:
/* Returns the number of occurrences of 'key' within b[]. */ method ComputeNumOccurrencesIn(b: array< int >, key: int) returns (count: nat) ensures count == numOccurrencesIn(b, key) |
5. (Challenging) Develop the method with this specification:
/* Returns the length of the shortest prefix of b[] containing k ** occurrences of 'key', or b.Length+1 if there are fewer than k ** occurrences of 'key' in b[]. For example if k == 4 and the ** 4th occurrence of 'key' is at b[25], then the value returned ** should be 26. */ method ComputeLenOfShortestPrefix (b: array< int >, k: nat, key: int) returns (length: nat) requires k > 0 ensures 1 <= length <= b.Length+1 ensures length == b.Length+1 ==> numOccurrencesIn(b,key) < k ensures 1 <= length <= b.Length ==> b[length-1] == key && numOccurrencesInSeg(b,0,length,key) == k |