TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving

摘要: We present a new approach to the implementation of graphical user interfaces (GUIs) for formal program development systems like transformation or interactive theorem provers. Its distinguishing feature is generic, open system design which allows family tools different methods on sound logical basis with uniform appearance. The context this work UniForM project [KPO+95], aim develop framework integrating in logically consistent way. Consistency achieved by encoding such as CSP and Z prover Isabelle [Pau94], used perform well prove correctness rules. One main objectives enable non-expert users actually at least part developmen~ themselves. Hence there crucial need an encapsulation technique these encodings providing generic way building interfaces.