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: f43e6,2c6139ce13be9980
X-Google-Attributes: gidf43e6,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: 1108a1,2c6139ce13be9980
X-Google-Attributes: gid1108a1,public
From: dewar@merv.cs.nyu.edu (Robert Dewar)
Subject: Re: Safety-critical development in Ada and Eiffel
Date: 1997/08/16
Message-ID: <dewar.871740021@merv>#1/1
X-Deja-AN: 264587932
References: <33E9ADE9.4709@flash.net> <EEsF5y.F5H@syd.csa.com.au>
 <JSA.97Aug12131358@alexandria.organon.com> <33F133D7.71AC@erols.com>
 <33F25933.7F83@flash.net> <33F30341.19F7DDE6@calfp.co.uk>
Organization: New York University
Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel
Date: 1997-08-16T00:00:00+00:00
List-Id: <comp.lang.ada>


Nick says

<<There is one advantage. If your assertions are compiled, they must
conform to a set restricted style. Comments are, on the other hand very
free form. I think it is reasonable to say that the compiled
assertions are less likely to be ambiguous than if they are just
a comment. They are more likely to be correct if they have been executed
and tested.>>


That is most definitely true, however, if you restrict assertions to
executable form, that is most certainly a fierce restriction, particularly
in languages like Ada and Eiffel whose expressive power is nowhere near
that of full set theory. 

It is perfectly reasonable to have assertions in comments that are impractical
to execute, or even to talk about infinite sets where the assertions are not
even conceptually computable.

I would not rule out the utility of such assertions, though there is always
considerable value in putting assertions (or specs of any kind) into 
executable form where possible.