Quelle README.thy

Sprache: Isabelle

theory README imports Main
begin

section ‹Hoare Logic for a Simple WHILE Language›

subsection ‹Language and logic›

text ‹
This directory contains an implementation of Hoare logic for a simple WHILE
language. The constructs are

▪ ▩‹SKIP›
▪ ▩‹_ := _›
▪ ▩‹_ ; _›
▪ ▩‹IF _ THEN _ ELSE _ FI›
▪ ▩‹WHILE _ INV {_} DO _ OD›

Note that each WHILE-loop must be annotated with an invariant.

Within the context of theory ▩‹Hoare›, you can state goals of the form
@{verbatim [display] ‹VARS x y ... {P} prog {Q}›}
where ▩‹prog› is a program in the above language, ▩‹P› is the precondition,
▩‹Q› the postcondition, and ▩‹x y ...› is the list of all ∗‹program
variables› in ▩‹prog›. The latter list must be nonempty and it must include
all variables that occur on the left-hand side of an assignment in ▩‹prog›.
Example:
@{verbatim [display] ‹VARS x {x = a} x := x+1 {x = a+1}›}
The (normal) variable ▩‹a› is merely used to record the initial value of
▩‹x› and is not a program variable. Pre/post conditions can be arbitrary HOL
formulae mentioning both program variables and normal variables.

The implementation hides reasoning in Hoare logic completely and provides a
method ▩‹vcg› for transforming a goal in Hoare logic into an equivalent list
of verification conditions in HOL: 🚫‹apply vcg›

If you want to simplify the resulting verification conditions at the same
time: 🚫‹apply vcg_simp› which, given the example goal above, solves it
completely. For further examples see 🚫‹Examples.thy›.

\‹IMPORTANT:›
This is a logic of partial correctness. You can only prove that your program
does the right thing ∗‹if› it terminates, but not ∗‹that› it terminates. A
logic of total correctness is also provided and described below.
›

subsection ‹Total correctness›

text ‹
To prove termination, each WHILE-loop must be annotated with a variant:

▪ ▩‹WHILE _ INV {_} VAR {_} DO _ OD›

A variant is an expression with type ▩‹nat›, which may use program variables
and normal variables.

A total-correctness goal has the form ▩‹VARS x y ... [P] prog [Q]› enclosing
the pre- and postcondition in square brackets.

Methods ▩‹vcg_tc› and ▩‹vcg_tc_simp› can be used to derive verification
conditions.

From a total-correctness proof, a function can be extracted which for every
input satisfying the precondition returns an output satisfying the
postcondition.
›

subsection ‹Notes on the implementation›

text ‹
The implementation loosely follows

Mike Gordon. ∗‹Mechanizing Programming Logics in Higher Order Logic›.
University of Cambridge, Computer Laboratory, TR 145, 1988.

published as

Mike Gordon. ∗‹Mechanizing Programming Logics in Higher Order Logic›. In
∗‹Current Trends in Hardware Verification and Automated Theorem Proving›,
edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.

The main differences: the state is modelled as a tuple as suggested in

J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka.
∗‹Mechanizing Some Advanced Refinement Concepts›. Formal Methods in System
Design, 3, 1993, 49-81.

and the embeding is deep, i.e. there is a concrete datatype of programs. The
latter is not really necessary.
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-30) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.