Kokichi Futatsugi

Razvan Diaconescu

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. Contents:Basic Specifications:SignaturesModelsSentencesSatisfactionProof SystemStructuring Specifications:Fundamental Semantics ConceptsModule ImportsViewsParameterized ModulesModule ExpressionsBuilt-in ModulesProof Technologies:RewritingInductionCoinductionMethodologies:NondeterminismConcurrent Object CompositionDynamic Systems of ObjectsApplications in Rewriting LogicGeneral Small Methodological Advises Readership: Students, researchers, and practitioners in software engineering and/or theoretical computer science. Keywords:Algebraic Specification;Software Engineering;CafeOBJ;OBJ;Object Oriented;Behavioural Specification;Hidden Algebra;Rewriting Logic;Equational Programming;Equational Specification

The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification

Cafeobj Report

This book develops model theory independently of any concrete logical system or structure, within the abstract category-theoretic framework of the so called ‘institution theory’. The development includes most of the important methods and concepts of conventional concrete model theory at the abstract institution-independent level. Consequently it is easily applicable to a rather large diverse collection of logics from the mathematical and computer science practice.

Institution-independent Model Theory

This is a report on the formal definition of the CafeOBJ algebraic specification language, which is a modern successor to the famous algebraic language OBJ. While the equational core of CafeOBJ is just a reshaping of OBJ, CafeOBJ significantly extends OBJ by incorporating several recent major developments in the area of algebraic specification, such as behavioural specification and rewriting logic. The definition of the language parallels its logical semantics based on the so-called institutions, which also provide a methodological framework for structuring the presentation of the basic constructs of the language and their semantics. This report presents all the basic constructs of the language together with their semantics and addresses both the programming in-the-small and in-the-large levels. However, it also discusses proof systems and technologies, as well as methodologies. Examples are provided throughout the report as intuitive support for the definitions of the constructs and for illustrating proof techniques and methodologies.

Razvan Diaconescu

About

Books

Join the club