On Sun, Aug 12, 2007 at 01:00:44AM -0500, JK Smith at Grid-Sky wrote:
> Three things needed in FPC:
>
> 2) Contract programming. We have to be able to show proof of correctness in
> code to prove the business value of FPC. This will be a major theme for the
> business side of software development in the future.
Actually, we (at Dept. Math/CS of TUE) have already contributed an
experimental branch to the repository for this. See branches/tue.
That project is in a stable state, ready to be merged (since January).
It is not finished (still a number of missing features).
I am to blame for the delay in taking follow-up actions; my apologies.
Documentation can be found at (in formann.zip, but also is also unzipped)
<http://www.win.tue.nl/~wstomv/software/formann/>
Basically, the current features are available (see user.pdf).
It is possible to insert assertions before, between or after
any statement, using {@ ...} syntax. These are (optionally)
compiled just like regular Assert()-statements. Furthermore,
pre- and postconditions of functions, procedures and methods
can be given. Class invariants are supported in a limited way.
Before loops the programmer can insert an invariant and a
variant function. Finally, there is support for propositions
and definitions, that act as abbreviations.
Missing are the abilities to use quantified expressions like
'for all', inheritance of class invariants, and giving pre- and
postconditions of procedures and functions in the unit header
instead of the unit implementation.
...
By default, formal annotation parsing is switched off. This
is to maintain backwards compatibility with programs that have
comments that start with [EMAIL PROTECTED] The FreePascal compiler
itself has
at least one place where a comment starts with [EMAIL PROTECTED]
To control the behavior of the compiler with respect to formal
annotation parsing, two options are made available: compiler
directives and command-line arguments.
The command-line argument -Sf switches formal annotation
parsing on.
The compiler directive {$FORMAL+} switches formal annotation
parsing on, {$FORMAL-} switches it off.
The directives take precedence.
(Please note that some formal annotation constructs make the
compiler generate run-time assertion checks. These are not
compiled into actual code if assert()-statement compilation is
switched off.)
If the argument -Aproofobl is given on the command-line, then
proof obligations for procedures and functions with pre- and
postconditions are generated (if feasible), as a LaTeX file.
(Two examples arincluded: naive.pdf, intelligent.pdf.)
The file programmer.pdf contains information for developers; it documents
how things have been implemented.
Maybe a developer can take a look, and we can discuss off-line whether
to merge this, and if so, how to proceed.
Best regards,
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
_______________________________________________
fpc-pascal maillist - fpc-pascal@lists.freepascal.org
http://lists.freepascal.org/mailman/listinfo/fpc-pascal
