代做Assignment 2 CSSE3100/7100 Reasoning

日期：2022-05-04 09:50

Assignment 2 CSSE3100/7100 Reasoning about Programs

Due: 1pm on 10 May, 2022

The aim of this assignment is to provide you with experience in specifying and deriving

array-based algorithms, and verifying them using Dafny. It is worth 20% of your final mark

for the course.

Instructions: Submit a Dafny file for each of Q1 and Q2, and if you are a CSSE7100

student for Q3. These files should be submitted to Blackboard by the due date and time.

1. A sequence is said to be monotonically non-decreasing if it either consists of only one

element, or it consists of two or more elements where these elements are in non-descending

order. The following function mono determines whether the sequence a[i..j] is monotonically

decreasing.

function mono(a: array<int>, i: nat, j: nat): bool

requires a.Length > 0 && 0 <= i < j <= a.Length

reads a

decreases j - i {

if j == i + 1 then true

else if a[i] <= a[i + 1] then mono(a, i + 1, j) else false

}

Your friend writes a method to return the index r of an array a such that a[0..r] is the longest

monotonically non-decreasing sequence in a starting at a[0].

method M(a:array<int>) returns (r: int)

requires a.Length > 0

ensures 1 <= r <= a.Length && mono(a, 0, r) && (r == a.Length || a[r - 1] > a[r])

{

r := 1;

while r < a.Length && a[r - 1] <= a[r]

invariant 1 <= r <= a.Length

invariant mono(a, 0, r)

{

r := r + 1;

} }

Unfortunately, he can't get it to verify in Dafny.

Your task: Write and prove a lemma which allows Dafny to verify your friend's program

when a call to the lemma is made from his code. Note you must not change the specification,

loop invariant or code above except to add a call to your lemma. (4 marks)

2. You have been asked to write a program PatternReplace which searches an integer array a

for a pattern of elements (provided in a strictly smaller integer array p) and

a) replaces the first occurrence of the pattern in a by another pattern of the same size

(provided in an integer array q), and

b) returns the position of the start of the pattern it replaced, if any, and -1 otherwise.

For example, if a were [2, 1, 2, 3, 4, 2, 3, 5], p were [2, 3] and q were [0, 0] then the program

should change a to [2, 1, 0, 0, 4, 2, 3, 5] and return 2.

If on the other hand p were [3, 2] and a and q were as before then the program would not

change a and return -1.

Your colleague suggests the following strategy for writing the program using 2 loops, an

outer and an inner loop. The outer loop iterates over the indices of the array a starting from 0.

For each index, it uses the inner loop to check whether the pattern in p is in a starting from

that index. If so, it sets r to that index and on this and the next p.Length-1 iterations of the

outer loop replaces the elements in a by those of q. To do this replacement, you can introduce

a local variable count which is initially p.Length and which reduces by 1 on each

replacement. When it reaches 0, you're done!

You like this strategy but want to be sure your algorithm is correct, so you are going to use

Dafny to verify it. You already realise you can use wishing to introduce count.

Your task: Write a Dafny program following your colleague's strategy including the

necessary specifications and loop invariants to verify it. You are not allowed to use break or

return statements or Dafny's mathematical types, such as sequences, in your code. You may

use Dafny's mathematical types in specifications.

For each loop invariant state which loop design technique you used to derive the invariant, or

otherwise state the reason the invariant was introduced, e.g., to place bounds on a variable

used as an array index. To simplify your predicates (and hence manage complexity!) it is recommended that you

a) Use multiple ensures clauses and invariants. Keep them as simple as possible. You

will find that you need many postconditions and invariants. Don't forget that there

may be different cases for when r == -1 and when r != -1.

b) Define a Boolean function IsStart, which determines whether an index i, in array (or

equivalent sequence) a is the start of the pattern defined by array (or equivalent

sequence) p. That is, for the first example above, i == 2 or i == 5 would result in true,

whereas i == 0 or i == 1 would result in false.

c) Avoid predicates with nested quantifications where possible. Dafny sometimes has

trouble reasoning about these without lemmas. (You should not need lemmas for this

question.) Note that a predicate like a[n..m] == 0 is essentially using universal

quantification. That is, a[n..m] == 0 is equivalent to forall i :: n <= i < m ==> a[i] == 0.

You may find this question challenging and not be able to get Dafny to verify your program.

Be assured you will get part marks for every correct part of your specification and invariants,

even if your program does not verify. (16 marks)

3. (CSSE7100 students only) The program of Q2 searches for the first occurrence of the

pattern p in a and replaces it with the pattern q, returning its starting position in r.

(a) Write a method header including pre- and postcondition specifications for a program

which performs the same search and replace starting from an index j, where j is provided as

an additional input. There is no need to provide invariants or code for this program.

(b) Write a method header including pre- and postcondition specifications for a program

which replaces all patterns p in a with q, returning true in r when there has been at least one

replacement and false otherwise. There is no need to provide invariants or code for this

program.

In both parts of this question, you may use your IsStart function from Q2. It is not required

that you avoid nested quantifications in this question. (4 marks)

Marking

In each question, you will get marks for parts of your specifications, invariants, etc. which are

correct even if your entire answer is not correct, e.g., your program is not verifying.

For Q1, the distribution of marks is 2.5 marks for the lemma header including specification,

0.5 marks for the lemma call, and 1 mark for the lemma proof.

For Q2, the distribution is 4.5 marks for the method header including specification, 8 marks

for loop invariants (including comments about derivation) and termination metrics (if not

automatically provided), and 3.5 marks for your code.

For Q3, each of the method specifications is worth 2 marks.

CSSE7100 students will be given a mark out of 24 which will then be scaled to their final

mark for the assignment out of 20.

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: