COMP1600/6260 Foundations of Computing: Week 2
S2 2025
Practical Session 2
• This tutorial will give you practice at devising and reasoning about logical proofs.
• Use the Dafny file 02-tutorial-handout.dfy for the Dafny questions.
• Upload a plain text file called u123456.dfy (replaced by your uID) to Wattle. You may lose some marks if you do not follow these instructions correctly.
• Submit the exercises marked MA by Wednesday 6th August, 2025, 09:00 via Wattle. Late submis-sions will score 0.
Exercise 1 Dessert
Consider the following incomplete lemma:
lemma Dessert(p:bool, q:bool, r:bool, s:bool)
ensures (p ==> r){
}
There is a dessert on the table. Let p represent that the dessert is a mud cake. Let q represent that the dessert contains chocolate. Let r represent that the dessert is tasty. Let s represent that the dessert has raspberry filling. We want to conclude that if the dessert is a mud cake, then it is tasty, represented by the ensures clause above. However, we only know the following facts:
• If the dessert contains chocolate, then it is tasty.
• If the dessert has raspberry filling, then it is a mud cake or it is tasty.
• If the dessert is a mud cake, then it has raspberry filling.
• If the dessert is a mud cake, then it contains chocolate.
(a) Complete the lemma in Dafny. Use one or more of the given facts to write requires clauses, so that the lemma satisfies the ensures clause. Note: you may not need all of the facts. You must use only the minimum set of facts that are necessary.
(b) Give a logical argument for the proof (i.e. without Dafny), stating which logic rules you used at each step. Write your answer in a comment in your Dafny file.
Exercise 2 Weather
Consider the following incomplete lemma:
lemma Weather(p:bool, q:bool, r:bool, s:bool)
ensures (!p){
}
Let p represent that it is winter. Let q represent that the weather is cold. Let r represent that it is snowing. Let s represent that there is frost. We want to conclude that the weather is not winter, represented by the ensures clause above. However, we only know the following facts:
• If it is snowing, then it is winter.
• There is no frost.
• If it is winter, then the weather is cold.
• If there is no frost, then the weather is not cold.
(a) Complete the lemma in Dafny. Use one or more of the given facts to write requires clauses, so that the lemma satisfies the ensures clause. Note: you may not need all of the facts. You must use only the minimum set of facts that are necessary.
(b) Give a logical argument for the proof (i.e. without Dafny), stating which logic rules you used at each step. Write your answer in a comment in your Dafny file.
Exercise 3 Mystery Mansion (MA, 6+4 credits)
Consider the following incomplete lemma:
lemma DinnerParty(..)
{
...
}
During a dinner party, a guest, Mina, realises that her valuable necklace has been stolen. Work out who stole the necklace, given the following clues.
• If Lucy stole the necklace, then the necklace was made only of gold.
• The necklace was a family heirloom.
• The necklace was in the library or Lucy was wearing a green dress.
• If the necklace was a family heirloom, then it was made only of silver or Jonathan stole it.
• If Lucy was wearing a green dress, then the necklace was made only of silver.
• If Mina was wearing a red dress, then Jonathan stole the necklace.
• The dinner party was held in a mansion and Lucy was not wearing a blue dress.
• If Lucy did not steal the necklace, then Mina was wearing a red dress.
• If the necklace was in the library, then it was made only of silver.
(a) Complete the lemma in Dafny. Use one or more of the given facts to write requires clauses, so that you can work out which guest is the thief. You will need to write the ensures clause as well as the required clauses. Note that the word “or” in the clauses should be used in the logical sense. You may not need all of the facts. You must use only the minimum set of facts that are necessary.
(b) Give a logical argument for the proof (i.e. without Dafny), stating which logic rules you used at each step. Write your answer in a comment in your Dafny file.
Exercise 4 Boolean formulae evaluation
This exercise is to be completed by hand, not with Dafny. For each of the following, either prove that the argument is valid or give a counterexample to show that it is invalid.
(a)
p → q
q → p
Therefore, p ∨ q
(b)
p
p → q
¬q ∨ r
Therefore, r
(c)
p ∨ q
p → ¬q
p → r
Therefore, r
(d)
p ∧ ¬q → r
p ∨ q
q → p
Therefore, r