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







Deposit Papers 


Kulczycki, Gregory W., Sitaraman, Murali, Ogden, William F., Weide, Bruce W. and Leavens, Gary T. (2002) Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction. Technical Report 02-13, Computer Science, Iowa State University.

Full text available as:Adobe PDF

There is a later version of this eprint available: Click here to view it.


A fundamental complexity in human understanding and reasoning about imperative, object-based software systems has to do with the need to distinguish references and values of objects. It is possible to eliminate this complexity by (deep) copying values of all mutable objects, but this is too inefficient for typical, non-trivial objects. The problem of minimizing the impact of the reference-value distinction without resorting to value copying manifests itself when objects are repeated as parameters to procedures. From a software engineering perspective, we consider alternative strategies to address the repeated argument problem ranging from ones that disallow repeated arguments to more permissive ones; from ones that do not require any new programming language mechanisms to ones that need new features. We introduce a parameter passing approach that neither requires the reference-value distinction nor value copying to handle repeated arguments. We present a specification-aware, unrestricted, proof rule schema for procedure calls that is suitable for verification using alternative parameter passing techniques, separately or in combination.

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: Studies of Program Constructs (D.3.2-3)
ID code:00000293
Deposited by:Gary T. Leavens on 08 January 2003
Alternative Locations:

Available Versions of This Paper

Contact site administrator at: