Accompanying files for this exercise can be found here.
This exercise focusses on proof techniques, and 'debugging' proofs.
DON'T FORGET to put the answer for the question posed in Task A,
and other observations you may have, in a report.txt, and hand that
in as part of a .zip or tarball containing all relevant Why3 files,
just as for the previous exercises.
Please, work in pairs!
You can submit these exercises in Brightspace; the deadline for submission is Tuesday 26 February 2019, 18:00.
In tree/tree.mlw, you will find a familiar definition of a binary tree, together with a function
that computes the number of leafs and the number of nodes.
Your challenge is to use Why3 to prove some very well-known facts about binary trees. As before, you are allowed to use whatever source you can find (e.g. informal proofs, proofs performed during the functional programming course). However, if you stumble across a Why3 proof by someone else (or a fellow student), only look at this after you have succeeded on your own.
tree.mlw contains a definition of nodes and leafs. Prove that for any tree, the number of leafs is
always exactly one greater than the number of nodes. This requires induction over the shape of the tree.
Write a function (or find one) height which computes the height of a tree.
Prove that a tree of height $h$ has at most $2^h$ leafs. (Hint: be mindful that power 2 x is undefined when x is negative)
There are more functions that will satisfy the last criterion. E.g., obviously a tree with $n$ leafs will have at most $2^n$ leafs.
Do you think it is possible to prove that your height function actually computes the height of a tree?
If so, what would such a proof look like? (You don't need to actually do it in Why3!).
If not, how could you convince someone of the correctness of that function?
In 1984, Morris and Jones (pdf) re-published a version of Turing's original 1949 proof of the factorial function with a commentary. (If you like reading about the history of computing science, it is worth a read, but it is not necessary for the exercise.) In it they describe that Turing's proof is incomplete, and add necessary corrections.
A translation of their corrected proof (listed as Figure A in their paper) can be seen in the folder turing/; the listed
invariants are taken straight from their paper.
If you try to verify it with Why3, you will discover that there is a problem with one of the invariants. Fix it so the program does get proven.
Morris and Jones note that the routine computes 0! correctly, but that Turing's proof only works for n > 0. Try to fix the Why3 proof so that it also works for n >= 0.