Browse Prior Art Database

Program Behavior Definition Generator

IP.com Disclosure Number: IPCOM000045620D
Original Publication Date: 1983-Apr-01
Included in the Prior Art Database: 2005-Feb-07
Document File: 5 page(s) / 18K

Publishing Venue

IBM

Related People

Larson, LE: AUTHOR

Abstract

Introduction. A process of generating a metalanguage definition of a program from a program specification is described. The metalanguage definition is useful for verifying the correct program behavior by a program auditor. In operation, the generator performs two main operations. The first operation is the creation of the metalanguage program description. The second is the insertion into the program specification (implementation) of the statements needed for the verification process. This description pertains to the generation of the behavior data and the corresponding change to the program specification and not to the verification process or error correction to be invoked.

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

Page 1 of 5

Program Behavior Definition Generator

Introduction.

A process of generating a metalanguage definition of a program from a program specification is described. The metalanguage definition is useful for verifying the correct program behavior by a program auditor. In operation, the generator performs two main operations. The first operation is the creation of the metalanguage program description. The second is the insertion into the program specification (implementation) of the statements needed for the verification process. This description pertains to the generation of the behavior data and the corresponding change to the program specification and not to the verification process or error correction to be invoked.

Operation.

A computer program can be thought of as the existence of a computer state which can be named. The name can be translated into a symbol or character which can be stored in a computer and processed. If the sequence of symbols produced by a series of programs is placed one after the other, the result is a string of symbols or characters satisfying a set of rules. Because a string of symbols constitutes a language, it is possible to apply interpreter technologies to the problem of verifying program operation or behavior. The problem is to generate the metalanguage for the specification of the behavior and to insert into the program implementation the required communications to the program auditor.

This operation is best illustrated by examining a program specification provided in a decision table format and observing the transformations taken. The example consists of three decision tables defined as follows: TOP 12

I=10 YN

INCLUDE DOJ 1

I=I+1 2

/* LOOP */ X

TOP='1'B X

I=1

RETURN

INCLUDE DOKT

DOJ 12

J=10 YN

CALL, DOK 1

J=J+1 2

/* LOOP */ X

DOJ='1'B X

J=1

/* END OF DOJ*/

DOKT 12

K=10 YN

1

Page 2 of 5

PUT LIST (I,J,K) 1

K=K+1 2

/* LOOP */ X

DOKT='1'B X

DOK:K=1

RETURN

Step 1.

The generator analyzes the decision table and adds invocations of the BEHAVIOR function to communicate to the program auditor the execution state of the program specified in the decision table. The BEHAVIOR function invocations are added to the initialization and termination stubs of the decision tables as well as the action stubs.

The invocations appear at the beginning and end of each rule (initialization and termination) which may be combined into one invocation if there are no intervening program invocations via CALL or INCLUDE.

STEP 2.

The code representing an implementation of the modified decision table is created and post optimizations are applied. The optimizations applied are of two main types: a. The first optimization applied is the combining of BEHAVIOR invocations. A code sequence of the type BEHAVIOR P1a
BEHAVIOR P1b is converted to the single invocation
BEHAVIOR P1.
b. Code expansions involving IF situations are likewise handled.

Thus the sequence

IF C1 THEN

BEHAVIOR P1

ELSE

BEHAVIOR P2 becomes simply BEHAVIOR P1 because only one of...