CAFE: An Industrial-Strength Algebraic Formal Method

1st Edition

Editors: K. Futatsugi A.T. Nakagawa T. Tamai
Hardcover ISBN: 9780444505569
eBook ISBN: 9780080528403
Imprint: Elsevier Science
Published Date: 6th October 2000
Page Count: 208
117.00 + applicable tax
71.00 + applicable tax
88.95 + applicable tax
113.00 + applicable tax
Unavailable
Compatible Not compatible
VitalSource PC, Mac, iPhone & iPad Amazon Kindle eReader
ePub & PDF Apple & PC desktop. Mobile devices (Apple & Android) Amazon Kindle eReader
Mobi Amazon Kindle eReader Anything else

Institutional Access


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 spe

Table of Contents

Building equational proving tools by reflection in rewriting logic (M. Clavel, F. Durán, S. eker, J. Meseguer). CafeOBL Jewels (R. Diaconescu, K. Futatsugi, S. Iida). An overview of the Tatami Project (J. Goguen, K. Lin, G. Roşu, A. Mori, B. Warinschi). Proof assistance for equational specifications based on proof obligations (M. Ishiguro, A. Nakagawa). Generating rewrite theories from UML collaborations (A. Knapp). CASL for CafeOBJ users (P. Mosses). CafePie: A visual programming system for CafeOBJ (T. Ogawa, J. Tanaka). On extracting algebraic specifications from untyped object-oriented programs (H. Ohkubo, T. Sakabe, Y. Inagaki). An environment for systematic development of algebrai specifications on networks (A. Seo, A. Nakagawa).

Details

No. of pages:
208
Language:
English
Copyright:
© Elsevier Science 2000
Published:
Imprint:
Elsevier Science
eBook ISBN:
9780080528403
Hardcover ISBN:
9780444505569

About the Editor

K. Futatsugi

Affiliations and Expertise

Japan Advanced Institute for Science and Technology (JAIST), 1-1 Asahidai, Ishikawa 923-12, Japan

A.T. Nakagawa

Affiliations and Expertise

Software Research Associates Inc. (SRA), Tokyo, Japan

T. Tamai

Affiliations and Expertise

University of Tokyo, Japan