Re: Call by reference vs. call by value

[Peter Amey <pna@erlang.praxis.co.uk>]

On Thu, 25 Jul 1996, Marin David Condic, 407.796.8997, M/S 731-93 wrote:

> Peter Amey <pna@ERLANG.PRAXIS.CO.UK> writes:
> >This is another Ada feature well covered by the SPARK subset.  The rules
> >of SPARK (which are checked by the SPARK Examiner) prohibit all cases
> >of aliasing where program meaning might be affected by the parameter
> >passing mechanism used. A SPARK program has copy-in, copy-out semantics
> >regardless of the compiler used to compile it.
> >
[snip]
>     I'd favor passing parameters by reference (for speed) over copy
>     mechanisms ...

SPARK does not enforce copying it simply ensures that the program _behaves_ 
as if parameters were copied even if the compiler passes by reference.  

I agree with many of your comments, but for the most critical of systems
not worrying about the obscure/rare error cases is not an option. Also,
tightening the language to the point where we can reason properly about
program meaning allows us to tackle the serious problem you identify of
the getting the logic wrong.  The kinds of formal verification we
routinely practice on critical code are simply not feasible if the meaning
of a source text in not fully defined. 

Peter