摘要: Formal methods are still expected to improve the practice of software engineering. The areas in which formal will play important roles include at least: (1) distributed component software, (2) network/system security, (3) embedded systems. better supported by specification languages equipped with verification capability.CafeOBJ is a language methodologies based on algebraic technique. CafeOBJ an executable wide spectrum multiple logical foundations; mainly initial and hidden algebras. Static aspects systems specified terms algebras, dynamic algebras.CafeOBJ first incorporates observational (or behavioral) specifications algebras serious way. Observational can be seen as nice combination static specifications, facilitate natural transparent complex systems.This paper gives overview system language. Some parts this updated modified versions already published book or papers such [10, 18, 3, 7].
springer.com
sci-hub.st 参考文章(28)
Joseph A. Goguen, José Meseguer, Unifying functional, object-oriented and relational programming with logical semantics Research directions in object-oriented programming. pp. 417- 478 ,(1987)
Joseph A. Goguen, José Meseguer, EQLOG: Equality, Types, and Generic Modules For Logic Programming. Logic Programming: Functions, Relations, and Equations. pp. 295- 363 ,(1986)
Koji Okada, Kokichi Futatsugi, Specification Writing as Construction of Hierarchically Structured Clusters of Operators. ifip congress. pp. 287- 292 ,(1980)
Răzvan Diaconescu, Extra Theory Morphisms for Institutions: Logical Semantics for Multi-Paradigm Languages Applied Categorical Structures. ,vol. 6, pp. 427- 453 ,(1998) , 10.1023/A:1008607717635
K. Futatsugi, T. Tamai, A. T. Nakagawa, CAFE: An Industrial-Strength Algebraic Formal Method Elsevier. ,(2000)
K. Futatsugi, An overview of OBJ2 Proceedings of the first Franco-Japanese Symposium on Programming of future generation computers. pp. 139- 159 ,(1988)
R.ăzvan Diaconescu, Kokichi Futatsugi, Shusaku Iida, Component-Based Algebraic Specification and Verification in CafeOBJ formal methods. pp. 1644- 1663 ,(1999) , 10.1007/3-540-48118-4_37
Yellamraju V. Srinivas, Richard Jüllig, Specware: Formal Support for Composing Software mathematics of program construction. pp. 399- 422 ,(1995) , 10.1007/3-540-60117-1_22
Kokichi Futatsugi, Razvan Diaconescu, Behavioural Coherence in Object-Oriented Algebraic Specification Journal of Universal Computer Science. ,vol. 6, pp. 74- 96 ,(2000)
José Meseguer, Membership algebra as a logical framework for equational specification workshop on recent trends in algebraic development techniques. pp. 18- 61 ,(1997) , 10.1007/3-540-64299-4_26