Re: Call by reference vs. call by value

[JP Thornley <jpt@diphi.demon.co.uk>]

Felaco <bcf@swlpts1.ssd.ray.com> 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                           |
------------------------------------------------------------------------