CSSE3100代写、代写Python，c++编程

日期：2023-04-28 11:30

ssignment 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