Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Karlsen, E.W.: Tool Integration in a Functional Setting. PhD thesis, Universität Bremen (1998)
Kolyang, T.S., Wolff, B.: A structure preserving encoding of Z in Isabelle/HOL. In: von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 283–298. Springer, Heidelberg (1996)
Krieg-Brückner, B.: UniForM perspectives for formal methods. In: International Workshop on Current Trends in Formal Methods, in LNCS. Springer, Heidelberg (1998) to appear
Lüth, C., Karlsen, E.W., Kolyang, S.W., Wolff, B.: HOL-Z in the UniForM-workbench - a case study in tool integration for Z. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 116–134. Springer, Heidelberg (1998)
Lüth, C., Karlsen, E.W., Kolyang, S. Westmeier, Wolff, B.: Tool integration in the UniForM workbench. In: Workshop on Tool Support for System Specification, Development, and Verification, Advances of Computing Science. Springer, Heidelberg (to appear)
Lüth, C., Westmeier, S., Wolff, B: sml_tk: Functional programming for graphical user interfaces. Technical Report 7/96, Universität Bremen (1996), See also the sml_tk home page at http://www.informatik.uni-bremen.de/~cxl/sml_tk/
Lüth, C., Wolf, B.: Functional design and implementation of graphical user interfaces for theorem provers. To appear in Journal of Functional Programming
Mossakowski, T., Kolyang, Krieg-Brückner, B.: Static semantic analysis and theorem proving for CASL. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 349–364. Springer, Heidelberg (1997)
Paulson, L.C.: In: Paulson, L.C. (ed.) Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Tej, H., Wolff, B.: A corrected failure-divergence model for CSP in Isabelle/HOL. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 318–337. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lüth, C., Tej, H., Kolyang, Krieg-Brückner, B. (1999). TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving. In: Finance, JP. (eds) Fundamental Approaches to Software Engineering. FASE 1999. Lecture Notes in Computer Science, vol 1577. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49020-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-49020-3_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65718-7
Online ISBN: 978-3-540-49020-3
eBook Packages: Springer Book Archive