Penelope: An Ada Verification Environment, Penelope User Guide: Penelope Tutorial
Geoffrey R. Hird · 1991
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.