Abstract
It is now considered important that formal methods should express properties of concurrence and time in the abstract languages to which developers are used. This article shows how modal action logic was incorporated in an object-oriented dialect of Z, respecting, as much as possible, the original syntax. We explain the specific modal action logic used and MaMooZ, the resulting language, is described.
Research funded by a CNPq postgraduate scholarship
Research funded by CNPq research grant number 300.133/85 CC
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.
References
H. Barringer. The use of temporal logic in the compositional specification of concurrent systems. In A. Galton, editor, Temporal Logics And Their Applications. Academic Press, 1987.
M. Danelutto and A. Masini. A temporal logic approach to specify and prove properties of finite state concurrent systems. In E. Borger, H.K. Blining, and M.M. Richter, editors, Proc. CSL’88 2nd Workshop on Computer Science Logic, Lecture Notes in Computer Science, 1988.
R. Duke, P. King, G. Rose, and G. Smith. The Object-Z Specification Language. Technical Report 91-1, SVRC—Software Verification Centre, The University of Queensland, May 1991.
J. Fiadeiro and T. Maibaum. Describing, structuring and implementing objects. In School/Workshop on Foundations of Object-Oriented Languages, REX/FOOL,Netherlands, 1990.
J. Fiadeiro and T. Maibaum. Towards Object Calculi. In IS-CORE Workshop,London, 1990.
J. Fiadeiro and A. Sernadas. Logics of Modal Terms for Systems Specification. Journal of Logic and Computation, l(2):187–227, 1990.
I. N. Kaufman. On the Application of Formal Specifications to the Logical Design of Software. Master’s thesis, Universidade Federal de Pernambuco, Recife-PE, Brazil, August 1992. In Portuguese.
S. R. L. Meira and A. L. C. Cavalcanti. Modular Object-Oriented Z Specifications. In Z Users & Technical Meeting, Workshops in Computing,Oxford-UK, December 1990. Springer-Verlag.
S. R. L. Meira and A. L. C. Cavalcanti. The MooZ Specification Language. Technical report, Universidade Federal de Pernambuco, Departamento de Informàtica, Recife-PE, 1992.
A. Pnueli. The temporal logic of programs. In Proc. 18th Ann. Symp. on Foundations of Computer Science, pages 46–57, 1977.
G. Saake and U.W. Lipeck. Using finite-linear temporal logic for specifying database dynamics. In E. Börger, H.K. Büning, and M.M. Richter, editors, Proc. CSL’88 2nd Workshop on Computer Science Logic,Lecture Notes in Computer Science, 1988.
J. M. Spivey. Understanding Z: A Specification Language and Its Formal Semantics. C. A. R. Hoare, Series Editor. Prentice Hall, 1988.
S. Stepney, R. Barden, and D. Cooper, editors. Object Orientation in Z.Workshops in Computing. Springer-Verlag, 1992.
D.A. Watt. Programming Language Syntax and Semantics. Prentice-Hall, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 British Computer Society
About this paper
Cite this paper
Kaufman, I.N., Meira, S.L. (1994). Modal Action Logic in a Practical Specification Language. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds) Algebraic Methodology and Software Technology (AMAST’93). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3227-1_32
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3227-1_32
Publisher Name: Springer, London
Print ISBN: 978-3-540-19852-9
Online ISBN: 978-1-4471-3227-1
eBook Packages: Springer Book Archive