From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,a48e5b99425d742a
X-Google-Attributes: gidfac41,public
X-Google-Thread: f43e6,a48e5b99425d742a
X-Google-Attributes: gidf43e6,public
X-Google-Thread: 103376,a48e5b99425d742a
X-Google-Attributes: gid103376,public
X-Google-Thread: 1108a1,5da92b52f6784b63
X-Google-Attributes: gid1108a1,public
X-Google-Thread: 107d55,a48e5b99425d742a
X-Google-Attributes: gid107d55,public
From: rfraer@sophia.inria.fr (Ranan Fraer)
Subject: Re: Please do not start a language war (was Re: Papers on the
 Ariane-5 crash and Design by Contract
Date: 1997/03/20
Message-ID: <5gr478$esd@news-sop.inria.fr>#1/1
X-Deja-AN: 226952772
Sender: rfraer@arthur.inria.fr (Ranan Fraer)
References: <332B5495.167EB0E7@eiffel.com> <tz8ohcjv7cc.fsf@aimnet.com>
 <dewar.858568071@merv> <5giu3p$beb$1@news.irisa.fr>
 <JSA.97Mar17180249@alexandria> <332f2ab7.1115984@news.wr.com.au>
Organization: INRIA, Sophia-Antipolis (Fr)
Newsgroups: 
 comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada,comp.lang.java.tech
Date: 1997-03-20T00:00:00+00:00
List-Id: <comp.lang.ada>


Kent Tong writes:

|> This is a rather uninformed statement. Have you seen anything
|> about the B method and the Abstract Machine Notation it uses?
|> Its support for pre/post conditions even goes further to include
|> component refinements/implementations.

I'd like to add that the B method is very close to Eiffel in stressing
the role of assertions in program development (not surprisingly, Bertrand Meyer 
and Jean-Raymond Abrial, the inventor of the B method have worked together).

However, the B method goes one step further by requiring to effectively prove
the validity of each assertion. A great deal of the proofs can be dealt with
automatically, but some of them have to be tackled interactively by the user.
Although very tedious, this approach might increase the confidence in the
final product and some standards already require formal proof in the development
of safety-critical systems.

Nonetheless, to fully exploit the potential of the B method one would have to
drop the existing code and redesign all of it from a formal specification.
This was out of question in the case of Ariane, so an alternative would
have been to do plain program verification in the Floyd-Hoare style by
annotating the existing code with assertions and using a program verifier
for Ada like Penelope/Larch.

--- Ranan Fraer
e-mail: rfraer@sophia.inria.fr  
WWW page : http://www.inria.fr/croap/personnel/Ranan.Fraer.html