(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