Accession Number:

AD0754856

Title:

Verification of APL Programs.

Descriptive Note:

Doctoral thesis,

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Gerhart,Susan Lucille

Report Date:

1972-11-01

Pagination or Media Count:

224.0

Abstract:

APL is of interest with regard to program verification for two reasons many loops may be expressed in the structured operators, resulting in fewer assertions and thus easier verification for some programs, especially those with arrays, and the partial operators introduce the complication of showing that a program is executable. A formal definition of the APL operators serves as the base for a deductive system in which it is possible to informally prove assertions about APL programs. A mechanical system is described which generates preconditions for proper program executability. Several programs are verified. Author

Descriptors:

• (*COMPUTER PROGRAMS
• TEST METHODS)
• PROGRAMMING LANGUAGES
• OPERATORS(MATHEMATICS)
• VECTOR ANALYSIS
• ALGORITHMS
• THESES

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE