Description
Using PBC
==
Proof by contradiction, like any other rule, can be used to justify claims. Subproofs can be confusing or require additional work. Therefore, PBC should be avoided if possible. When trying to prove a claim, there is a simple test on whether PBC should be used to prove the claim. Only in these cases should PBC be used:
1. The claim is just an atom i.e. p(x), or q
2. The top level of the claim is or i.e. (p->q) V r
3. The top level of the claim is the existential quantifier i.e. ∃ x p(x)
However sometimes, these can be justified without PBC. Sometimes these *can* be done directly. In any other case, there is a direct approach to build the claim using the previously justified claims.
Problems
==
1. (6 Points)
a. *Our hero Harry, has won the Triwizard tournament and needs his winnings in Knuts. He knows a goblin who will trade Galleons for Sickles and another who will trade Sickles for Knuts. Harry intends to invest these Knuts in the Weasley twin’s business, Weasley’s Wizard Wheezes.*
b. Add the logical steps to program 1.logika to prove that converting 1000 Galleons to Knuts by first converting to Sickles then Knuts provides the same number as a direct conversion (493 Knuts per Galleon).
c. The final assertion ensures that the value of the 2-stage conversion is the value of the direct conversion.
2. (6 Points)
a. *Weasley’s Wizard Wheezes does not provide Knuts as change. They round to the “nearest” Sickle. To ensure they don’t lose money, they want 15 Knuts to round down.*
b. Add the logical steps to program 2.logika to show that when less than 16 Knuts should be returned, the number of Sickles is rounded down and when 16-or-more Knuts should be returned the number of Sickles is rounded up.
c. The three middle assertions check this behavior.
d. The three bottom assertions check to make sure the Knuts are converted properly to Sickles.
3. (4 points)
a. *The Weasleys twins are worried they may lose money, and want stronger proof that the “nearest” is always in the favor of the business.*
b. Copy your entire working solution from 2.logika into 3.logika. Uncomment the last assertion at the bottom. Expand the existing logika proofs to satisfy the new assertion.
c. The final assertion checks that the total error (the difference in the amount given back as Sickles versus the value which should be returned in Knuts) is always 15-or-less; but when it is 15, the change rounds down (in favor of the business).
4. (8 points)
a. *To more efficiently accomplish her Arithmancy charts, Hermione needs to quickly approximate square roots. We have provided her with a program which calculates the ceiling of the square root for numbers above 1. The ceiling is the smallest natural number AT LEAST as large the value you want (we over-estimate the square root when the number is not a perfect square).*
b. Add the logical steps to program 4.logika to show that the assertions at the end of the program hold.
c. The Loop invariant is that we have not yet guessed the correct number.
d. The first assertion shows that the guess squared is at least as big as the number you started with.
e. The second demonstrates that the guess cannot be any smaller.
5. (8 points )
a. *The Weaslesy twins have finally paid Harry back for his investment in Weasley’s Wizard Wheezes. Tragically, they have paid him back in the Knuts they did not give out as change. We have provided Harry a program to convert the Knuts into Galleons so he can figure out if he made money through his investment.*
b. Add the logical steps to program 5.logika to show that the assertions at the end of the program hold.
c. The first assertion and the Loop invariant show that the total value has not changed (we did not create or destroy money, we just converted).
d. The last two assertions ensure that no more Sickles can be converted into Galleons and no more Knuts can be converted into Sickles.
What to submit
==
Commit and push your project containing the solutions to your github repository (see videos) before the deadline. A good practice is to commit/push whenever meaningful progress is made (like you finish a question or fix a bug).
