Cover for CAFE: An Industrial-Strength Algebraic Formal Method

CAFE: An Industrial-Strength Algebraic Formal Method

Book2000

Edited by:

K. Futatsugi, A.T. Nakagawa and T. Tamai

CAFE: An Industrial-Strength Algebraic Formal Method

Book2000

 

Cover for CAFE: An Industrial-Strength Algebraic Formal Method

Edited by:

K. Futatsugi, A.T. Nakagawa and T. Tamai

About the book

Browse this book

Book description

This book contains selected papers on the language, applications, and environments of CafeOBJ, which is a state-of -the-art algebraic specification language. The authors are speake ... read full description

Browse content

Table of contents

Actions for selected chapters

Select all / Deselect all

  1. Full text access
  2. Book chapterAbstract only

    Chapter 1 - Building Equational Proving Tools by Reflection in Rewriting Logic

    M. Clavel, F. Durán, ... J. Meseguer

    Pages 1-31

  3. Book chapterAbstract only

    Chapter 2 - CafeOBJ Jewels

    Rzvan Diaconescu, Kokichi Futatsugi and Shusaku Iida

    Pages 33-60

  4. Book chapterAbstract only

    Chapter 3 - An Overview of the Tatami Project

    Joseph Goguen, Kai Lin, ... Bogdan Warinschi

    Pages 61-78

  5. Book chapterAbstract only

    Chapter 4 - Proof Assistance for Equational Specifications Based on Proof Obligations

    Masaki Ishiguro and Ataru T. Nakagawa

    Pages 79-96

  6. Book chapterAbstract only

    Chapter 5 - Generating Rewrite Theories from UML Collaborations

    Alexander Knapp

    Pages 97-120

  7. Book chapterAbstract only

    Chapter 6 - Casl for CafeOBJ Users

    Peter D. Mosses

    Pages 121-144

  8. Book chapterAbstract only

    Chapter 7 - CafePie: A Visual Programming System for CafeOBJ

    Tohru Ogawa and Jiro Tanaka

    Pages 145-160

  9. Book chapterAbstract only

    Chapter 8 - On Extracting Algebraic Specifications from Untyped Object-Oriented Programs

    Hirotaka Ohkubo, Toshiki Sakabe and Yasuyoshi Inagaki

    Pages 161-178

  10. Book chapterAbstract only

    Chapter 9 - An Environment for Systematic Development of Algebraic Specifications on Networks

    Akishi Seo and Ataru T. Nakagawa

    Pages 179-193

About the book

Description

This book contains selected papers on the language, applications, and environments of CafeOBJ, which is a state-of -the-art algebraic specification language. The authors are speakers at a workshop held in 1998 to commemorate a large industrial/academic project dedicated to CafeOBJ. The project involved more than 40 people from more than 10 organisations, of which 6 are industrial. The workshop attracted about 30 talks and more than 70 attendees.

The papers in the book however, are either heavily revised versions presented at the workshop, to reflect recent advancements or research; or completely new ones, written especially for this book. In this regard, the book is not a usual postpublication after a workshop. Also, although it is a compendium of papers that are related to CafeOBJ, the book is not a manual, reference, or tutorial of CafeOBJ. Probably the best description is that it is a collection of papers that investigate how to use, or to make it easy to use, CafeOBJ. Reflecting the diverse nature of the project and its participants (most of the authors are participants to the project), the papers, put together, offer a comprehensive picture from this methodological perspective.

Some papers deal with various advanced aspects of the language, such as rewriting logic and behavioural logic. For rewriting logic, a couple of significant applications were reported. In particular, UML, now considered de facto standard language for modelling systems, is the subject of one paper. For behavioural logic, new methodological guidelines are presented. Some papers shed new light on a more traditional paradigm in the language; order-sorted equational specifications. One paper, in particular, deal with a way to associate CafeOBJ with object-oriented programming. The other papers deal with environments for writing and vertifying specifications written in CafeOBJ. Underlying those papers are two major considerations: user interfaces for manipulating specifications, and systematic supports for proofs. All the environments explained in the papers assume and support distributed computing, and de facto standard network technologies, such as WWW and http, are incorporated.

This book contains selected papers on the language, applications, and environments of CafeOBJ, which is a state-of -the-art algebraic specification language. The authors are speakers at a workshop held in 1998 to commemorate a large industrial/academic project dedicated to CafeOBJ. The project involved more than 40 people from more than 10 organisations, of which 6 are industrial. The workshop attracted about 30 talks and more than 70 attendees.

The papers in the book however, are either heavily revised versions presented at the workshop, to reflect recent advancements or research; or completely new ones, written especially for this book. In this regard, the book is not a usual postpublication after a workshop. Also, although it is a compendium of papers that are related to CafeOBJ, the book is not a manual, reference, or tutorial of CafeOBJ. Probably the best description is that it is a collection of papers that investigate how to use, or to make it easy to use, CafeOBJ. Reflecting the diverse nature of the project and its participants (most of the authors are participants to the project), the papers, put together, offer a comprehensive picture from this methodological perspective.

Some papers deal with various advanced aspects of the language, such as rewriting logic and behavioural logic. For rewriting logic, a couple of significant applications were reported. In particular, UML, now considered de facto standard language for modelling systems, is the subject of one paper. For behavioural logic, new methodological guidelines are presented. Some papers shed new light on a more traditional paradigm in the language; order-sorted equational specifications. One paper, in particular, deal with a way to associate CafeOBJ with object-oriented programming. The other papers deal with environments for writing and vertifying specifications written in CafeOBJ. Underlying those papers are two major considerations: user interfaces for manipulating specifications, and systematic supports for proofs. All the environments explained in the papers assume and support distributed computing, and de facto standard network technologies, such as WWW and http, are incorporated.

Details

ISBN

978-0-444-50556-9

Language

English

Published

2000

Copyright

Copyright © 2000 Elsevier B.V. All rights reserved

Imprint

Elsevier Science

Editors

K. Futatsugi

Japan Advanced Institute for Science and Technology, Tatsunokuchi, Japan

A.T. Nakagawa

Software Research Associates Inc., Tokyo, Japan

T. Tamai

University of Tokyo, Tokyo, Japan