Exercises for Week 05

As usual the handin should consist of two files:

• a .v file with your solutions; and
• a succinct .pdf file containing your report.

The report should highlight only a few of the mystery functions (less is more), but with a proper introduction and a proper conclusion.

Exercise 00

1. The index of concepts for this week is in a separate chapter. Peruse it and make sure that its entries make sense to you (otherwise, click on them to check them out).
2. The lecture notes start with updates (Chapter Updates). Make sure to check them out regularly, as they reflect the development of the lecture.
3. Do take the time to peruse the lecture notes of this week and to reproduce their technical content.
4. If you haven’t done that in your report for Week 04, summarize your current understanding of the tutorial about fold-unfold lemmas.

Mandatory exercises

• Exercise 00: reflecting on the material of this week

• Figure out as many mystery functions as you have the time for in the accompanying file.

  Make sure that you do treat

  • the mystery function about binary trees (mystery_function_19),
  • a vacuous specification, and
  • an ambiguous specification.

  Reminder from Chapter Specifications in Week 03:

  Some specifications are vacuous (no functions exist that satisfy them), some specifications are ambiguous (several distinct functions exist that satisfy them), and some specifications are neither (exactly one function exists that satisfy them).

  Among the specifications of the mystery functions, some are vacuous, some are ambiguous, and some are neither. You are being asked to treat at least one specification that is vacuous, at least one specification that is ambiguous, and as many others as you have the time for. (Which of course means that all of the above needs to be explained in your report, in archival form.)

Version

Created [16 Feb 2024]