Abstract:

More about TAS and IsaWin: Tools for Formal Program Development

Christoph Lüth and Burkhart Wolff


We present a family of tools for program development and verification, compris- ing the transformation system 
TAS and the theorem proving interface IsaWin. Both are based on the theorem prover Isabelle, which is used as 
a generic logical framework here. A graphical user interface, based on the principle of di- rect manipulation, 
allows the user to interact with the tool without having to concern himself with the details of the representation 
within the theorem prover, leaving him to concentrate on the main design decisions of program development or 
theorem proving. The tools form an integrated system for formal program development, in which TAS is used 
for transformational program development, and IsaWin for discharging the incurred proof obligations. However, 
both tools can be used sep- arately as well. Further, the tools are generic over the formal method employed. In 
this extended abstract, we will first give a brief overview over TAS and IsaWin. Since TAS and IsaWin have 
been presented on previous ETAPS conferences, the presentation will highlight the new features as sketched 
out below.