Browse Prior Art Database

ON THE GENERATION OF LOOP PREDICATES FOR FLOW CHART PROGRAMS OPERATING ON ARRAYS

IP.com Disclosure Number: IPCOM000148752D
Original Publication Date: 1978-May-15
Included in the Prior Art Database: 2007-Mar-30

Publishing Venue

Software Patent Institute

Related People

Ellozy, Hamed A.: AUTHOR [+2]

Abstract

Hamed A. Ellozy

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 13% of the total text.

Page 1 of 30

RC 7121 (#30493) 5/15/78
Computer
Science 27 pages

ON THE GENERATION OF LOOP PREDICATES FOR FLOW CHART PROGRAMS OPERATING ON ARRAYS

Hamed A. Ellozy

Computer Sciences Department


IBM Thomas J. Watson Research Center Yorktown Heights, New York 10598

Abstract: This paper describes a method for the generation of loop predicates (or invarianl assertions) for flow chart programs operating on arrays. The technique described is an applica- tion of difference equations.

[This page contains 1 picture or other non-text object]

Page 2 of 30

LIMITED DISTRIBUTION NOTICE
This report has been submitted for publication elsewhere and
has been issued as a Research Report for early dissemination
of its contents. As a courtesy to the intended publisher, it
should not be widely distributed until. after the date of outside
publication.

Copies may be requested from:
IBM Thomas J. Watson Research Center
Post Office Box 218
Yorktown Heights, New York 10598

[This page contains 1 picture or other non-text object]

Page 3 of 30

I. LA RAISON D'ETRE

One of the major difficulties plaguing the current program validation systems of the Floyd type is the determination of the so-called invariant assertions that must be supplied for each loop in the flowchart program. Several attempts at solving this problem have been undertaken; notable among them are the works of Katz and Manna C 1 1, Wegbreit I: 2 I, Elspas et al. C 3 I

and Caplain C 4 1.

 Katz and Manna C 11 attempt, via heuristics, to derive loop invariants from the input and output assertions and/or partially specified inductive assertions within the loop body. More precisely, given a flowchart program with input variables x which remain unchanged during execution (essentially a means of preserving the initial values of the program variables), program variables y (used as temporary storage during execution) and output variables z (assigned values only at the end of execution); given an input predicate +(x) which places restrictions on the values of the inputs variables and output predicate Q(Z) which indicates the
, desired relation between the input and output variables, the objective is then to cut all loops and attach appropriate inductive assertions to every cut point, such assertions being sufficiently strong to prove ~ ( z )
by assuming +(x).

Katz and Manna proceed to define heuristics and rules for tackling two general approaches for the solution of the problem at hand:

   (a) top-down approach in which the assertions are obtained by analyzing the predicates known to be true at the entrances and exits of the loop and

   (b) bottom-up approach in which the assertions are obtained directly by an analysis of the statements of the loop.

They further distinguish between the case of loops of programs without arrays and those with arrays, since the assertions involving quantification over the indices of arrays...