Browse Prior Art Database

A Proof Rule for Functions

IP.com Disclosure Number: IPCOM000128652D
Original Publication Date: 1977-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Document File: 7 page(s) / 26K

Publishing Venue

Software Patent Institute

Related People

David R. Musser: AUTHOR [+3]

Abstract

Clint and Hoare [2] gave a proof rule for functions (without side effects) which later was shown by Ashcroft [1] to be unsound. The way of avoiding the unsoundness suggested in [1] seems unattractive in that it requires "an unconventional interpretation for functional notation;" while other proof rules that have been proposed for functions are more complicated (e.g., as in [7]) or require proofs of termination for functions. This paper suggests a simple modification to Clint and Hoare's proof rule--an additional "consistency premise"--which makes it sound without requiring proofs of -termination. Although proving termination is in most cases a worthy goal, one may wish to consider functions that fail to terminate because they exit abnormally by a jump to an external label [2]. For such functions the present proof rule will be especially useful. It also permits a simpler algorithm for generating verification conditions than that described in [7], and has been implemented by the author in a verification condition generator at Information Sciences Institute. The new proof rule, like the Clint and Hoare rule, allows (and requires) the result of the computation performed by the body of a given function f to be specified as a mathematical functions of the input values, using the name f as the name of the mathematical function also. In order to make the proof rule applicable to programming languages in which nondeterministic computations are expressible, the rule includes a premise requiring that the body of the function deterministically computes its result value. Following some simple examples of use of the new proof rule, we give versions of the rule adapted to the Pascal [6] and Euclid [9,11] languages, and conclude with a discussion of the role in programming languages of function-like constructs which do have side effects.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 18% of the total text.

Page 1 of 7

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

A Proof Rule for Functions

David R. Musser

ARPA ORDER NO. 2223

ISIIRR-77-62 October 1977 INFORMATION SCIENCES INSTITUTE

46 76 Admiralty WaylMarina del ReylCalif orma 90291 UNIVERSITY of SOUTHERN CALIFORNIA (213) 822-1511

THIS RESEARCH IS SUPPORTED BY THE ADVANCED RESEARCH PROJECTS AGENCY UNDER CONTRACT NO. DAHC15 72 C 0308, ARPA ORDER NO. 2223. PROGRAM CODE NO. 3D30 AND 3P10. VIEWS AND CONCLUSIONS CONTAINED IN THIS STUDY ARE THE AUTHOR'S AND SHOULD NOT BE INTERPRETED AS REPRESENTING THE OFFICIAL OPINION OR POLICY OF ARPA, THE U.S. GOVERNMENT OR ANY OTHER PERSON OR AGENCY CONNECTED WITH THEM.

THIS DOCUMENT APPROVED FOR PUBLIC RELEASE AND SALE: DISTRIBUTION IS UNLIMITED.

Introduction

Clint and Hoare [2] gave a proof rule for functions (without side effects) which later was shown by Ashcroft [1] to be unsound. The way of avoiding the unsoundness suggested in [1] seems unattractive in that it requires "an unconventional interpretation for functional notation;" while other proof rules that have been proposed for functions are more complicated (e.g., as in [7]) or require proofs of termination for functions. This paper suggests a simple modification to Clint and Hoare's proof rule--an additional "consistency premise"--which makes it sound without requiring proofs of -termination. Although proving termination is in most cases a worthy goal, one may wish to consider functions that fail to terminate because they exit abnormally by a jump to an external label [2]. For such functions the present proof rule will be especially useful. It also permits a simpler algorithm for generating verification conditions than that described in [7], and has been implemented by the author in a verification condition generator at Information Sciences Institute.

The new proof rule, like the Clint and Hoare rule, allows (and requires) the result of the computation performed by the body of a given function f to be specified as a mathematical functions of the input values, using the name f as the name of the mathematical function also. In order to make the proof rule applicable to programming languages in which nondeterministic computations are expressible, the rule includes a premise requiring that the body of the function deterministically computes its result value.

Following some simple examples of use of the new proof rule, we give versions of the rule adapted to the Pascal [6] and Euclid [9,11] languages, and conclude with a discussion of the role in programming languages of function-like constructs which do have side effects.

Notation

University of Southern California Page 1 Dec 31, 1977

Page 2 of 7

A Proof Rule for Functions

Hoare's notation P(S)R, where P and R are predicates and S is a statement in a programming language, will be used to express the assertion that if P is true before the execution of S then R is true after the execution of S. P{S}R is vacuously true if S fails to terminate....