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,4835289e9b0eb32d X-Google-Attributes: gid103376,public From: gavin@praxis-cs.co.uk (Gavin Finnie) Subject: Re: Critical code, Ada, Eiffel, Ariane etc. Date: 1997/08/18 Message-ID: <5t9no5$7ut@erlang.praxis-cs.co.uk>#1/1 X-Deja-AN: 265033583 References: Organization: Praxis Critical Systems Ltd, Bath, U.K. Newsgroups: comp.lang.ada Date: 1997-08-18T00:00:00+00:00 List-Id: In article , Brian Rogoff wrote: > I looked at the Praxis web page, and noticed that generic units are >excluded from the Spark subset. What are the reasons for this choice? SPARK has so far totally excluded generics on the grounds of complexity, in terms of defining a formal model of generics, the additional static analysis and proof work required, and the effect on human understanding of the source code (and hence the potential for errors) when generics are used. However, we recognise that the controlled use of simple generics can assist in creating re-usable abstractions that can make code easier to structure, understand and reason about. Also, certain flaws in Ada 83's contract model have been fixed in Ada 95. We are therefore considering providing limited support for generics in a future version of SPARK. Gavin Finnie Praxis Critical Systems Ltd Tel (+44) 01225-466991 20 Manvers Street Fax (+44) 01225-469006 Bath BA1 1PX UK