Verification of APL Programs.
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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
- Computer Programming and Software