Ebook: Algebraic Foundations of Systems Specification

The aim of software engineering is the provision and investigation of methods for the development of software systems of high quality with correctness as a key issue. A system is called correct if it does what one wants, if it meets the requirements. To achieve and to guarantee correct systems, the need of formal methods with rigorous semantics and the possibility of verification is widely accepted. Algebraic specification is a software engineering approach of this perspective. When Liskov and Zilles, Guttag and the ADJ-group with Goguen, Thatch­ er, Wagner and Wright introduced the basic ideas of algebraic specification in the mid seventies in the U. S. A. and Canada, they initiated a very successful and still flourishing new area. In the late seventies, algebraic specification became a major research topic also in many European countries. Originally, the algebraic framework was intended for the mathematical foundation of ab­ stract data types and the formal development of first-order applicative pro­ grams. Meanwhile, the range of applications has been extended to the precise specification of complete software systems, the uniform definition of syntax and semantics of programming languages, and to the stepwise development of correct systems from the requirement definitions to the running programs. The activities in the last 25 years have led to an abundance of concepts, methods, approaches, theories, languages and tools, which are mathemati­ cally founded in universal algebra, category theory and logic.

---

This IFIP state-of-the-art report presents a collection of fundamental high-quality contributions on the algebraic foundations of systems specification. The contributions cover and survey current topics and recent advances, and address such subjects as: the role of formal specification, algebraic preliminaries, partiality, institutions, specification semantics, structuring, refinement, specification languages, term rewriting, deduction and proof systems, object specification, concurrency, and the development process. The authors are well-known experts in the field. The book is an outcome of IFIP WG 1.3 (Foundations of Systems Specification) in cooperation with Esprit Basic Research WG COMPASS, and provides the foundations of the algebraic specification language CASL designed in the CoFI (Common Framework Initiative for Algebraic Specification and Development) project. It is aimed at system developers, researchers, and students.

---

This IFIP state-of-the-art report presents a collection of fundamental high-quality contributions on the algebraic foundations of systems specification. The contributions cover and survey current topics and recent advances, and address such subjects as: the role of formal specification, algebraic preliminaries, partiality, institutions, specification semantics, structuring, refinement, specification languages, term rewriting, deduction and proof systems, object specification, concurrency, and the development process. The authors are well-known experts in the field. The book is an outcome of IFIP WG 1.3 (Foundations of Systems Specification) in cooperation with Esprit Basic Research WG COMPASS, and provides the foundations of the algebraic specification language CASL designed in the CoFI (Common Framework Initiative for Algebraic Specification and Development) project. It is aimed at system developers, researchers, and students.
Content:
Front Matter....Pages I-XII
The Role of Formal Specifications....Pages 1-12
Algebraic Preliminaries....Pages 13-30
From Total Equational to Partial First-Order Logic....Pages 31-104
Institutions: An Abstract Framework for Formal Specifications....Pages 105-130
Specification Semantics....Pages 131-158
Structuring and Modularity....Pages 159-200
Refinement and Implementation....Pages 201-242
Specification Languages....Pages 243-272
Term Rewriting....Pages 273-320
Proof in Flat Specifications....Pages 321-384
Proof Systems for Structured Specifications and Their Refinements....Pages 385-433
Object Specification....Pages 435-465
Algebraic Specification of Concurrent Systems....Pages 467-520
Formalization of the Development Process....Pages 521-562
Back Matter....Pages 563-616

---

This IFIP state-of-the-art report presents a collection of fundamental high-quality contributions on the algebraic foundations of systems specification. The contributions cover and survey current topics and recent advances, and address such subjects as: the role of formal specification, algebraic preliminaries, partiality, institutions, specification semantics, structuring, refinement, specification languages, term rewriting, deduction and proof systems, object specification, concurrency, and the development process. The authors are well-known experts in the field. The book is an outcome of IFIP WG 1.3 (Foundations of Systems Specification) in cooperation with Esprit Basic Research WG COMPASS, and provides the foundations of the algebraic specification language CASL designed in the CoFI (Common Framework Initiative for Algebraic Specification and Development) project. It is aimed at system developers, researchers, and students.
Content:
Front Matter....Pages I-XII
The Role of Formal Specifications....Pages 1-12
Algebraic Preliminaries....Pages 13-30
From Total Equational to Partial First-Order Logic....Pages 31-104
Institutions: An Abstract Framework for Formal Specifications....Pages 105-130
Specification Semantics....Pages 131-158
Structuring and Modularity....Pages 159-200
Refinement and Implementation....Pages 201-242
Specification Languages....Pages 243-272
Term Rewriting....Pages 273-320
Proof in Flat Specifications....Pages 321-384
Proof Systems for Structured Specifications and Their Refinements....Pages 385-433
Object Specification....Pages 435-465
Algebraic Specification of Concurrent Systems....Pages 467-520
Formalization of the Development Process....Pages 521-562
Back Matter....Pages 563-616
....