[fpc-devel] Request to merge formal annotation facility into main trunk

[Tom Verhoeff]

(I already mailed this off-list to Florian, but it might be better to
discuss it on the list.)

We had a student (Jochem Berndsen) who 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 (though we don't have a concrete timeline).

Is it possible to merge Jochem's extensions with the main trunk?
They are in the SVN repository in branches/tue/.

We would like 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
  *  programmer.pdf provides implementation details for developers
  *  user.pdf explains how to use the formal annotation facility
  *  format.tex contains LaTeX definitions for expressing proof obligations
  *  naive.pdf, intelligent.pdf are two examples of extracted
     proof obligations
  *  formann.zip is an archive with all documentation

I can also write something in the wiki (or another part of the documentation;
where?).

Looking forward to your response,

	Tom
-- 
E-MAIL: T.Verhoeff @ TUE.NL     | Dept. of Math. & Comp. Science
PHONE:  +31 40 247 41 25        | Technische Universiteit Eindhoven
FAX:    +31 40 247 54 04        | PO Box 513, NL-5600 MB Eindhoven
http://www.win.tue.nl/~wstomv/  | The Netherlands