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

摘要

This rationale provides a careful, but informal, account of the meanings ofLarch/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.