Abstract
This paper discusses our proposal on how to embed theorems in Z specifications. One reason behind this proposal is to ease Z users in writing theorems directly in their Z specifications. Another reason is not to overwhelm Z users in learning other language, which in this case is SAL language. In doing so, we need to inform Z2SAL programmers how to translate these embedded theorems into equivalence theorems in SAL specifications. Based on our experiments, Z2SAL is able to translate these kind of theorems and SAL model checker is also able to model check SAL specifications with theorems that are written directly in the Z specifications.References
J. Jacky, The Way of Z: Practical Programming for Formal Methods. Cambridge University Press, 1997.
J. Derrick, S. North, and T. Simons, “Issues in Implementing a Model Checker for Z,” in Formal Methods and Software Engineering, 2006, pp. 678–696.
L. de Moura, S. Owre, and N. Shankar, “The SAL Language Manual,” 2019.
M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004.
R. Pelanek, “Reduction and Abstraction Techniques for Model Checking,” Masaryk University, 2006.
M. U. Siregar, “Support for Model Checking Z Specifications,” The University of Sheffield, 2016.
R. Duke and G. Smith, “Temporal Logic and Z Specification,” Aust. Comput. J., vol. 21, no. 2, pp. 62–66, 1989.
P. King, “Printing Z and Object_Z Latex Documents,” Dep. Comput. Sci. Univ. Queensl., vol. 393, pp. 404–410, 1990.
R. Duke, P. King, G. Rose, and G. Smith, “The Object-Z Specification Language: Version 1,” 1991.
J. M. Spivey, The Z Notation. Prentice Hall New York, 1989.
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
Copyright (c) 2019 IJID (International Journal on Informatics for Development)