More About TAS and IsaWin - Tools for Formal Program Development
作者： Christoph Lüth , Burkhart Wolff
关键词:
摘要: We present a family of tools for program development and verification, comprising the transformation system TAS theorem proving interface IsaWin. Both are based on prover Isabelle [8], which is used as generic logical framework here. A graphical user interface, principle direct manipulation, allows to interact with tool without having concern himself details representation within prover, leaving him concentrate main design decisions or proving.
springer.com
sci-hub.st 参考文章(9)
Bernd Krieg-Brückner, Jan Peleska, Ernst-Rüdiger Olderog, Alexander Baer, The UniForM Workbench, a Universal Development Environment for Formal Methods formal methods. pp. 1186- 1205 ,(1999) , 10.1007/3-540-48118-4_13
Kolyang, C. Lüth, T. Meyer, B. Wolff, TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving colloquium on trees in algebra and programming. pp. 855- 858 ,(1997) , 10.1007/BFB0030646
P. Garbett, J. P. Parkes, M. Shackleton, S. Anderson, Secure Synthesis of Code: A Process Improvement Experiment formal methods. pp. 1816- 1835 ,(1999) , 10.1007/3-540-48118-4_46
Christoph Lüth, Haykal Tej, Kolyang, Bernd Krieg-Brückner, TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving fundamental approaches to software engineering. pp. 239- 243 ,(1999) , 10.1007/978-3-540-49020-3_17
Tobias Nipkow, Lawrence C. Paulson, Isabelle: A Generic Theorem Prover ,(1994)
Till Mossakowski, CASL: From Semantics to Tools tools and algorithms for construction and analysis of systems. pp. 93- 108 ,(2000) , 10.1007/3-540-46419-0_8
C. LÜTH, B. WOLFF, Functional design and implementation of graphical user interfaces for theorem provers Journal of Functional Programming. ,vol. 9, pp. 167- 189 ,(1999) , 10.1017/S0956796899003421
Donald Sannella, What does the future hold for theoretical computer science colloquium on trees in algebra and programming. pp. 15- 19 ,(1997) , 10.1007/BFB0030585
Ralph-Johan Back, Joakim Wright, Refinement Calculus Springer New York. ,(1998) , 10.1007/978-1-4612-1674-2