From formal specification to full proof : a stepwise method

Abstract

High integrity system specifications are very difficult to analyse and check for correctness, whether they are written formally, informally, or are on the way to being formalised. Such specifications are often written by many different stakeholders and therefore it is a laborious task bringing all the components together. This thesis introduces and new and stepwise toolkit to assist the translation of formal specifications into theorem provers based on the MathLang Framework. Each step comes with it’s own correctness checks, some of which can be done on informal as well as formal specifications. Steps can be performed in isolation or all together in a sequence in order to translate a formal specification into a formal proof in Isabelle - even by someone who is not necessarily proficient in theorem proving. The ZMath-Lang toolkit allows users to bring their specifications together and helps to manage all the components.