Add-on Tools

I3P

I3P stands for »Interactive Interface for the Isabelle Prover«. Its aim is to enhance the user experience by employing standard widgets and well-known UI metaphors. On the architectural side, it is built to be extensible and emphasizes the use of design patterns.

AWE extensions pack

This provides facilities to establish morphisms between theories, allowing the interpretation of logical entities from one theory to another.

HOL-TestGen

HOL-TestGen HOL-TestGen is an environment for model-based Test-Generation. Models for unit-, sequence and reactive-sequence test scenarios can be written in HOL and tests are generated automatically.

HOL-OCL

HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into HOL. It provides mechanisms to read UML Class Diagrams (edited with ArgoUML), to annotate them with OCL, and to produce proofs compliant to the semantics UML/OCL 2.0. For Isabelle2005 only.

HOL-Z

HOL-Z is a proof environment for Z. It allows for importing Z specifications written in LaTeX and type-checked by the Java-based ZeTa-System. HOL-Z then allows for the formal analysis of such specifications, in particular data refinement proofs. For Isabelle200 only.

HOL-Boogie

HOL-Boogie is an interactive back-end for the Boogie program verifier and, in particular, may be used to proof verification conditions arising from C programs.

Haskabelle

Haskabelle is a converter from Haskell source files to Isabelle/HOL theories implemented in Haskell itself. This is part of the Isabelle distribution.