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,203d1f2317947ef5 X-Google-Attributes: gid103376,public From: sgb@erlang.praxis.co.uk (Stephen Bull) Subject: Re: others clause Date: 1996/09/02 Message-ID: #1/1 X-Deja-AN: 177976732 sender: sgb@praxis.co.uk references: organization: Praxis plc newsgroups: comp.lang.ada Date: 1996-09-02T00:00:00+00:00 List-Id: In article <50d4fc$elf@fozzie.sun3.iaf.nl> geert@fozzie.sun3.iaf.nl (Geert Bosch) writes: > One of the features I'm really missing in Ada is a syntax to > specify assertions, pre- and post-conditions and invariants for > code and interfaces. Compilers wouldn't have to check these > conditions, except some simple cases like static expressions, > but they (or external programs) *could* check them and moreover > compilers could use them for optimizations. The SPARK language is a secure subset of Ada augmented by an set of annotations which allow such checks to be made by the support tool the SPARK Examiner. SPARK is developed and supported by Praxis Critical Systems. For more information please refer to our web pages: http://www.praxis.co.uk/technols/spark/sp_lang.htm -- ----------------------------------------------------------------------------- Stephen Bull Praxis Critical Systems 20 Manvers Street BATH BA1 1PX UK +1225 444700 (switchboard) +1225 739286 (direct) +1225 739281 (fax) ----------------------------------------------------------------------------- -- ----------------------------------------------------------------------------- Stephen Bull Praxis Critical Systems 20 Manvers Street BATH BA1 1PX UK +1225 444700 (switchboard) +1225 739286 (direct) +1225 739281 (fax) -----------------------------------------------------------------------------