Programming Tutorials

Every practical seminar project has a complete tutorial in this appendix. A project may consist of one problem or of several staged problems. One tutorial may cover the whole sequence, but it records the result of every stage.

Mathematical exercises remain in appendix B. Practical projects use worked tutorials because the reader needs to see how the program is built, not only its final source and output.

Begin each entry with the \tutorialfor command applied to the stable project identifier and its exercise labels, followed immediately by a tutorial* environment. List several labels when one tutorial covers a staged sequence. Every practical-project label occurs in exactly one tutorial and does not occur in the mathematical solutions appendix.

Each tutorial has the following parts.

1. Problem and result. Restate the problem, the calculus or algorithm, the invariant, the concrete result, and the decidable acceptance test.

2. Representation. Choose representations for the relevant data. Explain their advantages and disadvantages, and compare them with at least one plausible alternative.

3. First complete version. Build the smallest end-to-end program that already produces a useful result.

4. Remaining cases. Add the remaining cases in the order used by the metatheory. Point out cases emphasized by the printed proof, such as capture in substitution, neutral terms, or eigenvariable conditions.

5. A failing version. Show at least one incorrect version and a named input that reveals the error.

6. Acceptance test. Run the program on the named inputs and check the expected outcomes. The check may compare exact output or decide a stated property of the output.

7. Mathematical boundary. Name the metatheorem illustrated by the program and state explicitly that running the program does not prove it.

Repository, commit, toolchain, commands, and the full raw transcript belong in appendix E. Tutorials report the concise result needed to check the construction but do not duplicate that provenance. Tutorials follow chapter order.