| Generic Transformation Systems for Formal Methods (2007) | |||||||||||||||
Abstract | |||||||||||||||
| Introduction We will present two tools, TAS and IsaWin, for transformational program development and theorem proving respectively, based on the theorem prover Isabelle. Their distinguishing feature is a generic, open system design which allows the development of a family of tools for different formal methods on a sound logical basis with a uniform appearance. The context of this work is the UniForM project, the aim of which is to develop a framework integrating different formal methods in a logically consistent way. Consistency is achieved by encoding formal methods in the theorem prover Isabelle, which is used to perform the program development as well as to prove the correctness of the transformation rules. The Transformation Application System TAS TAS is a system for transformational program development in Isabelle. It is designed to keep everything about proofs in Isabelle away from the user. The proof obligations resulting from applying | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||