Accession Number:

ADA289616

Title:

Report on Logical Foundations.

Descriptive Note:

Informal technical rept.

Corporate Author:

ODYSSEY RESEARCH ASSOCIATES INC ITHACA NY

Personal Author(s):

Report Date:

1994-02-26

Pagination or Media Count:

84.0

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