SENG 2011
Assignment 2
Proofs and Program Verification
Due Sunday 9pm, 21st November, 2021
Welcome to the 2nd assignment. Some notes:
• The total number of marks of the exercises will be scaled to 25 marks for the course assessment.
• In the Dafny exercises,
– Please make sure your code verifies with the CSE dafny verifier.
– None of the exercises requires you to compile code, or generate output.
– Use the given method and file names exactly. The auto-marker is case-sensitive.
– Do not use the assume statement or function methods in this assignment or this course.
– You may include your own Dafny predicates and functions except where noted.
– Specifications will be assessed for readability, conciseness and structure, and performance when
efficiency is a factor. Warnings are treated as errors in the assessment.
ex1.dfy 10 marks
It is a property of natural numbers that the product of the two consecutive natural numbers (CNNs),
that is n ∗ (n + 1), where n ≥ 0, is even. Dafny does not ‘know’ this property unfortunately.
Write a lemma called LemCNN that proves by induction this property. The signature of the lemma
should be:
lemma LemCNN(n: nat)
The proof should be Level 3 as described in the lecture notes. (There should be a base case, and every
step should be justified using comments.)
Using the lemma, write a tester that confirms that Dafny ‘has learnt’ this property for any natural
number n. (So your tester should verify.) The tester may be called anything that does not conflict
with Dafny.
Submit the file ex1.dfy, which should contain the lemma LemCNN and the tester.
ex2.dfy 10 marks
Write a method with signature:
method SecondLargest(a:array) returns (seclar:int)
which returns with the second largest element, here named seclar, in the input array. If there is no
such element, then the largest element in the input array should be returned. You may assume the
array cannot be empty.
Write a tester as well that verifies the method SecondLargest. The tester may be called anything that
does not conflict with Dafny. Include enough testcases to properly exercise the code. For example, if
the array is [2,42,-4,123,42] then Dafny should prove that the returned value is 42.
Submit the file ex2.dfy, which should contain method SecondLargest, the tester method, and no
other methods.
1
ex3.dfy 10 marks
In the English language, if something is the odd one out then it is different from all the rest, which
are all the same. We can apply the concept to sequences of numbers. For example, the odd-one-out in
the sequence [1,1,42,1] is 42. Note the odd-one-out has nothing to do with even/odd numbers. More
examples of sequences with an odd-one-out element are [99,99,1] and [0,42,42,42,42,42]. You can have
at most one element that is odd-one-out in a sequence of course.
A sequence of length 2 has an odd-one-out if the elements are different. We’ll arbitrarily define the odd-
one-out as the first element. So for example, the odd-one-out is the sequence [99,42] is 99. Sequences
of length less than 2 are not allowed. Example of sequences that have no odd-one-out element are
[99,99,99,99], [0,99,99,1], [1,2,3] and [42,42].
i Write a predicate with signature:
predicate ooo(s:seq)
which returns true if the input squence s contains an odd-one-out element, and false otherwise.
Write a tester for the predicate that includes appropriate testcases (see below). The tester may
be called anything that does not conflict with Dafny.
ii Write a verified method with signature:
method Getooo(s: seq) returns (x: int)
which returns the index x of the odd-one-out in sequence s, and -1 if there is none. (The indices
in the sequence start at count 0 of course.)
Test your method by calling it with appropriate testcases. A sample tester for both the predicate
and the method that shows two testcases in the following. You may of course write a different
tester for each part.
method Testooo()
{
var s:seq;
var r:int;
s := [1,1,42,1];
assert s[0]==1 && s[1]==1 && s[2]==42 && s[3]==1;
assert ooo(s); // Part (i)
r := Getooo(s); // Part (ii)
assert r==2;
s := [1,1,42,42];
assert s[0]==1 && s[1]==1 && s[2]==42 && s[3]==42;
assert !ooo(s);
r := Getooo(s);
assert r==-1;
}
Conditions:
• You are not allowed to use sets and multisets (and function methods of course).
• Do not count the number of instances of elements: this would be very inefficient as the problem
requires you to count to 1 only.
• Part (i) should verify quickly. The verification in Part (ii) may take longer, but recommended is
less than 5 seconds. There is a hard timelimit of 30 seconds.
Submit the file ex3.dfy, which should contain just methods Getooo and your tester.
2
ex4.dfy 10 marks
On the website you will find a file QuackRepair.dfy that contains a version of the Quack class data
type. The data type represents a stack of characters: it has operations Push(), Pop() and Empty().
There is also a series of tests in a method called Tester().
The datatype is missing an operation called Repair() that has signature:
method Repair(i:nat, c:char)
The method replaces the i-th element from the top of stack with the character c. If the value of i goes
passed the bottom of stack, the operation does nothing (there is no change). So, for example, if i = 0
then this operation replaces the element at the top of stack, assuming the stack is not empty. If i = 1
then this operation replaces the second element on the stack, if it is there, and so on. There is also a
tester in the file. This tester exercises the stack data type by pushing, popping and repairing.
You are asked to implement Repair(), verifying its correctness consistent with the other operations in
the class.
• Apart from the addition of the new method you are not allowed to modify the Quack class or
Tester in any way.
• The method should not call any other methods in the class.
• It should not be necessary to write any predicates or functions in this exercise.
• It is recommended your solution verify the series of tests in less than 5 seconds. There is a hard
timelimit of 30 seconds.
The submission process for ex4.dfy:
• Submit just the method Repair() in ex4.dfy. Your method will be auto-marked by append-
ing it to the system’s class and verified with the tester, so do not send Quack or Tester. Just
send method Repair.
• If this tester fails to verify, but you have a modified version that does verify, then you may include
another tester (name it something else). Marking does not involve program execution, so do not
submit a method Main().
ex5.dfy 10 marks
In lectures, the 100 Prisoners and a Light Bulb problem was handled. It assumed that initially the
light was turned off.
Write a verified solution in Dafny to this problem that makes no assumption about the initial state of
the light bulb. The signature and specification that you must use is the following:
method Prison(all: set, inlight:bool) returns (swch: set)
requires |all| > 1
ensures |swch|+1 == |all|
ensures swch < all
decreases *
where in the signature:
• all is the set of prisoners (there is more than 1 in the prison)
• inlight is the initial state of the light (true/false represents on/off)
• swch is the set of prisoners that have switched the light on (at least once) (note the prisoner that
does the counting is not a member of this set).
You may use the solution presented in Week 8 lectures, and any accompanying lemmas, as starting
point.
Submit the file ex5.dfy, which should contain just the method Prison and no other methods.
3
In total, you should submit the files ex1.dfy, ex2.dfy, ex3.dfy, ex4.dfy and ex5.dfy on the course website.
If you have made no attempt at a question, submit an empty file for that question.
Good luck.
4

学霸联盟