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: 103376,cd5c71f09395807a
X-Google-Attributes: gid103376,public
From: dewar@merv.cs.nyu.edu (Robert Dewar)
Subject: Re: Assertions in Ada
Date: 1997/08/21
Message-ID: <dewar.872218059@merv>#1/1
X-Deja-AN: 267788183
References: <adaworksEF8qn5.I15@netcom.com>
 	<EF9nDu.EIK.0.-s@inmet.camb.inmet.com>
 <JSA.97Aug21183650@alexandria.organon.com>
Organization: New York University
Newsgroups: comp.lang.ada
Date: 1997-08-21T00:00:00+00:00
List-Id: <comp.lang.ada>


Jon Anthony says

<<b) If a) is the expectation, then why was this pragma left out of the
   standard??  Just hadn't thought of it at the time? (oops that makes
   3)>>


It is one thing to stick this into an implementation, quite another to
formally define what you mean. In particular the whole issue of whether
the compiler can use the assertion involves some tricky business. We
found that different people had very different ideas in mind.

In GNAT (I can't speak for the other vendors)

pragma Assert (X);

is *exactly* equivalent to

  if not X then
     raise System.Assertions.Assert_Failure;
  end if;

This is a simple definition, but it is not at all what some people want. They
argued that the assert statement should not be allowed to affect the program
in any way (this is quite tricky to define exactly, in fact there is more
than one possible definition), but clearly the above equivalence does not
meet this requirement, because the compiler can assume a postcondition of
X after the assert.

We could not resolve this issue, so the feature got omitted. It's always
surprising (especially to those who do not have experience in language
design) how the simplest appearing things can turn out to be very complex.