Exercise Set 2

The files for this exercise can be found here; this file contains a directory structure with a couple of .mlw files.

Please, work in pairs!

You can submit these exercises in Brightspace; the deadline for submission is Tuesday 12 February 2019, 12:00.

Describe any interesting findings and your answers by adding a report.txt (don't forget to mention the student id of you and your partner) in the exercise folder, and then zip/tar the entire structure (so that it includes all the files that Why3 generates)

Task A: familiarizing with Why3

  1. Install Why3, detailed instructions for that can be found here.

  2. Go into the fibo/ folder. This contains a .mlw file that contains two approaches to computing Fibonacci numbers: as a fast program, and a direct mathematical formula. This uses the int.Fibo module from the Why3 standard library which specifies Fibonacci numbers in the usual, recursive sense. You can find its definition in /usr/local/share/why3/stdlib/int.mlw.

Use Why3 to verify that all proof goals actually become proved.

(Hint: you should be able to do this the lazy way by just using the "Auto (level 2)" strategy, but also try playing around with manually splitting goals into smaller ones and running provers.)

Question

Everything should get proven, but what is actually being proven here?

Task B: Russian peasant multiplication

In russian/, you will find an almost completed implementation of Russian peasant multiplication, which multiplies two numbers by a repeated double-and-add scheme.

Instruction

  1. Complete the code by completing the odd function. Test your program by executing why3 execute russian.mlw Russian.main, then verify it in the Why3 IDE.

  2. Give a specification for the function half, and verify it.

  3. Find invariant(s) for the while loop in the function mult, so that the post-condition of mult will be verified (ignore termination for now).

  4. Prove that the function terminates by finding a suitable variant. You may need to add additional invariants to prove that this variant is suitable.

  5. The file uses int.EuclideanDivision. There is also a module int.ComputerDivision. What is the difference? Does the code still verify if you change line 5 to use int.ComputerDivision instead? If not, can you fix it?

  6. More challenging We can compute "a to the power of b" in a similar fashion, using a square-and-multiply method. Duplicate your verified version of mult as a function pow, and change the code so it implements exponentiation instead of multiplication. After you have convinced yourself that your modifications are correct (e.g. by testing it), prove your function correct in a similar fashion to how you proved mult.

    Tips: