## CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-oriented Algebraic SpecificationCafeOBJ 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.

### Contents

Sentences | 11 |

Proof System | 30 |

Structuring Specifications | 35 |

Views | 54 |

Module Expressions | 73 |

Induction | 86 |

Dynamic Systems of Objects | 105 |

CafeCBJ Syntax | 123 |

a CASE study | 143 |

Notations and Conventions | 163 |

### Other editions - View all

### Common terms and phrases

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

### References to this book

Software Engineering with OBJ: Algebraic Specification in Action Joseph A. Goguen,Grant Malcolm No preview available - 2000 |

Foundations of Software Science and Computation Structures: 5th ... Mogens Nielsen,Uffe Engberg No preview available - 2002 |