Penelope: An Ada Verification Environment, Penelope User Guide: Larch/ Ada Reference Manual. Volume 5A

Abstract

This reference manual describes the specification language for the Penelope verification environment. It provides a brief, informal account of the syntax and semantics of Penelope annotations. Ada, Larch, Larch/Ada, Formal Methods, Formal Specification, Program Verification, Predicate Transformers, Ada Verification

Open PDF

Document Details

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

Entities

People

  • Carla Marceau

Tags

Communities of Interest

  • Air Platforms

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Air Force Facilities
  • Computations
  • Contracts
  • Corporations
  • Environment
  • Guarantees
  • Language
  • Mathematics
  • Semantics
  • Short Circuits
  • Side Effects
  • Specifications
  • Strategic Defense Initiative
  • Verification
  • Words (Language)

Fields of Study

  • Engineering

Readers

  • Computational Linguistics
  • Software Verification and Validation.