Browse Prior Art Database

THE VALIDITY PROBLEM OF THE 9l-FUNCTION

IP.com Disclosure Number: IPCOM000128298D
Original Publication Date: 1968-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 13 page(s) / 28K

Publishing Venue

Software Patent Institute

Related People

Zohar Manna: AUTHOR [+4]

Abstract

Abstract: Several methods for proving the weak and strong validity of algorithms are presented. For proving the weak validity (i.e., correctness) we use satisfiability methods, while for proving the strong vali- dity (i.e., termination and correctness) we use unsatisfi- ability methods. Two types of algorithms are discussed; recursively defined functions and programs. Among the methods we include known methods due to Floyd, Manna,, and,-McCarthy. All the methods will be introduced quite informally by means of an example (the 91-functicn).

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

Page 1 of 13

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

THE VALIDITY PROBLEM OF THE 9l-FUNCTION

by Zohar Manna Amir Pnueli

Abstract: Several methods for proving the weak and strong validity of algorithms are presented. For proving the weak validity (i.e., correctness) we use satisfiability methods, while for proving the strong vali- dity (i.e., termination and correctness) we use unsatisfi- ability methods. Two types of algorithms are discussed; recursively defined functions and programs. Among the methods we include known methods due to Floyd, Manna,, and,-McCarthy. All the methods will be introduced quite informally by means of an example (the 91-functicn).

The research reported here was supported in part by,the Advanced Research Projects Agency ofthe Office of the Secretary of Defense (SD-183)

THE ALGORITHMS

Let us consider t he function f defined recursively as:113

(Equation Omitted)

with some given domain D total predicate p(x) over D [ i.e., mapping D into fT, F)I and total functions g(x) and h(x) [mapping -D into DI.

Given an element x C D 1~ f is said to converge for x I if the recursive process for computing f(x) terminates in a finite number of steps and with some definite value for f(x)

For example, if

(Equation Omitted)

we obtain:

(Equation Omitted)

) Here, f converges for

(Equation Omitted)

. but for

(Equation Omitted)

we obtain

(Equation Omitted)

then 0 else f(O) and therefore f does not converge for x 0

Stanford University Page 1 Dec 31, 1968

Page 2 of 13

THE VALIDITY PROBLEM OF THE 9l-FUNCTION

Given a total predicate *(x, y) over D 2 we shall say,that:

1. f is weakly valid (with respect to if

for every x C D if f converges for x then *(x, f(x)) and 2. f is strongly valid (with respectto ~f) , if

for every x C D f converges for x and *(x, f(x))

[11 See McCarthy [1962J[19631. [21 10=1 means 'is defined by'. For illustration we shall use.

1. the function defined as f with D I (the integers

(Equation Omitted)

and

2. the predicate Z(x, Y) over 1 2 defined as:

(Equation Omitted)

The function f can also be described by a program P (Figure 1).

Given an element x E D J. the program P is said to terminate for x if the execution of the program reaches the exit point. In this case, the final value of y will be denoted by P(x)

Moreover., given a total predicate *(x,, y) over D 2 . we shall say that:

1. P is weakly valid (with respect to if

for every x E D if P terminates for x then *(x, PW) and 2. P is,strongly valid (with respect to if

for every x E D P terminates for x and *(xP PW)

The reader can verify easily that for every given predicate

f is weakly [strongly] valid (with respect to if and only if

P is weekly [strongly] valid (with respect to

For illustration we shall use the program T~ (Figure 2) which is obtained from Figure 1 with D = I (the integers),

(Equation Omitted)

. i.e., the p . rogram T~ corresponds to the function 2.

(Image Omitted: Figure 1:, The Program P)

(Image Omitted: Figure,2: The Program :)

St...