COMP1600 6260
Foundations of Computing: Week 4
S2 2025
Practical Session 4
• This tutorial will give you practice at mathematical induction, both by hand and using Dafny.
• Use the Dafny file 04-tutorial-handout.dfy for the Dafny and mini-assignment questions.
• Upload a plain text file called u123456.dfy (replace by your uID) to Wattle, you might lose (some) marks otherwise.
• Submit the exercises marked MA by Wednesday 20th August, 2025, 09:00 via Wattle. Late submissions will score 0.
Exercise 1 Induction Problem 1
Notice that the following holds:
1 = 1
1 + 3 = 4
1 + 3 + 5 = 9
1 + 3 + 5 + 7 = 16
1 + 3 + 5 + 7 + 9 = 25
Work out a general formula for the above, and prove it using mathematical induction. All steps of the proof must be shown. The proof should be completed without Dafny.
Exercise 2 Induction Problem 2
Prove, using mathematical induction, that:
for all integers n ≥ 2.
All steps of the proof must be shown. The proof should be completed without Dafny.
The next few exercises require the following definitions of even and odd:
ghost predicate even (n: nat) { exists k : nat :: n == 2 * k }
ghost predicate odd (n: nat) { exists k : nat :: n == 2 * k + 1 }
Exercise 3 Even, Odd and Successor
These lemmas were shown in the lectures. They are needed for the later questions in this tutorial. Try to implement them without re-watching the lectures, but if you get stuck, take a look at the lectures.
lemma even_succ (n: nat) lemma odd_succ (n: nat)
ensures even (n) ==> odd (n+1) ensures odd(n) ==> even (n+1)
{ /* your proof here */ } { /* your proof here */ }
Exercise 4 All Integers are Even or Odd
To show that all integers are either even or odd, another lemma is required, which shows that a given integer is either even or odd. There are two different ways to prove thi: one is by induction, and the other uses arithmetic and division with remainder (i % k is the remainder of dividing i by k in Dafny).
Implement the following lemma, by using further lemmas as described below::
lemma all_even_odd()
ensures forall n: int | n >= 0 :: even(n) || odd(n){
{ /* Insert your proof here, which uses even_odd_ind.*/ }
lemma even_odd_ind (n:nat) lemma even_odd_nonind (n: nat)
ensures even(n) || odd(n) ensures even(n) || odd(n)
{ /* your inductive proof here */ } { /* your non-inductive proof here */ }
For the inductive proof, you might want to use the auxiliary lemmas from the previous exercise.
Exercise 5 Verification of Functions (MA, 10 credits)
The following function (very inefficiently) determines whether or not a number is even.
function is_even (n: nat) : bool { lemma is_even_corr (n: nat)
if (n == 0) then true ensures is_even(n) ==> even(n)
else if (n == 1) then false { /* your proof here */ }
else is_even(n-2)
} lemma even_is_corr (n: nat)
ensures even(n) ==> is_even(n)
{ /* your proof here */ }
Show that this function indeed matches its specification by proving the lemma on the right above. You might want to prove an auxiliary statement first, or use one of the previous lemmas from this tutorial. Hint: More than one base case may be required.