Browse Prior Art Database

Verification of Algorithms Written in a Simple High Level Language

IP.com Disclosure Number: IPCOM000089195D
Original Publication Date: 1977-Sep-01
Included in the Prior Art Database: 2005-Mar-04
Document File: 5 page(s) / 20K

Publishing Venue

IBM

Related People

Evangelisti, CJ: AUTHOR [+2]

Abstract

For a subset of PL/I, a method is described of [1] mapping PL/I into PL/R, a hardware language, [2] verifying the consistency of such programs against other versions of the programs, and [3] using the algorithm VERIFY in a new manner. The subset of PL/I discussed consists of assignment statements with Boolean and arithmetic operators -- if-then-else statements and :DO statements. The method could be extended to other statements. A method of transformation of such 'control' programs into PL/R is described. Having the Program in PL/R, RTRAN is used to translate it into a Regular Logic Design (RLD). Thence a method is described of determining the consistency, in an effective manner, relative to another version of the program.

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

Page 1 of 5

Verification of Algorithms Written in a Simple High Level Language

For a subset of PL/I, a method is described of [1] mapping PL/I into PL/R, a hardware language, [2] verifying the consistency of such programs against other versions of the programs, and [3] using the algorithm VERIFY in a new manner. The subset of PL/I discussed consists of assignment statements with Boolean and arithmetic operators -- if-then-else statements and :DO statements. The method could be extended to other statements. A method of transformation of such 'control' programs into PL/R is described. Having the Program in PL/R, RTRAN is used to translate it into a Regular Logic Design (RLD). Thence a method is described of determining the consistency, in an effective manner, relative to another version of the program. This involves the usage of the algorithm VERIFY applied to compute a generalization of "primitive D-cubes of failure" (gpdcf -- terminology peculiar to the D-algorithm. Having computed a gpdcf, the D-algorithm is invoked to compute a test determining the inequivalence of unsuspected portions of the program. For some portions of the program the new version should not be equivalent to the old version. For others they should remain the same; these are the portions for which discriminating tests are sought. The algorithm presented here can ascertain which is the case for small changes in programming systems.

The problem of verifying that programs are correct is a difficult and important one. Here the discussion is restricted to a subset of PL/I. Furthermore, only the proof of consistency of a program with another version of the program is of concern -- a considerably less difficult problem than proving correctness in the abstract.

What is done first is to define a method of transforming a PL/I program into PL/R [1], a hardware specification language. Thence by means of a compiler RTRAN [1] the PL/R is transformed into a Regular Logic Design (RLD) [2]. Assuming another design -- in general a version of the original program -- the D- algorithm [3] is applied to the verification problem [4]. Strictly speaking, the second design is assumed to be a small variation of the original PL/I program, say just one statement. The differences between the two programs are transformed into PL/R. Since the implementations from PL/I to PL/R and from PL/R to RLD are modular, the RLD implementations will be identical almost everywhere. In effect this permits the representation of the design change as a failure of a logic design and the employment efficaciously of the D-algorithm to compute tests distinguishing the two designs if such tests exist. First, the means of translating PL/I into PL/R will be described.

A sequential program is executed sequentially, one instruction at a time, whereas in hardware operations they are simultaneous. A problem: how to represent sequential operations in hardware.

The solution that has been devised wilt be described. A shift register, c...