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作业君