SENG 2011
Assignment 2
Program Verification and Reasoning
Due Friday 9pm, 20th November, 2020
• The total number of marks of the exercises will be scaled to 25 marks for the course assessment.
• Readability and conciseness in both the code and the specification are considered in marking.
• Please make sure your code verifies with the CSE dafny verifier.
• Be careful in naming the methods and predicates in each exercise as the auto-marker will use exactly
these names to check your code and specification.
• There is no output in any of the exercises: so no print statements, no Main(), and no executable.
ex1.dfy 5 marks
Write a Dafny method that has signature:
method StringSwap(s: string, i:nat, j:nat) returns (t: string)
that swaps the elements at indexes i and j in string s resulting in a new string t, which is returned.
The indexes in the string are numbered from 0 of course. The indexes in the parameter list must be
within bounds of the string except if the string is empty, in which case the indexes do not matter (but
must be type-correct of course).
You should verify that the method behaves correctly. For example, the following fragment of code
should verify.
var a:string := "1scow2";
var b:string := StringSwap(a, 1, 5);
assert b == "12cows";
var c:string := "";
var d:string := StringSwap(c, 1, 2);
assert c == d;
You are not permitted to use any arrays in this exercise.
ex2.dfy 5 marks
Write a Dafny method that has signature:
method String3Sort(a: string) returns (b: string)
that sorts an input string a of exactly length 3 into ascending ASCII order, and returns the result in
string b. You are not permitted to use any arrays in this exercise.
An example of a fragment of code that checks the verification is the following:
var a:string := "cba";
var b:string := String3Sort(a);
assert b=="abc";
1
ex3.dfy 10 marks
Write a Dafny method that has signature:
method BadSort(a: string) returns (b: string)
which implements the linear sort algorithm described in slide 14 of the Flag Sort lecture. Notice the
data type is a string. You are not allowed to use an array in this exercise. The letters in the string are
an arbitrary string of letters ’b’, ’a’ and ’d’ (these correspond to the 3 colours). The method orders the
string into all the b’s first, then a’s and finally all the d’s. The string may have any length.
A fragment of code that checks the verification is the following:
var f:string := "dabdabdab";
var g:string := BadSort(f);
assert multiset(f)==multiset(g);
assert sortedbad(g);
Note the following:
• As shown in the fragment above, you should declare and call a predicate that has signature:
predicate sortedbad(s:string)
which verifies that the elements in the string are sorted into the correct order (b-a-d).
ex4.dfy 15 marks
Write a Dafny method that has signature:
method ShuffleSort(a: array) returns (b: array)
which implements an insertion sort using a shuffle-based strategy described in slides 7–10 in the
lecture Insertion Sort. (Hence do not use the swap-based strategy.) In this method, the elements of
the input array a are sorted using the shuffle strategy resulting in a sorted array b (in ascending order),
which is returned. The array a and its elements should not be affected. The array may be of any
length.
A fragment of code that checks the verification is the following
var a := new char[5][’e’,’d’,’c’,’b’,’a’];
assert a[0]==’e’ && a[1]==’d’ && a[2]==’c’ && a[3]==’b’ && a[4]==’a’;
var b := ShuffleSort(a);
assert sortedarray(b, 0, b.Length);
assert multiset(b[..]) == multiset(a[..]);
Note the following:
• As shown in the fragment above, you should declare a predicate that has signature:
predicate sortedarray(c:array, m:nat, n:nat)
which verifies that the elements between m and n− 1 of the array c are sorted in ascending order.
• It is possible that CSE dafny will take more than a minute to verify the program for the fragment
of code above. The marking will also reward performance in this exercise.
ex5.dfy 10 marks
1. Write a recursive Dafny function that computes xn, for integer x, and n ≥ 0, and has signature:
function expo(x:int, n:nat): int
2. Write a level-3 Dafny inductive lemma that proves the expression 23n − 3n mod (2+3) is 0 for
n ≥ 0. Use the signature:
lemma {:induction false} Expon23(n: nat)
The lemma should use the expo() function to compute the expression.
2
ex6.dfy 10 marks
On the website you will find a version of the Quack class data type that represents a stack of characters
and operations Push(), Pop() and Empty(). There is also a test case in a method called Checker().
The datatype is missing an operation called TopSort() that ‘sorts’ the top two data items on the stack.
If the second element on the stack (from the top) is larger than the element at the top, then the two
elements are swapped, otherwise there is no change. The operation does nothing if there is less than
two elements on the stack. The operation takes no arguments and returns no results. The operation is
called in Checker(), which pushes and pops data onto and off the stack in a testcase.
You are asked to implement TopSort(), 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 in any
way, or Checker() (but see also below).
• It is important that you accurately specify the changes that TopSort() makes to the class in the
pre- and post-conditions. The marking takes this into account.
The submission process for ex6.dfy:
• Submit only the method TopSort() in ex6.dfy. Your method will be auto-tested by including
it into the system’s Quack and verified with Checker().
• If Checker() fails to verify, but you have a modified version that does verify, then optionally you
may submit a file called mychecker.dfy (notice all lower case), which should contain just your
version of Checker(). Note that printing is not verification, and programs are not executed, so
do not submit a method Main().
As with the first assignment, there will be a submit instructions document on the website.
Good luck.
3

欢迎咨询51作业君