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 non-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: http://www.itee.uq.edu.au/itee-student-misconduct-including-plagiarism