Examples for the Proofchecker
=============================

This directory contains some small examples to demonstrate the
proofchecker extension of the oasys interpreter. In order to execute these
examples you must install the Opal system with the option
'--enable-proofchecker' (disabled by default).

Simply call 'oasyspc' instead of 'oasys', this invokes the enhanced oasys
interpreter. Use 'pc <UNIT>' to start proofchecking. Other commands may be
found via the online help of oasys. Documentation is still scarce. Sort of
an introduction is the Technical Report 'Compiler Support for Specification
and Justification -- Description of a Case Study' (99-18), which may be
accessed via http://uebb.cs.tu-berlin.de/

Examples:

sNat.impl	Properties of natural numbers
sSeq.impl	Properties of sequences
sNatAux.impl	simple test and simple program synthesis (*)
Colour.impl	data type implementation
ColourOrd.impl  wrongly implemented order on colour (*)
SecureCom.impl  study for specifying secure commands (+)

The directory Sieve contains a formal proof of the Sieve-of-Eratosthenes
algorithm, following a proof given by Hoare. Call 'pc Sieve.impl' to execute
the associated proofs.

Some examples (*) produce error messages. This is intentional. The purpose
of the proofchecker extension is to catch more errors than the standard
compiler, and these structures serve to demonstrate this. SecureCom (+)
contains an unfinshed proof, because it is not clear how to prove properties
of monads.

Note that you must set the environment variable OCSPROJECT to point to the
ProjectDefs.proofchecker file in this directory before these files can be
compiled with the Opal compiler. The sources use some extensions of the Opal 
language which are switched off by default. ('oasyspc' switches these
extensions on automatically.)

Finally note that this is alpha software and only tested by its author.
The current version is 2.7c of January 2000

I appreciate any comments, bug messages and suggestions for further
improvement.


Klaus Didrich
kd@cs.tu-berlin.de
