Path: utzoo!attcan!uunet!mcsun!ukc!stl!pgh
From: pgh@stl.stc.co.uk (P.G.Hamer)
Newsgroups: comp.lang.eiffel
Subject: Re: Exceptions and Assertions
Message-ID: <3354@stl.stc.co.uk>
Date: 6 Sep 90 10:55:47 GMT
References: <723@tetrauk.UUCP> <404@eiffel.UUCP>
Sender: news@stl.stc.co.uk
Reply-To: "P.G.Hamer" <pgh@stl.stc.co.uk>
Organization: STC Technology Limited, London Road, Harlow, Essex, UK
Lines: 42

In article <404@eiffel.UUCP> bertrand@eiffel.UUCP (Bertrand Meyer) writes:
>>This is only a step towards answering Mr. Jones's broader question.
>Should we tend towards a situation where precondition checking
>will always be on, even in a released software product?
>-- 
>-- Bertrand Meyer

Which raises the even broader question. Can at least some preconditions be
expressed so that they can be checked at compile time? In which case the 
there is zero run-time overhead, and *much more importantly* some classes
of error can be *guaranteed* not to occur (and hence there is no potential
exception to consider).

The language NIL claimed to support an interesting class of such compile
time checks using a concept called 'typestate'. 

Basically it added a form of context-sensitive type checking. A finite state
machine was defined for each object type giving: its major states; the
operations that were legitimate in each state; and the resultant state (or set
of possible states). Not only the type but the state of parameters is given. By
using data flow analysis it is possible to verify that an object can never have
an operation performed on it when it is in an unsuitable state.

For example, a stack might have three states; empty, full, and partially-full;
and pushing onto a full stack or popping from an empty one is (defined to be)
illigitimate. Programs which pushed onto a stack which was not demonstrably 
non-full (ie with a history of: just created and hence empty, just popped, just
tested for non-fullness, or an input with a stateset excluding full) would
generate compile time errors.

For details of what seems to be a very powerful idea  see -

Typestate: a programming language concept for enhanced software reliability.
R.E. Strom.
IEEE Trans S.E.
12(1), Jan 86, pp  157-171

NIL was (is?) an experimental language for distributed processing, with several
unusual features. Some of these undoubtably made typestate checking easier. I
don't how possible it would be to add it to a language such as Eiffel. 

Peter