| Abstract: |
The aim of this work is twofold: on the one hand, it constitutes the first extended application
of the recently developed calculus of monadic dynamic logic and thus demonstrates how this calculus can be applied to serious verification tasks. To name two examples, the total
correctness of a breadth-first search algorithm and of a pattern matching algorithm involving
Java-like exception handling have been established.
On the other hand, driven by the insight that due to the complexity even of relatively
small software systems it is not feasible to carry out formal proofs about these manually, the
calculus had to be implemented in some proof assistant tool. Furthermore, the formalisation
within such a tool provides further evidence of the correctness of one’s inferences – provided
one trusts in the correctness of the tool, of course. We chose the generic proof assistant
(often termed ‘theorem prover’) Isabelle/HOL in which we could base our implementation
on a stable and well developed formalisation of higher-order logic. Isabelle/HOL comes
with tools for proving theorems outright (by means of a classical tableau reasoner) as well
as a term rewriting system that allows for equational reasoning and functional programming.
Tasks during this implementation included the definition of a syntax for monadic dynamic
logic, proving the theorems needed as foundations for the logic, and working out theorems
and setting up Isabelle’s automatic proof facilities to make life easier when applying the logic.
The embedding into higher-order logic is a deep one in the sense that we define monadic
logical connectives, as well as a predicate ` asserting the validity of monadic
formulae. HOL formulae may, however, appear in monadic formulae thanks to existence of
an insertion function Ret mapping HOL formulae into those of dynamic logic. |
