Ebook: Semantics of Specification Languages (SoSL): Proceedings of the International Workshop on Semantics of Specification Languages, Utrecht, The Netherlands, 25 – 27 October 1993

SoSL was the first International Workshop on Semantics of Specification Languages, held from 25-27 October 1993 in Utrecht, the Netherlands. The workshop was organized by the Department of Philosophy of Utrecht University with financial support from the Nationale Faciliteit Informatica of the Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO), and under the auspices of the British Computer Society'S specialist group in Formal Aspects of Computing Science (BCS FACS). The concern of the workshop was the semantics of specification languages, and the issues closely related to this area, such as type checking and the justification of proof rules and proof obligations. Its aim was the exchange of problems and ideas in this field of formal methods, and the identification of common programs of work for further investigation. The program of SoSL consisted of 3 invited lectures presenting the developments of the semantics of 3 major specification languages. Furthermore, there were 16 presentations of submitted papers. This volume provides a direct account of the workshop. It contains 3 papers that match the invited lectures and the 16 selected papers. The editors want to thank all those who have contributed to the workshop; the Program Committee and the referees for selecting the contributed papers, the invited speakers for their interesting talks, the Organizing Committee for all their efforts, and of course the participants. We have the feeling that the workshop was worthwhile and should be repeated.

---

This volume is based on the proceedings of the International Workshop on Semantics of Specification Languages (SoSL), held in Utrecht, the Netherlands, 25-27 October 1993. The aim of the workshop - the first in a proposed series - was to assess various attempts to formally define specification languages, and to identify a programme of work for further investigation. There are currently no other workshops or conferences covering this area. The papers provide a comprehensive overview of research into this important topic, with particular emphasis on recent developments in formal proof systems, proof checking, type consistency, static semantics, and stepwise developments of specifications. In addition to the submitted papers the volume includes three invited papers, each of which outlines the development of the semantics of a major specification language.

---

This volume is based on the proceedings of the International Workshop on Semantics of Specification Languages (SoSL), held in Utrecht, the Netherlands, 25-27 October 1993. The aim of the workshop - the first in a proposed series - was to assess various attempts to formally define specification languages, and to identify a programme of work for further investigation. There are currently no other workshops or conferences covering this area. The papers provide a comprehensive overview of research into this important topic, with particular emphasis on recent developments in formal proof systems, proof checking, type consistency, static semantics, and stepwise developments of specifications. In addition to the submitted papers the volume includes three invited papers, each of which outlines the development of the semantics of a major specification language.
Content:
Front Matter....Pages i-viii
The Development of Z....Pages 1-14
An Overview of the Development of COLD....Pages 15-22
The formal basis for the RAISE specification language....Pages 23-50
The Static Part of the Design Language COLD-K....Pages 51-82
Generation of Proof Obligations for Type Consistency (Extended Abstract)....Pages 83-100
Experiences in Developing a Proof Theory for VDM Specifications....Pages 101-117
Towards Proof Rules for Looseness in Explicit Definitions from VDM-SL....Pages 118-134
Loose Real-Time Communicating Agents....Pages 135-151
A Timed Specification Language for Concurrent Reactive Systems....Pages 152-167
Multiparadigm Specification Languages: a First Attempt at Foundations....Pages 168-185
The Semantics of Extended ML: A Gentle Introduction....Pages 186-215
Type-checking Revisited: Modular Error-handling....Pages 216-231
Proof Theory for µCRL: A Language for Processes with Data.....Pages 232-251
Case Study: Stepwise Development of a Communication Processor using Trace Logic....Pages 252-269
Rendez- Vous with Bundle Event Structures....Pages 270-288
Syntactic Action Refinement in Presence of Multiway Synchronization....Pages 289-303
From Implicit via Inductive to Explicit Definitions....Pages 304-314
Verifying Process Algebra Proofs in Type Theory....Pages 315-339
Reasoning about Dynamic Features in Specification Languages....Pages 340-355
Back Matter....Pages 357-359

---

This volume is based on the proceedings of the International Workshop on Semantics of Specification Languages (SoSL), held in Utrecht, the Netherlands, 25-27 October 1993. The aim of the workshop - the first in a proposed series - was to assess various attempts to formally define specification languages, and to identify a programme of work for further investigation. There are currently no other workshops or conferences covering this area. The papers provide a comprehensive overview of research into this important topic, with particular emphasis on recent developments in formal proof systems, proof checking, type consistency, static semantics, and stepwise developments of specifications. In addition to the submitted papers the volume includes three invited papers, each of which outlines the development of the semantics of a major specification language.
Content:
Front Matter....Pages i-viii
The Development of Z....Pages 1-14
An Overview of the Development of COLD....Pages 15-22
The formal basis for the RAISE specification language....Pages 23-50
The Static Part of the Design Language COLD-K....Pages 51-82
Generation of Proof Obligations for Type Consistency (Extended Abstract)....Pages 83-100
Experiences in Developing a Proof Theory for VDM Specifications....Pages 101-117
Towards Proof Rules for Looseness in Explicit Definitions from VDM-SL....Pages 118-134
Loose Real-Time Communicating Agents....Pages 135-151
A Timed Specification Language for Concurrent Reactive Systems....Pages 152-167
Multiparadigm Specification Languages: a First Attempt at Foundations....Pages 168-185
The Semantics of Extended ML: A Gentle Introduction....Pages 186-215
Type-checking Revisited: Modular Error-handling....Pages 216-231
Proof Theory for µCRL: A Language for Processes with Data.....Pages 232-251
Case Study: Stepwise Development of a Communication Processor using Trace Logic....Pages 252-269
Rendez- Vous with Bundle Event Structures....Pages 270-288
Syntactic Action Refinement in Presence of Multiway Synchronization....Pages 289-303
From Implicit via Inductive to Explicit Definitions....Pages 304-314
Verifying Process Algebra Proofs in Type Theory....Pages 315-339
Reasoning about Dynamic Features in Specification Languages....Pages 340-355
Back Matter....Pages 357-359
....