ECE653 Software Testing, Quality Assurance, and Maintenance Assignment 3

Description

Question 1 (5 points)
The following program computes a sum of telescoping series1 of powers of two in a variable r:
1 assume (n >= 0);
2 r := 0;
3 i := 0;
4 p := 1;
5 while not (i = n) do
6 {
7 r = r – p;
8 p = 2 * p;
9 r = r + p;
10 i = i + 1;
11 }
Show that the program is correct using the rules of Hoare logic and the fact that
Xn
i=1
(2i − 2
i−1
) = 2n − 2
0
That is, let P denote the statements in lines 510. Construct a derivation to show validity of the following Hoare
triple:
{n ≥ 0 ∧ r = 0 ∧ i = 0 ∧ p = 1} P {r = 2n − 1}
Hint: you can use p = 2i ∧ r = 2i − 1 ∧ i ≤ n as an inductive invariant for the while loop.
You can use the combined rule of assignment and consequence to shorten the proof
P =⇒ Q[e/x]
{P} x := e {Q}
ASGN + CONS
Recall that the notation Q[e/x] stands for an expression Q in which e replaces all occurrences of x.
1https://en.wikipedia.org/wiki/Telescoping_series.
2
Question 2 (10 points)
For this question, you will have to verify two small programs in Dafny. You can install Dafny locally on your
machine following the instructions in the lecture notes. Alternatively, you can use the web-interface at http:
//rise4fun.com/dafny. Local installation is preferred.
All les for this questions are contained in dafny folder of the repository.
(a) CalcTerm.dfy: The le contains a method
CalcTerm(m:int, n:nat) returns (res:int)
The method computes 5 × m − 3 × n using a loop and operations to add 3, and subtract 1 and 2.
Provide the missing invariants and decreases annotations so that the method veries.
(b) SlowMax.dfy: The le contains a method
slow_max(a:nat, b:nat) returns (z:nat)
that computes z = max(a, b) via a series of increments and decrements.
Provide the missing invariants and decreases annotations so that the method veries.
Question 3 (30 Points)
For this question, you will have to verify two implementation of sorting methods in Dafny. You can install Dafny
locally on your machine following the instructions in the lecture notes. Alternatively, you can use the web-interface
at http://rise4fun.com/dafny. Local installation is preferred.
All les for this questions are contained in dafny folder of the repository.
(a) Pancake sorting2
is a sorting technique that uses only ip operation in which elements of an array are reversed (ipped) at some position. The directory pancakesort contains an implementation of pancake sorting
algorithm in Dafny.
• Specify and verify method findMax in findmax.dfy
• Specify and verify method flip in flip.dfy
• Specify and verify method pancakeSort in PancakeSort.dfy
(b) Quicksort3
is an ecient sorting technique developed by Tony Hoare. The directory quicksort contains an
implementation of quick sort in Dafny.
• Write a loop invariant to complete the verication of partition method in part.dfy
• (Bonus) Complete and verify the implementation of qsort method in QuickSort.dfy. You might nd
Chapter 6 of Calculus of Computation useful for this problem.
2https://en.wikipedia.org/wiki/Pancake_sorting
3https://en.wikipedia.org/wiki/Quicksort
3
Question 4 (25 points)
The repository includes an implementation of a parser, interpreter, and symbolic execution engine for the WHILE
language from the lecture notes. Your task is to extend the symbolic execution engine to a verication engine. You
can use the provided code, or the symbolic execution engine you have developed as part of Assignment 2. The
implementation of the symbolic execution engine is located in directory wlang. You can execute the engine using
the following command:
(venv) $ python -m wlang.sym wlang/test1.prg
A sample program is provided for your convinience in wlang/test1.prg
The syntax of the WHILE language has been extended with annotation for
while b inv inv do s
where b is a Boolean loop condition, inv is a Boolean invariant, and s a statement. Recall (from the lecture notes)
that execution of an annonated while-loop is equivalent to the following loop-free program that checks that inv is
indeed a loop invariant:
assert inv;
havoc V;
assume inv;
if b then { s ; assert inv; assume false }
where V is the set of all variables modied (i.e., dened) in the loop body s.
(a) Extend your symbolic execution engine to execute while-loops annotated with loop invariants. Your engine
should execute the loop according to the scheme above and report any assertion failures (i.e., whether inv fails
initiation or invariance).
Hint: You can use your Undened Use Visitor from Assignment 1 to nd all variables that are modied/dened
by the loop body.
(b) Provide the missing inductive invariants and use your implementation to verify the following program:
havoc x, y;
assume y >= 0;
c := 0;
r := x;
while c < y
inv [MISSING]
do
{
r := r + 1;
c := c + 1
};
assert r = x + y
(c) Extend the test suite test_sym.py to achieve 100% branch coverage of your implementation. Recall that
you can run the test suite using
(venv) $ python -m wlang.test
and measure coverage of the test suite using
(venv) $ coverage run -m wlang.test
(venv) $ coverage html
(d) Construct a program with at least one loop and inductive invariants and verify it using your system. You can
use a variant of a program from part (b) of this question, or create a dierent one. Save the program in the
le called q3d.prg at the top of the repository.