[fpc-pascal] Need three things (follow-up on contracts)

[Tom Verhoeff]

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 {@.  The FreePascal compiler itself has
	at least one place where a comment starts with {@.

	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