Penelope: An Ada Verification Environment, Penelope User Guide: Penelope Tutorial

Abstract

This tutorial introduces program verification with Penelope and Penelope's proof editor. Penelope incrementally generates verification conditions for a program, and the proof of those verification conditions implies that the program meets its specifications. Penelope's proof editor supports proofs of the verification conditions in ordinary first-order logic. We present the proof rules for Penelope, and discuss specification and proof strategies by means of examples. 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
ADA249420

Entities

People

  • Geoffrey Hird

Tags

Communities of Interest

  • Space

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Air Force Facilities
  • Arithmetic
  • Calculus
  • Computer Science
  • Contracts
  • Corporations
  • Hypotheses
  • Language
  • Logic
  • Specifications
  • Standards
  • Strategic Defense Initiative
  • Template Patterns
  • Verification
  • Visibility

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Software Verification and Validation.