Abstract
Although formal methods have the potential to greatly enhance software development, they have not been widely used in industry (particularly in the United States). We have developed a system for executing specifications by compiling them to Oz programs. Executability is a great aid in developing specifications, and also increases the usefulness of specifications by allowing them to serve as prototypes and test oracles. In this work, we describe how we have used the Oz language both as a translation target and in implementing a library of procedures used by the generated programs. Oz is ideal for our purposes, as it has allowed us to easily use declarative, concurrent constraint and graphical user interface programming together within a single framework.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Graphical User Interface
- Domain Variable
- Inductive Logic Programming
- Choice Point
- Java Modeling Language
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
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1990)
Fitzgerald, J.S., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, Cambridge (1998) ISBN 0521623480
Spivey, J.M.: An introduction to Z and formal specifications. Software Engineering Journal 4, 40–50 (1989)
Davies, J., Woodcock, J.C.P.: Using Z: Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1996)
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996) ISBN 0 521 49619 5
B-Core(UK) Ltd: B-Core website (2004), http://www.B-core.com/
Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, Minneapolis, Minnesota, pp. 105–106. ACM, New York (2000)
Wahls, T., Leavens, G.T.: Formal semantics of an algorithm for translating model-based specifications to concurrent constraint programs. In: Proceedings of the 16th ACM Symposium on Applied Computing, Las Vega, Nevada, pp. 567–575 (2001)
Wahls, T., Leavens, G.T., Baker, A.L.: Executing formal specifications with concurrent constraint programming. The Automated Software Engineering Journal 7 (2000)
West, M.M., Eaglestone, B.M.: Software development: Two approaches to animation of Z specifications using Prolog. IEE/BCS Software Engineering Journal 7, 264–276 (1992)
Fuchs, N.: Specifications are (preferably) executable. Software Engineering Journal 7, 323–334 (1992)
Gray, J.G., Schach, S.R.: Constraint animation using an object-oriented declarative language. In: Proceedings of the 38th Annual ACM SE Conference, Clemson, SC, pp. 1–10 (2000)
O’Neill, G.: Automatic translation of VDM specifications into Standard ML programs. The Computer Journal 35, 623–624 (1992)
Elmstrøm, R., Larsen, P.G., Lassen, P.B.: The IFAD VDM-SL toolbox: A practical approach to formal specifications. ACM Sigplan Notices 29, 77–80 (1994)
Fröhlich, B.: Program Generation Based on Implicit Definitions in a VDM-like Language. PhD thesis, Technical University of Graz (1998)
Jackson, D., Damon, C.: Semi-executable specifications. Technical Report CMU-CS-95-216, School of Computer Science, Carnegie Mellon University (1995)
Breuer, P.T., Bowen, J.P.: Towards correct executable semantics for Z. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop, Cambridge 1994. Workshops in Computing. Springer, Heidelberg (1994)
Grieskamp, W.: A computation model for Z based on concurrent constraint resolution. In: P. Bowen, J., Dunne, S., Galloway, A., King, S. (eds.) ZB 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 414–432. Springer, Heidelberg (2000)
Mehl, M., Müller, T., Popov, K., Scheidhauer, R., Schulte, C.: DFKI Oz User’s Manual. Programming Systems Lab, German Research Center for Artificial Intelligence (DFKI) and Universität des Saarlandes, Postfach 15 11 50, D-66041 Saarbrücken, Germany (1998)
Mozart Consortium: Mozart Programming System website (2004), http://www.mozart-oz.org
Van Roy, P., Haridi, S.: Concepts, Techniques and Models of Computer Programming. The MIT Press, Cambridge (2004)
Wu, D., Cheng, Y., Wahls, T.: A graphical user interface for executing formal specifications. The Journal of Computing in Small Colleges 17, 79–86 (2002)
Marriott, K., Stuckey, P.J.: Programming with Constraints: An Introduction. The MIT Press, Cambridge (1998)
Struyf, J., Blockeel, H.: Query optimization in inductive logic programming by reordering literals. In: Horváth, T., Yamamoto, A. (eds.) ILP 2003. LNCS (LNAI), vol. 2835, pp. 329–346. Springer, Heidelberg (2003)
Overton, D., Somogyi, Z., Stuckey, P.J.: Constraint-based mode analysis of Mercury. In: Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, Pittsburgh, PA, USA, pp. 109–120. ACM Press, New York (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wahls, T. (2005). Compiling Formal Specifications to Oz Programs. In: Van Roy, P. (eds) Multiparadigm Programming in Mozart/Oz. MOZ 2004. Lecture Notes in Computer Science, vol 3389. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31845-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-31845-3_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25079-1
Online ISBN: 978-3-540-31845-3
eBook Packages: Computer ScienceComputer Science (R0)