Report on Logical Foundations.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 26, 1994
Accession Number
ADA289616

Tags

DTIC Thesaurus Topics

  • Air Force
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Contractors
  • Contracts
  • High Level Languages
  • Language
  • Notation
  • Programming Languages
  • Semantics
  • Software Development
  • Theoretical Computer Science
  • Transformers

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.
  • Software Verification and Validation.