CSSE3100/7100 Reasoning about Programs Assignment 2

Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

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 Programmingfrom 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