Assignment 2 CSSE3100/7100 Reasoning about Programs
Due: 4pm on 28 April, 2023
The aim of this assignment is to consolidate your understanding of the course's material on
arrays, program derivation and recursion. It is worth 20% of your final mark for the course.
Instructions: Upload a plain text file with your solution to Question 1(b) and a Dafny
file with your solutions to Questions 1(a) and 2 (and Question 3, if applicable) to
Gradescope by the due date and time.
1. Imagine you need to make multiple queries regarding the number of even numbers in
various parts of a large integer array, a. For example, a first query might ask for the number
of even numbers from position 336 up to, and including, position 500 of a, and the second
may ask for the number of even numbers from 336 up to, and including, 479. If you search
through the relevant part of a on each query, you may end up duplicating work previously
carried out (in the example the range of positions from 336 to 479 would be searched twice).
An alternative is to search through the entire array just once, storing in a second integer array
of the same length, b, the number of even numbers up to each point in array a, i.e., b[i] will
hold the number of even numbers occurring in the elements a[0] ... a[i] (note that an even
number in a[i] is included in this count). The number of even numbers from positions i up to,
and including, position j of a would then be b[j] - b[i-1] when i > 0, and b[j] otherwise.
(a) Given the function Count below, specify and derive a method PreCompute which given
two integer arrays a and b of the same length, assigns values to b as described above. The
method must call a second method ComputeCount which uses recursion (and not a loop) to
write values to the array b. Provide a termination metric that allows Dafny to verify this
method and hence verify your method PreCompute.
Note that Count is declared as ghost which means it cannot be used in code. It can only be
used in specifications and invariants. You are not allowed to define and use any other
functions in your solution. (6 marks)
ghost function Count(hi: nat, s:seq): int
requires 0 <= hi <= |s|
decreases hi
{
if hi == 0 then 0
else if s[hi-1]%2 == 0 then 1 + Count(hi-1, s) else Count(hi-1, s)
}
(b) Provide a weakest precondition proof that PreCompute is partially correct. (4 marks)
2. For further efficiency, specify and derive a program Evens which given an integer array a,
returns a 2-dimensional integer array c such that c[i, j] directly provides the number of even
numbers from position i up to, and including, position j of a. Note that this will be 0
whenever j < i.
Your program should call PreCompute to get the values in array b and then use one or more
loops (no recursion this time) to write the values to the array c. Again, you are not allowed to
define and use any other functions in your solution.
Check your program using the Dafny verifier. There is no need to provide a proof.
(10 marks)
3. (CSSE7100 students only) Using your specification of PreCompute from Question 1,
derive a program PreComputeL using one or more loops (no method calls or recursion) to
write values to b. Again, you are not allowed to define and use any other functions in your
solution.
Check your program using the Dafny verifier. There is no need to provide a proof.
(3 marks)
Hints: Be careful regarding end points: Count provides the number of even numbers from
position 0 up to, but not including, position hi, whereas b[i] is the number of even numbers
from position 0 up to, and including, position i.
Don't forget about aliasing, and that a <= b < c is a <= b && b < c!
Marking
For Questions 1(a) and 2 (and Question 3 if applicable), you will get marks for
correctness of specifications
completeness of specifications
key lines of code
correctness and completeness of loop invariants
Note that you will get part marks even if your code doesn't verify in Dafny.
For Question 1(b), you will get marks for
the application of the appropriate weakest precondition rules for each line of code,
stating why the entire method is correct, and
correct and, where necessary, justified predicate transformations.
You must justify all predicate transformations which are not due to either simple arithmetic
or commutativity of && or ||. Justification must be either
a law from Appendix A of Programming from Specification (Questions 1),
a brief explanation for any non-obvious arithmetic step (Question 1), or
"strengthening" when you have strengthened a predicate (Question 1). Strengthening
steps must be obvious, e.g., adding one or more conjuncts, or restricting the range of
values of one or more variable.
For CSSE7100 students, the final mark is M - (3 - m) where M is the mark for Questions 1
and 2 (out of 20) and m is the mark for Question 3 (out of 3).
School Policy on Student Misconduct
This assignment is to be completed individually. You are required to read and understand the
School Statement on Misconduct, available on the School's website at:
http://www.itee.uq.edu.au/itee-student-misconduct-including-plagiarism