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,1e5c102037393131
X-Google-Attributes: gid103376,public
From: dale@cs.rmit.edu.au (Dale Stanbrough)
Subject: Re: Assertions
Date: 1999/05/12
Message-ID: <dale-1205990834030001@dale.bu.cs.rmit.edu.au>#1/1
X-Deja-AN: 476773430
References: <3736D243.1EEBF1AB@globalnet.co.uk> <3736F549.E3DDCDEB@pwfl.com>
 <7h83lc$rd$1@nnrp1.deja.com> <37383efd@eeyore.callnetuk.com>
 <7h9p82$at0$1@nnrp1.deja.com>
X-Complaints-To: abuse@cs.rmit.edu.au
X-Trace: emu.cs.rmit.edu.au 926462042 18365 144.205.16.58 (11 May 1999
 22:34:02 GMT)
Organization: RMIT
NNTP-Posting-Date: 11 May 1999 22:34:02 GMT
Newsgroups: comp.lang.ada
Date: 1999-05-11T22:34:02+00:00
List-Id: <comp.lang.ada>

Robert Dewar wrote:

"Here are some questions to answer:
 
 1. Is an assertion a post condition that the compiler can
    rely on?
 
 2. Can assertions have side effects
 
 3. If assertions are off, are there still static semantic
    restrictions on assertions."


One solution to the first questions (as suggested before) is to
have two types of assertions. One is the

   "please check this condition at run time and don't do
    any optimisations based on what you may be able to 
    deduce from this assert"


and the other is

   "I know this condition is true, please use it to the
    fullest to provide any further optimisations that you
    can".


The latter is of course used as a supplement to the type
system. I'm not sure which of these Eiffel supports, but 
probably Anna (the Ada83 annotation toolkit) would fall into
the 1st category.


I view Q2 as being very much like the question "should functions
have side effects". I would tend to say no for assertions, but
obviously this would be hard for a compiler to check (and of
course assertions have timing side effects, which could cause
problems in a time critical program).


Dale