Reasoning about Procedure Calls with Repeated Arguments
		 and the Reference-Value Distinction
				  by
	       Gregory W. Kulczycki, Murali Sitaraman,
		William F. Ogden, and Gary T. Leavens

			       Abstract

In a language with clean semantics, the effect of a call to an
operation is local; this effect-restrictive property makes it easy for
software engineers to understand and reason about their code.
However, in order to give clean semantics for procedure calls in the
presence of aliasing, it is necessary to view variables that refer to
complex objects as mere references into a global store.  The reasoning
difficulties this indirection introduces do not disappear even when a
language designer or a disciplined software engineer avoids explicit
assignment of references - the more common source of aliasing.  This
is because of an independent source of aliasing that arises when
procedures are called with repeated arguments and references are
copied for parameter passing.  This repeated argument problem exists
in all well-known imperative languages.  We examine the software
engineering issues in solving the repeated argument problem,
discussing in the process the reasoning problems introduced by
aliasing and the benefits of preserving clean semantics.  A key design
consideration is avoiding value copying, both because it is
inefficient and because it cannot, in general, be automated.

Keywords: aliasing, language design, parameter passing, proof rules,
specification, verification.

2002 CR Categories:
 D.2.1 [Software Engineering] Requirements/Specifications -- languages;
 D.2.4 [Software Engineering] Software/Program Verification --
        correctness proofs, formal methods, programming by contract,
        reliability;
 D.3.1 [Programming Languages] Formal Definitions and Theory -- semantics;
 D.3.3 [Programming Languages] Language Constructs and Features --
        Procedures, functions, and subroutines;
 F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and
       Reasoning about Programs -- Assertions, logics of programs,
       pre- and postconditions, specification techniques;
 F.3.3 [Logics and Meanings of Programs] Studies of Program Constructs --
       Functional constructs, object-oriented constructs.

Submitted for publication.