This exercise should take less time than the previous weeks.
As before, put any observations you may have, in a report.txt, and hand that
in as part of a .zip or tarball containing all relevant Why3 files.
Please, work in pairs!
Submit this exercise in Brightspace; the deadline for submission is Tuesday 5 March 2019, 18:00.
This is a continuation of Task B of exercise 4. Up till now, we have ignored integer overflow (as Turing did), and assumed a computer that supports integers of arbitrary size.
Turing's computer had 80 bits integers; today 64 bits are more natural. So, modify your verified version (or if you failed, use the provided solution) so that it works on 64-bit integers.
Use mach.int.UInt64 and modify the signature of fac so it operates on uint64.
The preconditions of some operations will now not hold. Feel free to make minor changes to the code (which do not alter its meaning) to fix this.
Figure out what a maximum n is for which fac still computes factorial correctly, and verify using Why3 that fac indeed computes correctly for inputs up to that maximum value.
Use Why3 to extract C code from your .mlw file.
Note: you will need to replace the absurd statement with a simpler return statement that returns your favourite
64-bit integer.
Does the final C code look reasonable to you?