archives

Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Kulczycki, Gregory K., Sitaraman, Murali, Ogden, William F. and Leavens, Gary T. (2003) Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction. Technical Report TR02-13a, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

This is the latest version of this eprint.

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
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Studies of Program Constructs (D.3.2-3)
ID code:00000324
Deposited by:Gary T. Leavens on 15 December 2003
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/TR02-13/TR.ps.gz ftp://ftp.cs.iastate.edu/pub/techreports/TR02-13/TR.pdf

Available Versions of This Paper



Contact site administrator at: ssg@cs.iastate.edu