CSSE3100/7100 Reasoning about Programs
Week 7 Exercises
In each of the following exercises, use the loop design techniques from Week 5 to find invariants that imply the postconditions when the loop terminates. Provide additional invariants based on your mental model of the implementation when needed.
Exercise 7.1.
Specify and implement a method that increases every element of an integer matrix by 1. Verify your method is correct using the Dafny verifier.
Note: An integer matrix has type array2<int> and has number of rows Length0 and number of columns Length1.
Exercise 7.2.
Specify and implement a method that copies the elements of one matrix to another of the same dimensions. Allow the matrices to be possibly aliased. Verify your method is correct using the Dafny verifier.
Exercise 7.3.
Specify and implement a method
method DoubleArray(src: array<int>, dst: array<int>)
that sets dst[i] to 2*src[i] for each i. Assume the given arrays have the same lengths, and allow the possibility that they reference the same array. Verify your method is correct using the Dafny verifier.
Exercise 7.4.
Specify and implement a method that in a given array rotates the elements “left” . That is, what used to be stored in a[i + 1] gets stored in a[i], and what used to be stored in a[0] gets stored in a[a.Length - 1]. Verify your method is correct using the Dafny verifier.
Hint: There is a strategy which involves swapping pairs of elements of a. Try working out this strategy on paper first.
Exercise 7.5.
Specify and implement a method that in a given array rotates the elements “right” . That is, what used to be stored in a[i - 1] gets stored in a[i], and what used to be stored in a[a.Length - 1] gets stored in a[0]. Verify your method is correct using the Dafny verifier.
Hint: Again there is a strategy which involves swapping pairs of elements of a.