PVS (Prototype Verification System) ist ein Spezifikations- und Verifikationssystem mit integriertem interaktivem Theorembeweiser, entwickelt am SRI International; es basiert auf typisierter Higher-Order-Logik und wird besonders bei der NASA (Langley) für Hardware- und Protokoll-Verifikation eingesetzt. Eine Spezifikation besteht aus Theorien in .pvs-Dateien.
Arbeiten mit Theorien
pvs # Emacs-Oberflaeche starten
M-x typecheck # Theorie typisieren (C-c C-t)
M-x prove # Formel im Beweiser bearbeiten (C-c C-p)
M-x typecheck-prove # Typecheck + Beweis in einem Schritt (tcp)Eine Theorie definiert Typen, Konstanten und Axiome; Lemmata und Theoreme werden mit THEOREM bzw. LEMMA deklariert und mit Taktiken bewiesen.
Beweisführung im Prover
prove-it: Komplettbeweis aller offenen Beweisziele („autopilot“).grind: Standard-Mischung aus Vereinfachen, Suchen und Auto-Beweis — der wichtigste Allround-Befehl.simplify: Formel propositional vereinfachen.(skolem!)/flatten: Quantoren instanziieren bzw. Konjunktionen/Implikationen auflösen.(assert): Entscheidbare Teile (Arithmetik, Gleichheit) automatisch schließen.quit: Beweissitzung verlassen; Beweise landen als.prf-Dateien neben der Theorie.
PVS ist eng verwandt mit anderen Formale-Verifikations-Werkzeugen wie Coq, Lean und Isabelle; mit VDM teilt es die Idee der formalen Spezifikation vor der Implementierung.