Reliable Software Through Very High-Level Verification.
Abstract
A semantics of a significant fragment of APL has been constructed and is summarized. This semantics has been used to construct an implementation of the fragment of APL and part of the implementation has been verified. This research program was moved from the Univ. of Arizona to Virginia Polytechnic Inst. and State Univ. As a result of this move, the computing services used for this software have been changed from a DECsystem-10 to an IBM system 370/158. Although there were some difficulties, the software is substantially machine independent. The current state of the soft-ware and some of the problems encountered in the move are described. The starting point for the construction of an APL verifier is an incremental assertion synthesizer that was written at the Univ. of Arizona. The next step in the research is to complete the verification of the first part of the APL implementation. When this is completed, the work will branch into two cooperating projects. One of these projects is to complete the semantics and implementation of APL. The other is to derive the rules of inference for the APL primitives that have been defined and to work with the verifier to extend it to a more powerful verifier. After the semantics of APL are completed, the verifier will be further extended.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 10, 1978
- Accession Number
- ADA065193
Entities
People
- Richard J. Orgass
Organizations
- University of Arizona