The University of New South Wales SENG2011: Workshop on Reasoning about Programs MOCK Examination Paper Term 3, 2020 • Total time allowed: 50 minutes including 5 minutes reading time • You should have read the Examination Rules document before attempting the exam. ex1.dfy 0 marks Write a Dafny predicate Acheck that, given an array a of integers, and integer n, is true if the following properties are satisfied (and false otherwise): • the length of the array is even • if the index of an element in the array is divisible by n then the element is 0 The input parameter n cannot be 0 of course. You are not allowed to write any other predicates or methods. So, for example, Acheck(a, 2) is true if array a is [0,42,0,42,0,42]. But Acheck(a, 2) is false if array a is [0,4,2,0] or [0,0,0] or [1,2]. Another example is Acheck(a, 5) is true if array a is [0,1,2,3] or even just []. Limit the time you spend on each exercise. Submission: give se2011 mock ex1.dfy ex2.dfy 0 marks Write a Dafny method that has signature: method Deli(a: array
, i: int) which deletes the character at index i of an array, where 0 ≤ i < a.Length, by shuffling all the characters from index i + 1 up to the end of the array each down 1 place in the array. (hence the element that was at index i is over-written). A ’.’ is put at the last index in the array. For example, if the array a is [’b’,’r’,’o’,’o’,’m’], then calling deli(a, 1) will delete the character at index 1 by shuffling the 3 letters ’o’, ’o’ and ’m’ down 1 place, and put ’.’ at the last index. The result is the array into [’b’,’o’,’o’,’m’,’.’]. The integer i must be an index in the array (which means the array cannot be empty). You are not allowed to write any other predicates, functions or methods. A method that does a basic check of the verification is the following: 1 method Ex2Checker() { var z := new char[][’b’,’r’,’o’,’o’,’m’]; Deli(z, 1); assert z[..] == "boom."; z := new char[][’x’]; Deli(z, 0); assert z[..] == "."; } You can find a copy of this method on the course website for your convenience, under the Exam link. You are allowed to cut&paste this checker and use it to do testing. If you have time you should add more tests. Limit the time you spend on each exercise. Submission: give se2011 mock ex2.dfy End of Mock Exam 欢迎咨询51作业君