CMPT 477/777 Formal Verification
Programming Assignment 3
This assignment is due by 11:59pm PT on Friday Nov 15, 2024. Please submit it to Canvas.
Late policy:
Suppose you can get n (out of 100) points based on your code and report
• If you submit before the deadline, you can get all n points.
• If you submit between 11:59pm PT Nov 15 and 11:59pm PT Nov 16, you get n − 10 points.
• If you submit between 11:59pm PT Nov 16 and 11:59pm PT Nov 17, you get n − 20 points.
• If you submit after 11:59pm PT Nov 17, you get 0 points.
1. (20 points) Verify the program in Algorithm 1. Note that you cannot change the existing implementation.
Algorithm 1 Find an element in the array
method Find(a : array⟨int⟩, v : int) returns (index : int)
ensures index ≥ 0 → index < a.Length ∧ a[index] = v
ensures index < 0 → ∀k. 0 ≤ k < a.Length → a[k] = v
1: var i : int := 0;
2: while i < a.Length do
3: if a[i] = v then
4: return i;
5: i := i + 1;
6: return −1;
2. (20 points) Verify the program in Algorithm 2. Note that you cannot change the existing implementation.
Algorithm 2 Sum of 10n + 10(n − 1) + . . . + 10
method Sum(n : int) returns (sum : int)
requires n > 0
ensures sum = 5n × (n + 1)
1: sum := 0;
2: var i : int := n;
3: while i > 0 do
4: var k : int := 0;
5: var j : int := i;
6: while j > 0 do
7: k := k + 10;
8: j := j − 1;
9: sum := sum + k;
10: i := i − 1;
1
3. (30 points) Given a non-empty array of integers, write a method called ArrayMin that finds the minimum
value min in the array. Verify the method can ensure
• min is less than or equal to all elements in the array
• min is equal to some element in the array
4. (30 points) Given an array of coins showing either Front or Back side on top, write a program with a
SortCoins method that sorts the coins. Verify it can ensure
• All coins showing the Front side occur before those showing Back
• The sorted array is a permutation of the original array
Deliverable
A zip file called P3 SFUID.zip that contains at least the followings:
• A file called P3 SFUID.dfy that contains Dafny programs for the above four questions.
• A report called P3 SFUID.pdf that explains the design choices, features, issues (if any), and anything
else that you want to explain about your programs.
2

请加QQ：99515681  邮箱：99515681@qq.com   WX：codinghelp