Penelope: An Ada verification Environment, Larch/Ada Rationale. Volume 2

Abstract

This rationale provides a careful, but informal, account of the meanings of Larch/Ada specifications. It also describes the simplifying assumptions under which proofs in the Penelope verification environment imply that an Ada program satisfies its Larch/Ada specification. The account is intended to be adequate to the needs of a Penelope or Larch/Ada user, and to serve as an introduction for mathematically motivated readers who wish to consult other documents detailing the mathematics of Penelope.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1991
Accession Number
ADA249192

Entities

People

  • David Guaspari
  • Ian Sutherland

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Air Force
  • Air Force Facilities
  • Compilers
  • Computer Programming
  • Computer Programs
  • Computers
  • Contracts
  • Conversion
  • Environment
  • Language
  • Mathematics
  • Numbers
  • Programming Languages
  • Semantics
  • Side Effects
  • Specifications
  • Standards

Readers

  • Computational Linguistics
  • Computational Modeling and Simulation
  • Software Verification and Validation.