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: Peter Amey Subject: Re: Assertions Date: 1999/05/12 Message-ID: <37397272.4B2FC372@praxis-cs.co.uk>#1/1 X-Deja-AN: 476985796 Content-Transfer-Encoding: 7bit References: <3736D243.1EEBF1AB@globalnet.co.uk> X-Accept-Language: en Content-Type: text/plain; charset=us-ascii X-Complaints-To: abuse@uk.uu.net X-Trace: soap.pipex.net 926511975 14712 194.129.236.147 (12 May 1999 12:26:15 GMT) Organization: Praxis Critical Systems Mime-Version: 1.0 NNTP-Posting-Date: 12 May 1999 12:26:15 GMT Newsgroups: comp.lang.ada Date: 1999-05-12T12:26:15+00:00 List-Id: J & A Richardson wrote: > > I have looked through the RM and can not find any refference to > assertions, pre conditions, or post conditions. > > It was my understanding that Ada 95 used assertions. > > I have also looked through a couple of webpages. > > Does Ada 95 use exceptions to work as assertions? Or am I missing > something? > The SPARK Ada subset has assertions in the form of pre/post conditions, loop invaraints etc. which are used to generate verification conditions (prrof obligations) allowing partial correctness to be established. These are not checks which are monitiored at run time. Peter -- --------------------------------------------------------------------------- __ Peter Amey, Product Manager ) Praxis Critical Systems Ltd / 20, Manvers Street, Bath, BA1 1PX / 0 Tel: +44 (0)1225 466991 (_/ Fax: +44 (0)1225 469006 http://www.praxis-cs.co.uk/ --------------------------------------------------------------------------