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,ab9378bfb1a6fc98 X-Google-Attributes: gid103376,public From: Peter Amey Subject: Re: Call by reference vs. call by value Date: 1996/07/26 Message-ID: #1/1 X-Deja-AN: 170629605 references: <96072514363025@psavax.pwfl.com> content-type: TEXT/PLAIN; charset=US-ASCII organization: Praxis plc, U.K. mime-version: 1.0 newsgroups: comp.lang.ada Date: 1996-07-26T00:00:00+00:00 List-Id: On Thu, 25 Jul 1996, Marin David Condic, 407.796.8997, M/S 731-93 wrote: > Peter Amey 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