We will present two tools, TAS and IsaWin, for transformational program development and theorem proving respectively, based on the theorem prover Isabelle [9]. Their distinguishing features are a graphical user interface based on the principle of direct manipulation, and 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.
展开▼
