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,8e64f4db20d57eb5
X-Google-Attributes: gid103376,public
From: Peter Amey <pna@erlang.praxis.co.uk>
Subject: Re: Call by reference vs. call by value
Date: 1996/07/23
Message-ID: <Pine.SUN.3.91.960723082703.22250A-100000@erlang.praxis.co.uk>#1/1
X-Deja-AN: 169623413
references: <31F10E50.726@egr.uri.edu> <dewar.837901109@schonberg>
 <DuwxvJ.G4t@world.std.com> <dewar.837995690@schonberg>
 <Duy5ur.4Dt@world.std.com>
content-type: TEXT/PLAIN; charset=US-ASCII
organization: Praxis plc, U.K.
mime-version: 1.0
newsgroups: comp.lang.ada
Date: 1996-07-23T00:00:00+00:00
List-Id: <comp.lang.ada>


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.

Peter