From: Peter Amey <pna@praxis-cs.co.uk>
Subject: Re: Assertions
Date: 1999/05/12
Date: 1999-05-12T12:26:15+00:00 [thread overview]
Message-ID: <37397272.4B2FC372@praxis-cs.co.uk> (raw)
In-Reply-To: 3736D243.1EEBF1AB@globalnet.co.uk
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/
--------------------------------------------------------------------------
next prev parent reply other threads:[~1999-05-12 0:00 UTC|newest]
Thread overview: 35+ messages / expand[flat|nested] mbox.gz Atom feed top
1999-05-10 0:00 Assertions J & A Richardson
1999-05-10 0:00 ` Assertions Marin David Condic
1999-05-11 0:00 ` Assertions Robert Dewar
1999-05-11 0:00 ` Assertions Nick Roberts
1999-05-11 0:00 ` Assertions Robert Dewar
1999-05-12 0:00 ` Assertions Dale Stanbrough
1999-05-12 0:00 ` Assertions Robert Dewar
1999-05-12 0:00 ` Assertions Tucker Taft
1999-05-12 0:00 ` Assertions Marin David Condic
1999-05-12 0:00 ` Assertions Larry Kilgallen
1999-05-12 0:00 ` Assertions Tucker Taft
1999-05-13 0:00 ` Assertions Nick Roberts
1999-05-17 0:00 ` Assertions Dale Stanbrough
1999-05-19 0:00 ` Assertions Nick Roberts
1999-05-22 0:00 ` Assertions Dale Stanbrough
1999-05-22 0:00 ` Assertions Robert Dewar
1999-05-22 0:00 ` Assertions Ray Blaak
1999-05-22 0:00 ` Assertions Robert Dewar
1999-05-23 0:00 ` Assertions Nick Roberts
1999-05-24 0:00 ` Assertions Ray Blaak
1999-05-24 0:00 ` Assertions Dale Stanbrough
1999-05-23 0:00 ` Assertions Nick Roberts
1999-05-18 0:00 ` Assertions Richard D Riehle
1999-05-19 0:00 ` Assertions Nick Roberts
1999-05-19 0:00 ` Assertions Richard D Riehle
1999-05-20 0:00 ` Assertions Ehud Lamm
1999-05-21 0:00 ` Assertions Robert Dewar
1999-05-21 0:00 ` Assertions Ehud Lamm
1999-05-21 0:00 ` Assertions Tucker Taft
1999-05-20 0:00 ` Assertions stimuli
1999-05-21 0:00 ` Assertions Richard D Riehle
1999-05-21 0:00 ` Assertions Robert Dewar
1999-05-20 0:00 ` Assertions stimuli
1999-05-12 0:00 ` Peter Amey [this message]
1999-05-12 0:00 ` Assertions Robert Dewar
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox