Abstract
We present the generic system framework of Isabelle/Isar underlying recent versions of Isabelle. Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising extensible state components and extensible syntax that can be bound to tactical ML programs. Thus the Isabelle/Isar architecture may be understood as an extension and refinement of the traditional "LCF approach©, with explicit infrastructure for building derivative systems. To demonstrate the technical potential of the framework, we apply it to a concrete formal methods tool: the HOL-Z 3.0 environment, which is geared towards the analysis of Z specifications and formal proof of forward-refinements. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Wenzel, M., & Wolff, B. (2007). Building formal method tools in the Isabelle/Isar framework. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4732 LNCS, pp. 352–367). Springer Verlag. https://doi.org/10.1007/978-3-540-74591-4_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
