COMP1600/6260 Foundations of Computing: Week 1
S2 2025
Tutorial 1
In this tutorial you will:
• become familiar with propositional formulae,
• construct truth tables,
• learn how to understand logical equivalence, and
• learn how to use the Dafny tool to create simple program specifications.
No submission is required for this tutorial.
Exercise 1 Boolean formulae evaluation
Consider the truth value assignment σ that assigns the following truth values to the variables p, q and r: σ(p) = T, σ(q) = T, and σ(r) = F. Which of the following formulae evaluate to T under the assignment σ? Use truth tables to work it out.
1. (¬p ∨ ¬q) ∨ ¬(r ∧ q)
2. ¬(¬p ∨ ¬q) ∨ (p ∨ ¬r)
3. ¬(p ∨ ¬q) ∧ r
4. ¬(p ∨ ¬q ∧ r)
Exercise 2 Logical Equivalence
Which of the formulae are logically equivalent? Use truth tables to work it out.
1. p ∧ q ∨ ¬p ∧ ¬q
2. ¬p ∨ q
3. (p ∨ ¬q) ∧ (q ∨ ¬p)
4. ¬(p ∨ q)
5. (q ∧ p) ∨ ¬p
Exercise 3 Card Games
Imagine that a logician puts four cards on the table in front of you. Each card has a number on one side and a letter on the other. On the uppermost faces, you can see E, K, 4, and 7. He claims that if a card has a vowel on one side, then it has an even number on the other. How many cards do you have to turn over to check this?
Exercise 4 Postconditions in Dafny
Make sure that you watch the lectures this week, where basic Dafny concepts were discussed.
Suppose that you have the following function for computing the maximum of three integers:
function FindMax(x:int,y:int, z:int): int
ensures FindMax(x,y,z) >= x && FindMax(x,y,z) >= y && FindMax(x,y,z) >= z{
if x > y && x > z then x
else if y > x && y > z then y
else z
}
a) Run it in Dafny. Is the postcondition proved? If not, see whether you can fix the issue in the function so that the postcondition (ensures clause) is proved.
b) Is the postcondition want we want? Write a function that would satisfy the ensures clause, but does not return the maximum of the three integers in some cases.
c) Write a new postcondition that resolves the issue from (b), i.e. make sure that the postcondition ensures that the maximum of the three integers is always returned.
Exercise 5 Preconditions in Dafny
Suppose that you have the following function for multiplying two integers:
function Multiply(x:int,y:int): int
{
match y
case 0 => 0
case _ => x + Multiply(x,y-1)
}
a) Write a postcondition by adding an ensures clause and verify it in Dafny. Does it verify? If not, do you think the issue is the postcondition or the code itself? If the issue is the code, do not try to change the code. Just move on to Part b.
b) As you may have figured out, there is a problem where certain inputs will cause undesired behaviour. Work out what values cause this problem. Without changing the code, add a precondition, given by a requires clause. This restricts the function to only run if the precondition is satisfied. Use the precondition to rule out the invalid inputs.
Exercise 6 More postconditions in Dafny
3) Suppose that you have the following specification. The function is supposed to return true if x > y and false otherwise.
function IsGreaterThan(x:int,y:int): bool
ensures IsGreaterThan(x,y) ==> (x > y)
{
// To do.
}
a) Does the ensures clause adequately model what the function is supposed to do? Implement the function so that the postcondition is proved, but where the function returns false when x > y.
b) Modify the postcondition so that it correctly represents the desired behaviour, i.e. so that your previous implementation would fail the postcondition.