Penelope Reference Manual, Version 3-3 (COO 1), includes Larch/Ada Specification Manual for Sequential Ada (C002).

Abstract

Penelope is an interactive environment that helps its user to develop and verify programs written in a rich subset of sequential Ada. Penelope is well-suited to developing programs in the goal-directed style advocated by Gries and Diijkstra. In this style the programmer develops a program from a specification in a way that ensures the program will meet the specification. Of course, Penelope can also be used to verify previously written programs. With Penelope, it is often possible to modify a verified program and verify the modified version with minimal effort by replaying and modifying the original program's proof.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 02, 1994
Accession Number
ADA289828

Entities

People

  • Carla Marceau

Organizations

  • Unisys

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Computations
  • Computer Programming
  • Computer Programs
  • Computers
  • Contractors
  • Contracts
  • Guarantees
  • High Level Languages
  • Language
  • Mathematics
  • Real Numbers
  • Side Effects
  • Specifications
  • Standards
  • User Interface

Fields of Study

  • Computer science
  • Engineering

Readers

  • Game Theory.
  • Software Engineering.