CSSE3100/7100 Reasoning about Programs
Week 6 Exercises
Exercise 6.1.
Below is the linear-search specification from the lecture slides that returns the first element satisfying P, and a.Length if there is no such value.
method LinearSearch2(a: array, P: T -> bool) returns (n: int)
ensures 0 <= n <= a.Length
ensures n == a.Length || P(a[n])
ensures forall i :: 0 <= i < n ==> ! P(a[i])
a) Write a linear-search specification for a method that returns the first element that satisfies P and uses a negative value (instead of a.Length) to signal that no element satisfies P.
b) Using the strategy for implementing linear search from the lectures, determine the loop invariant and state how it is derived from the postcondition of the loop. Depending on how you decide to implement the use of the value -1, the postcondition of the loop may be different to the postcondition of the method.
c) Write the code for the method and verify it is correct using the Dafny verifier.
Exercise 6.2.
Following a similar 3-step approach to Exercise 6.1, specify and implement a method to compute the maximum of an array of type array. Allow the array to be empty, and in that case return -1 as the maximum. Verify your method is correct using the Dafny verifier.
Exercise 6.3.
Binary search works on sorted arrays. Binary search begins by comparing an element in the middle of the array with the target value. If the target value matches the element, its position in the array is returned. If the target value is less than the element, the search continues in the lower half of the array. If the target value is greater than the element, the search continues in the upper half of the array. (Wikipedia)
a) What is the precondition required to complete the specification of the binary search method below in which key is the target value, and the method returns the “earliest insertion point”, i.e., the index of the leftmost occurrence of the key, if it exists in the array, or the index where to insert the key, if it’s not in the array.
method BinarySearch(a: array, key: int) returns (n: int)
requires ???
ensures 0 <= n <= a.Length
ensures forall i :: 0 <= i < n ==> a[i] < key
ensures forall i :: n <= i < a.Length ==> key <= a[i]
b) The following is an incomplete implementation of binary search. Calculate the
postcondition of the loop needed to apply the loop rule. Explain how each of the invariants is derived from this postcondition.
{
var lo, hi := 0, a.Length;
while lo < hi
invariant 0 <= lo <= hi <= a.Length
invariant forall i :: 0 <= i < lo ==> a[i] < key
invariant forall i :: hi <= i < a.Length ==> key <= a[i]
{}
n := lo;
}
c) Complete the code for the loop body below and verify it is correct using the Dafny verifier.
{
var lo, hi := 0, a.Length;
while lo < hi
invariant 0 <= lo <= hi <= a.Length
invariant forall i :: 0 <= i < lo ==> a[i] < key
invariant forall i :: hi <= i < a.Length ==> key <= a[i]
{
var mid := (lo + hi) / 2;
if a[mid] < key {
???
} else {
???
}
}
n := lo;
}
d) Change the specification and implementation for binary search so that it returns the “latest insertion point”, that is, an array position just after all occurrences ofthe key. Verify your changes using the Dafny verifier.