Jochem Berndsen (math student at Technische Universiteit Eindhoven, NL)
extended FPC with the following facilities for formal annotation in Pascal:

  *  the scanner can recognize {@ ...} in programs.
     (controled by a command-line option, and a compiler directive)
     The ... can be a boolean assertion, pre, post, inv, or definition.

  *  the compiler can translate {@ ...} into an appropriate assert
     statement (whether this results in code depends on the -Sa flag).

  *  the compiler can extract so-called verification conditions (VCs) and
     generate a LaTeX document with all VCs.

Jochem has finished his work, including doumentation.  Note that our
research effort has not finished, and that the extensions that Jochem
made to FPC can be taken further (for instance, not all language
constructs are supported; though we don't have a concrete timeline).

It is possible to merge Jochem's extensions with the main trunk.
They are in the FreePascal SVN repository in branches/tue/.

We intend to use Jochem's facility of formal annotation in Pascal
programs in our education at TU/e.  So it would be very helpful if
that facility would be available in the standard FPC distribution.
Alternatively, we could maintain a separate branch, but that seems an
undesirable burden.

The documentation can be found here:

        <http://www.win.tue.nl/~wstomv/software/formann/>

  *  patch: incorporates formal annotation in the FPC compiler
  *  fpc-developer.*: implementation details for developers
  *  fpc-user.*: explains how to use the formal annotation facility
  *  format.tex: LaTeX definitions for expressing verification conditions
  *  naive.pdf, intelligent.pdf are two examples of extracted VCs
  *  formann.zip: an archive with all documentation