CAFE : an industrial-strength algebraic formal method / edited by K. Futatsugi, A.T. Nakagawa, T. Tamai.

Format:

Book

Contributor:

Futatsugi, Kokichi.

Nakagawa, A. T. (Ataru T.)

Tamai, T. (Tetsuo)

Language:

English

Subjects (All):

Formal methods (Computer science)--Congresses.

Formal methods (Computer science).

Algebraic logic--Congresses.

Algebraic logic.

Physical Description:

1 online resource (209 p.)

Place of Publication:

Oxford : Elsevier, 2000.

Language Note:

English

Summary:

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 co

Contents:

Front Cover; CAFE: An Industrial-Strength Algebraic Formal Method; Copyright Page; Preface; Contents; Chapter 1. Building Equational Proving Tools by Reflection in Rewriting Logic; 1. Introduction; 2. Basic Concepts and Tool Design; 3. The Inductive Theorem Prover; 4. The Church-Rosser Checker; 5. Concluding Remarks; Chapter 2. CafeOBJ Jewels; 1. Introduction; 2. Sorting Strings; 3. Nondeterminism; 4. Behavioural Sets and Lists; 5. Composing Objects Concurrently; Chapter 3. An Overview of the Tatami Project; 1. Introduction; 2. Tatami System Design; 3. User Interface Design

4. Conclusions and Future ResearchA. Sample DUCK Code; B. Sample XSL Code; C. A Formal Description of 2-Doags; Chapter 4. Proof Assistance for Equational Specifications Based on Proof Obligations; 1. Introduction; 2. Overview; 3. Extracting Proof Obligations; 4. Using Proof Obligations for Arbitrary Equations; 5. Proof Construction for Parameterised Modules; 6. Conclusions and Future Works; Chapter 5. Generating Rewrite Theories from UML Collaborations; 1. UML Collaborations; 2. Semantic Domains for Instances; 3. Generating Rewrite Theories from Collaborations

4. Correctness of the TranslationA. UML Meta-Model; B. Sample UML Model; Chapter 6. CASL for CafeOBJ Users; 1. Introduction; 2. The Common Features: CafeOBJΩ CASL; 3. The Differences: CafeOBJ \ CASL; 4. The Differences: CASL \ CafeOBJ; 5. Conclusion; A. Appendix: CASL Overview and Examples; Chapter 7. CafePie: A Visual Programming System for CafeOBJ; 1. Introduction; 2. Features of Visual Programming; 3. The ""CafePie"" System; 4. Related Works; 5. Summary and Further Research; Chapter 8. On Extracting Algebraic Specifications from Untyped Object-Oriented Programs; 1. Introduction

2. Overview of Hennicker & Schmitz's Transformation and Type Inference of TinyObject3. Transformation of Polymorphic TinyObject Programs to Order-sorted Algebraic Specifications; 4. Relationship between Algebraic and Operational Semantics of TinyObject; 5. Concluding Remarks; A. Definitions; Chapter 9. An Environment for Systematic Development of Algebraic Specifications on Networks; 1. Introduction; 2. Specification Development Environment We Want; 3. On the Framework; 4. On the Implementation; 5. Conclusions

Notes:

Selected papers from a symposium held in Numazu, April 1998.

Includes bibliographical references.

ISBN:

1-281-05967-6

9786611059675

0-08-052840-6

OCLC:

476113159