Re: Call by reference vs. call by value

[bobduff@world.std.com (Robert A Duff)]

In article <Pine.SUN.3.91.960723082703.22250A-100000@erlang.praxis.co.uk>,
Peter Amey  <pna@erlang.praxis.co.uk> wrote:
>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.

Right, but you could equally well say that a SPARK program has by-ref
semantics.  SPARK ensures that the two are equivalent by avoiding
aliasing, as you said, and also by avoiding exception handlers.

- Bob