NetNews Usenet Archive 1992 #19/NN_1992_19.iso/spool/comp/lang/eiffel/1080

Text File | 1992-08-23 | 3.4 KB | 84 lines

Newsgroups: comp.lang.eiffel
From: [e-mail] (Trevor Nash)
Path: sparky!uunet!pipex!demon!holon!tcn
Subject: system-level validity
Distribution: world
References: <[e-mail]>
Organization: .
Lines: 71
Date: Sun, 23 Aug 1992 16:00:01 +0000
Message-ID: <[e-mail]>
Sender: [e-mail]


In article <[e-mail]> [e-mail] writes:

>    "Does ISE Eiffel 3.0 perform system-level validity checking?"

Fair question, but poorly phrased: having read the definition of system
validity in Eiffel The Language, a yes or no to this is inadequate: see
later.  And why pick on ISE - I'd like to hear what Sig have to say.
In particular it is important to know what the compiler does with programs
which are system invalid: its not clear that refusing to compile them is
a good idea.

> I only ask because I strongly believe that 3.0 vendors should be up
> front about this very important issue; after all, is a compiler that
> only performs 99% of the possible static checking any long term use,
> especially when Eiffel is trumpeted as robust?

Come on Mike, this is a bit OTT isnt it?  Eiffel claims to be more robust
than most other languages, not that it is impossible to write an incorrect
Eiffel program.  I wonder how many real errors you expect to find with the
system-level checks that are not trapped by the class-level checks?  And
do you realise that a system-invalid program is not necessarily incorrect?

You seem to view the question of system validity as if it was simply a
further type-check that the compiler writer has chosen not to implement.
Its actually much more complicated than this:
I would like to quote the example from ETL to clarify this and bring out a
couple of other points for discussion.

(this is abridged from p359 of ETL)

    a:X    -- exports feature 'proc'
    b:Y    -- Y is an hier of X, and hides (does not export) 'proc',
        -- which thus allows 'proc' to violate the class invariant
    !!b
    if false then a:=b end
    a.proc

Cleary if when a.proc is executed, a is ever dynamically of type Y you get
into trouble through a broken class invariant.  But I can prove this
never happens.  A compiler writer can either:

1) Not bother to check system validity, and silently generate correct code.
2) Flag it as system invalid, but generate correct code anyway.
3) Flag it as system invalid and refuse to generate code.
4) Implement a cleverer system validity check than that defined by ETL, and
   silently generate correct code (i.e. it does the flow analysis)

Which of these solutions conform to the standard defined by ETL, and thus
earn the name Eiffel?  I would say all with the possible exception of 3 since
this seems to go against the reasoning in ETL for leaving the 'type holes' in
the language in the first place, i.e. it rules out a significant number of
useful programs.

A couple of options which I think should be ruled out:
5) Flag it as system invalid, and generate bad code -- i.e. the code
   generated for a.proc gets it wrong even when a is dynamically of type X
6) Silently generate bad code.

How useful is 2?  In ETL Meyer puts forward the view that in practice very
few programs are class valid but system invalid (p364).  I would add the
further conjecture that of these most are also correct.


> ps. I know the people at ISE are doing a very difficult job, no
> criticism is intended.

Seconded.  I only hope they read this far :-)

Trevor Nash
[e-mail]