Dafny coursework exercises
Copyright By PowCoder代写 加微信 powcoder
Autumn term 2022
There are three tasks, each of which involve some programming, some ver-
ifying, and a few short questions. The tasks appear in roughly increasing order
of difficulty, and each is worth 15 marks. Tasks labelled (?) are expected to be
straightforward. Tasks labelled (??) should be manageable but may require quite
a bit of thinking. Tasks labelled (???) are highly challenging; it is not expected
that many students will complete these.
Marking principles. If you have completed a task, you will get full marks
for it and it is not necessary to show your working. If you have not managed
to complete a task, partial credit may be given if you can demonstrate your
thought process. For instance, you might not be able to come up with all
the invariants that are necessary to complete the verification, but perhaps you
can confirm some invariants and express (in comments) some of the other
invariants that you think are needed but haven’t managed to verify.
Submission process. You are expected to produce a single Dafny source
file called YourName.dfy. This file should contain your solutions to all
of the tasks below that you have attempted. You are welcome to show your
working on incomplete tasks by decorating your file with /*comments*/ or
//comments. Some of the tasks contain questions that require short written
answers; these answers can be provided as comments.
Plagiarism policy. You are allowed to consult the coursework tasks from
previous years – the questions and model solutions for these are available.
You are allowed to consult internet sources like Dafny tutorials. You are
allowed to work together with the other student in your pair. Please don’t
submit these programs as questions on Stack Overflow! And please don’t
share your answers to these tasks outside of your own pair. If you would
like to share your answers to these tasks publicly, e.g. on a public GitHub
repo, you are welcome to do so after the deadline, but please check with me
first, because some students may still be working on the coursework with an
extended deadline.
Task 1 (?) How many squares (of any size) are in the following 3×3 grid? [1 mark]
Here is a Dafny program that calculates how many squares are in an nxn
1 method countsquares(n:nat) returns (result:nat)
2 ensures result == /*TODO*/
4 var i := 0;
5 result := 0;
6 while i < n {
7 i := i + 1;
8 result := result + i * i;
Replace /*TODO*/ with an expression that captures the relationship be-
tween the input n and the calculated result.[4 marks] Add annotations to
your program so that Dafny can verify that your postcondition always holds.[5 marks]
Here is another Dafny program that calculates the same result in a different
1 method countsquares2(n:nat) returns (result:nat)
2 ensures result == /*TODO*/
4 var i := n;
5 result := 0;
6 while i > 0 {
7 result := result + i * i;
8 i := i – 1;
Replace /*TODO*/ with the same postcondition as before, and add anno-
tations so that Dafny can verify that it always holds.[4 marks]
Which is easier to verify, countsquares or countsquares2? Com-
ment briefly on why that might be.[1 mark]
Task 2 (??) Let us define the sorted predicate as follows:
1 predicate sorted(A:array
4 forall m,n ::
5 0 <= m < n < A.Length ==> A[m] <= A[n]
Here is a Dafny implementation of binary search for a value v in a sorted
array A of integers.
1 method binarysearch_between(A:array
2 lo:int, hi:int) returns (result:bool)
4 if lo == hi {
5 return false;
7 var mid:int := (lo + hi) / 2;
8 if v == A[mid] {
9 return true;
11 if v < A[mid] {
12 result := binarysearch_between(A,v,lo,mid);
14 if v > A[mid] {
15 result := binarysearch_between(A,v,mid+1,hi);
19 method binarysearch(A:array
20 returns (result:bool)
22 result := binarysearch_between(A,v,0,A.Length);
Provide a postcondition for the binarysearch method that says that
result is true if and only if v is one of the elements in A.[3 marks] Add an-
notations so that Dafny can verify that this postcondition always holds.[5 marks]
Write a second implementation of binary search, called binarysearch_iter,
that uses iteration (a while loop) instead of recursion.[3 marks] Prove that
your iterative implementation satisfies the same postcondition as the recur-
sive implementation.[4 marks]
Task 3 (???) Here is a Dafny implementation of the Quicksort algorithm pub-
lished by C.A.R. Hoare in 1961:
1 method partition(A:array
2 returns (pivot:int)
3 requires 0 <= lo < hi <= A.Length
4 ensures 0 <= lo <= pivot < hi
5 ensures forall k ::
6 (0 <= k < lo || hi <= k < A.Length) ==>
7 old(A[k]) == A[k]
8 modifies A
10 pivot := lo;
11 var i := lo+1;
12 while i < hi
13 invariant 0 <= lo <= pivot < i <= hi
14 invariant forall k ::
15 (0 <= k < lo || hi <= k < A.Length) ==>
16 old(A[k]) == A[k]
17 decreases hi – i
19 if A[i] < A[pivot] {
20 var j := i-1;
21 var tmp := A[i];
22 A[i] := A[j];
23 while pivot < j
24 invariant forall k ::
25 (0 <= k < lo || hi <= k < A.Length) ==>
26 old(A[k]) == A[k]
27 decreases j
29 A[j+1] := A[j];
30 j := j-1;
32 A[pivot+1] := A[pivot];
33 A[pivot] := tmp;
34 pivot := pivot+1;
36 i := i+1;
40 method quicksort_between(A:array
41 hi:int)
42 requires 0 <= lo <= hi <= A.Length
43 ensures forall k ::
44 (0 <= k < lo || hi <= k < A.Length) ==>
45 old(A[k]) == A[k]
46 modifies A
47 decreases hi – lo
49 if lo+1 >= hi { return; }
50 var pivot := partition(A, lo, hi);
51 quicksort_between(A, lo, pivot);
52 quicksort_between(A, pivot+1, hi);
55 method quicksort(A:array
56 modifies A
58 quicksort_between(A, 0, A.Length);
The code has been partially verified for you: enough annotations have been
added to convince Dafny that (1) none of the array accesses are out-of-
bounds, and (2) that the quicksort_between method only modifies
the A array between indices lo and hi.
Explain briefly what the old keyword on line 7 means, and why it is
needed.[2 marks]
Complete the verification by establishing sorted(A) as a postcondition
for the quicksort method.[13 marks]
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com