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

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.

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

Abstract

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.

Available Versions of This Paper

• Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction (deposited 08 January 2003) [Currently displayed]
  • Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction (deposited 15 December 2003)