Penelope: An Ada verification Environment, Larch/Ada Rationale. Volume 2
David Guaspari, Ian A. Sutherland · 1991
ABSTRACTPMkmum I'll)ihis 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.