Integrating Isabelle/HOL with Specware

Abstract. Isabelle/HOL is integrated with Specware in order to discharge proof obligations arising during Specware’s specification and refinement process. Specware’s proof obligations arise from use of predicate subtypes, termination conditions, and correctness of refinements as well as any explicit theorems. Specware specifications are structured into units called specs which correspond to Isabelle/HOL theories. Refinement is specified using spec morphisms and spec substitutions, a particular kind of colimit. We provide a system based on translating a Specware specification and its refinement into Isabelle/HOL theories, such that if Isabelle accepts all the translated theories, then the refinement is correct. Isabelle scripts for proving obligation theorems are embedded in Specware spec files so that proofs can be reused. The paper describes this translation and the issues that arise.