CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-oriented Algebraic Specification
CafeOBJ is an industrial strength modern algebraic specification language, a successor of the famous OBJ language, and directly incorporating new paradigms such as behavioural concurrent specification and rewriting logic. CafeOBJ is the core of an environment supporting the systems (mainly software but not only) development process at several levels, including prototyping, specification, and formal verification.This book presents not only the formal definition of the language and its semantics, but also methodologies for specification and verification in CafeOBJ, with emphasis on concurrent object composition and modularity.The presentation of the CafeOBJ concepts is supported by many examples, and an appendix illustrates the power of the language and its methodologies by a larger CASE study including specification, testing, and verification.The book may be used both by software engineers interested in algebraic methodologies, and by students and researchers in software engineering and/or theoretical computing science as a fast introduction to state-of-art algebraic specification.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Dynamic Systems of Objects
a CASE study
Notations and Conventions
Other editions - View all
algebraic specification arity attribute BARE-NAT basic specifications behavioural equivalence behavioural specification behaviourally coherent Bool built-in modules CafeCBJ category theory co-limit coinduction commutativity composing objects concurrent congruence counter defined denotation denotational semantics diagram eq eq eq equational logic equational specification Example extra theory morphisms free monoids functor hidden sorts HSS-BNAT implementation importation mode initial algebra initial model input instantiation institution morphism language method bop module expressions module imports module-expr MON-POW monoids Nat eq NAT-OMEGA NAT-TIMES natural numbers NNat non-sharing object composition omega operational semantics paradigms parameter parameterized module predicate projection operation proof calculus proof score proof theory protecting protecting mode pushouts put-money reduction rewrite model rewrite specification rewriting logic sentences sharing sign(SP signature morphism SIMPLE-NAT sort Elt specification morphism STRG STRG-BNAT strings StrÝ switch take-money TelSys term tions TopLevel transitions TRIV user-id atm variables withdraw X-terms
Software Engineering with OBJ: Algebraic Specification in Action
Joseph A. Goguen,Grant Malcolm
No preview available - 2000
All Book Search results »
Foundations of Software Science and Computation Structures: 5th ...
Mogens Nielsen,Uffe Engberg
No preview available - 2002