Abstract:


The Z Specification Language and the Proof Environment Isabelle/HOL-Z


David Basin and Hironobu Kuruma and Shin Nakajima and Burkhart Wolff



Z is a standardized and well-established formal specification language originally 
developed in the 80ies by researchers at oxford University. Although the original 
emphasis of Z is on specification, the semantics for Z can be expressed within 
higher-order logic (HOL). On this basis, a theorem-proving environment such as 
Isabelle/HOL-Z can be built. In this paper, we show how properties over 
specifications can be formally proven in HOL-Z. Particular emphasis is put on 
proving relationships between specification such as refinement.