Accession Number : ADA289616

Title :   Report on Logical Foundations.

Descriptive Note : Informal technical rept.

Corporate Author : ODYSSEY RESEARCH ASSOCIATES INC ITHACA NY

PDF Url : ADA289616

Report Date : 26 FEB 1994

Pagination or Media Count : 84

Abstract : The Penelope Ada proof editor allows a user to incrementally develop provably correct Ada programs. The current version of the Penelope system is formally based on a predicate transformer semantics for sequential Ada. The purpose of this work is to provide the mathematical foundations for extending Penelope to Ada tasking programs.

Descriptors :   *COMPUTER PROGRAM VERIFICATION, *ADA PROGRAMMING LANGUAGE, SPECIFICATIONS, SEMANTICS, SEQUENCES, MATHEMATICS, EDITING, TRANSFORMERS.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE