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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,8e64f4db20d57eb5 X-Google-Attributes: gid103376,public From: JP Thornley Subject: Re: Call by reference vs. call by value Date: 1996/08/03 Message-ID: <234976638wnr@diphi.demon.co.uk>#1/1 X-Deja-AN: 172155051 x-nntp-posting-host: diphi.demon.co.uk references: <31F10E50.726@egr.uri.edu> x-mail2news-path: relay-4.mail.demon.net!post.demon.co.uk!diphi.demon.co.uk organization: None reply-to: jpt@diphi.demon.co.uk newsgroups: comp.lang.ada Date: 1996-08-03T00:00:00+00:00 List-Id: Felaco writes: > I keep seeing SPARK mentioned in this thread. Although I don't think > I like the sounds of it, where can I get more info about this? (Feel > free to send direct e-mail rather than post a response.) Well, no-one from Praxis has posted a response to this (although maybe someone e-mailed) and ISTR there was an earlier post in this thread asking about it, so here's a short description. The SPARK language consists of:- 1. A subset of the Ada (83) language judged to be appropriate for producing safety-critical code. It can (rather crudely) be seen as the Pascal core of Ada, with some of the good Ada features added (packages, private types and some others). 2. A number of obligatory annotations (written as Ada comments) that describe the data flow in each subprogram (the derivation relationships between the imports and the exports). The SPARK Examiner is a tool that checks for conformance to the subset and that the Ada code correctly implements the data flows in the annotations. Other features of the SPARK toolset (which I haven't used yet) are the ability to generate path functions for a subprogram (so that the V&V people can check them against the specification) and a run time error checker that either (1) proves that a piece of code cannot cause a run-time error or (2) produces proof obligations (on the caller of that code) which (if met) ensure that a run-time error cannot be caused. HTH Phil Thornley -- ------------------------------------------------------------------------ | JP Thornley EMail jpt@diphi.demon.co.uk | ------------------------------------------------------------------------