Don't hardwire OS features

[Alaric B. Williams]

On  8 Dec 96 at 1:50, Francois-Rene Rideau wrote:

> >[limited specifications in Eiffel]
> > The extension beyond assert() is that they have an "implies"
> > boolean operator, the import of which is not clear. I have seen
> > written: "divisor /= 0 implies Valid()" and things like that.
> This means that Eiffel can manage several kinds
> of possible assert() for a piece of code.
> More powerful than assert(), but not much more expressive.
> Quite far away from full specifications that would allow
> to statically check for program correctness.

So what would "full specifications" look like?
 
ABW
--
Governments are merely protection rackets with good images.

Alaric B. Williams Internet : alaric@abwillms.demon.co.uk
http://www.abwillms.demon.co.uk/