Abstract
The UniForM-Workbench is an open tool-integration environment providing type-safe communication, a toolkit for graphical user-interfaces, version management and configuration management.
We demonstrate how to integrate several tools for the Z specification language into the workbench, obtaining an instantiation of the workbench suited as a software development environment for Z. In the core of the setting, we use the encoding HOL-Z of Z into Isabelle as semantic foundation and for formal reasoning with Z specifications. In addition to this, external tools like editors and small utilities are integrated, showing the integration of both self-developed and externally developed tools.
The resulting prototype demonstrates the viability of our approach to combine public domain tools into a generic software development environment using a strongly typed functional language.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bahlke, R., Snelting, G.: The PSG system: From formal language definitions to interactive programming environments. ACM Transactions on Programming Languages and Systems (October 1986)
Bloesch, A., Kazmierczak, E., Kearney, P., Traynor, O.: Cogito: A methodology and system for formal development. International Journal of Software Engineering 4(3) (1995)
Bowen, J.P., Gordon, M.J.C.: Z and HOL. In: Bowen, J.P., Hall, J.A. (eds.) Workshops in Computing, Z Users Workshops, Cambridge, UK, pp. 141–167. Springer, Heidelberg (1994)
The H-PCTE Crew. H-PCTE vs. PCTE, version 2.8. Technical report, Universität Siegen (June 1996)
ECMA. Reference model for frameworks of software engineering environments. Technical Report TR/55, European Computer Manufacturers Association (June 1993)
ECMA. Portable Common Tool Environment (PCTE) – Abstract Specification. European Computer Manufacturers Association, 3 edition, Standard ECMA-149 (December 1994)
Open Software Foundation. OSF/Motif Series. Prentice Hall (1992)
Fröhlich, M., Werner, M.: daVinci V2.0.3 online documentation. Universität Bremen, German (1997), http://www.informatik.uni-bremen.de/~davinci/
Habermann, A.N., Notkin, D.: Gandalf: Software Development Environments. IEEE Transactions on Software Engineering (December 1985)
Hudak, P., Peyton Jones, S.L., Wadler, P.: Report on the programming language Haskell – a non strict purely functional language. version 1.2. ACM SIGPLAN notices 27(5), 1–162 (1992)
Jones, R.B.: ICL ProofPower. BCS FACS FACTS, Series III 1(1), 10–13 (1992)
Karlsen, E.W.: Integrating interactive tools using concurrent Haskell and synchronous events. In: CLaPF 1997: 2nd Latin-American Conference on Functional Programming (September 1997)
Karlsen, E.W.: The UniForM concurrency toolkit and its extensions to concurrent Haskell. In: GWFP 1997: Glasgow Workshop on Functional Programming (September 1997)
Karlsen, E.W.: The UniForM user interaction manager. Draft technical report, FB 3, Universität Bremen (1998)
Karlsen, E.W.: The UniForM WorkBench – a higher order tool integration framework. In: International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, October 7–9 (1998), http://www.dfki.de/vse/fm-trends/
Karlsen, E.W., Westmeier, S.: Using concurrent haskell to develop views over an active repository. In: Clack, C., Hammond, K., Davie, T. (eds.) IFL 1997. LNCS, vol. 1467, p. 285. Springer, Heidelberg (1998)
Kolyang, Lüth, C., Meier, T., Wolff, B.: TAS and IsaWin: Generic interfaces for transformational program development and theorem proving. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 855–859. Springer, Heidelberg (1997)
Kolyang, Santen, T., Wolff, B.: A structure preserving encoding of Z in Isabelle/ HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 283–298. Springer, Heidelberg (1996)
Kraan, I., Baumann, P.: Implementing Z in Isabelle. In: Bowen, J.P., Hinchey, M. (eds.) ZUM 1995. LNCS, vol. 967, pp. 355–373. Springer, Heidelberg (1995)
Krasner, G., Pope, S.: A cookbook for using the model-view-controller user interface paradigm in Smalltalk-80. Journal of Object Oriented Programming 1(3), 26–49 (1988)
Lacroix, M., Vanhoedenaghe, M. (eds.): Tool Integration in an Open Environment. LNCS, vol. 387. Springer, Heidelberg (1989)
Libes, D.: expect: Scripts for controlling interactive processes. Computing Systems 4(2) (Spring 1991)
Nagl, M. (ed.): IPSEN 1996. LNCS, vol. 1170. Springer, Heidelberg (1996)
Nicholls, J., The Z Standards Panel: Z notation (September 1995), http://www.comlab.ox.ac.uk/oucl/groups/zstandards/
Ousterhout, J.K.: Tcl and the Tk Toolkit. Addison-Wesley, Reading (1994)
Paulson, L.C. (ed.): Isabelle – A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Peyton Jones, S., Gordon, A., Finne, S.: Concurrent Haskell. In: Principles of Programming Languages 1996 (POPL 1996), Florida (1996)
Reif, W., Schellhorn, G., Stenzel, K.: Proving system correctness with KIV. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 859–862. Springer, Heidelberg (1997)
Reppy, J.H.: Higher-Order Concurrency. PhD thesis, Department of Computer Science, Cornell University, USA (1992)
Reps, T.: Generating Language Based Environments. PhD Thesis, Cornell University, USA. MIT Press (1983)
Schefström, D., van den Broek, G.: Tool Integration. John Wiley & Sons, Chichester (1993)
Westmeier, S.: Verwaltung versionierter persistenter objekte in der UniForM Work- Bench (UniForM OMS toolkit). Diplomarbeit, FB 3, Universität Bremen, Germany (January 1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lüth, C., Karlsen, E.W., Kolyang, (.)., Westmeier, S., Wolff, B. (1998). 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 ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive