Ebook: VDM '90 VDM and Z — Formal Methods in Software Development: Third International Symposium of VDM Europe Kiel, FRG, April 17–21, 1990 Proceedings

The present volume is the third in a series of VDM Symposia Proceedings. VDM, the Vienna Development Method, is a formal method for software engineering, Z refers to Zermelo, a mathematician whose name is associated with set theory. Many computing science, programming and software engineering proceedings are published regularly. The ones by VDM Europe have the distinguished mark that they are concerned with bringing real theory to apply to real programming. In Europe, there is very much interest in methodology, semantics and techniques, that is, in understanding how we build and what it is that we are building. The papers of these proceedings basically fall into four major groups: Applications, Methodology, Formalisations, and Foundations. The Methodology group has been further subdivided into five areas: Specification Methodology, Design Methodology, Modularity, Object Orientedness, and Processes, Concurrency and Distributed Systems.

---

The present volume is the third in a series of VDM Symposia Proceedings. VDM, the Vienna Development Method, is a formal method for software engineering, Z refers to Zermelo, a mathematician whose name is associated with set theory. Many computing science, programming and software engineering proceedings are published regularly. The ones by VDM Europe have the distinguished mark that they are concerned with bringing real theory to apply to real programming. In Europe, there is very much interest in methodology, semantics and techniques, that is, in understanding how we build and what it is that we are building. The papers of these proceedings basically fall into four major groups: Applications, Methodology, Formalisations, and Foundations. The Methodology group has been further subdivided into five areas: Specification Methodology, Design Methodology, Modularity, Object Orientedness, and Processes, Concurrency and Distributed Systems.

---

The present volume is the third in a series of VDM Symposia Proceedings. VDM, the Vienna Development Method, is a formal method for software engineering, Z refers to Zermelo, a mathematician whose name is associated with set theory. Many computing science, programming and software engineering proceedings are published regularly. The ones by VDM Europe have the distinguished mark that they are concerned with bringing real theory to apply to real programming. In Europe, there is very much interest in methodology, semantics and techniques, that is, in understanding how we build and what it is that we are building. The papers of these proceedings basically fall into four major groups: Applications, Methodology, Formalisations, and Foundations. The Methodology group has been further subdivided into five areas: Specification Methodology, Design Methodology, Modularity, Object Orientedness, and Processes, Concurrency and Distributed Systems.
Content:
Front Matter....Pages -
Object orientation and formal techniques....Pages 1-11
An algebraic approach to refinement....Pages 12-28
Modal logic programming....Pages 29-40
Z specification of an object manager....Pages 41-71
Correctness in the small....Pages 72-98
A formal approach to hypertext using post-prototype formal specification....Pages 99-121
Programming with VDM domains....Pages 122-134
A buffering system implementation using VDM....Pages 135-149
Formal specifications as reusable frameworks....Pages 150-163
Z and the refinement calculus....Pages 164-188
Modularizing the formal description of a database system....Pages 189-210
Modular extensions to Z....Pages 211-232
Adding abstract datatypes to Meta-IV....Pages 233-243
Towards a semantics for object-Z....Pages 244-261
HOOD and Z for the development of complex software systems....Pages 262-289
Using Z as a specification calculus for object-oriented systems....Pages 290-318
Specifying open distributed systems with Z....Pages 319-339
Refinement of state-based concurrent systems....Pages 340-351
Refining data to processes....Pages 352-369
Two approaches towards the formalisation of VDM....Pages 370-398
Type checking BSI/VDM-SL....Pages 399-425
Type inference in Z....Pages 426-451
Recursive definitions revisited....Pages 452-476
Towards the semantics of the definitional language of MetaSoft....Pages 477-503
On conservative extensions of syntax in the process of system development....Pages 504-525
A formal semantics for Z and the link between Z and the relational algebra....Pages 526-551
A naive domain universe for VDM....Pages 552-579
Back Matter....Pages -

---

The present volume is the third in a series of VDM Symposia Proceedings. VDM, the Vienna Development Method, is a formal method for software engineering, Z refers to Zermelo, a mathematician whose name is associated with set theory. Many computing science, programming and software engineering proceedings are published regularly. The ones by VDM Europe have the distinguished mark that they are concerned with bringing real theory to apply to real programming. In Europe, there is very much interest in methodology, semantics and techniques, that is, in understanding how we build and what it is that we are building. The papers of these proceedings basically fall into four major groups: Applications, Methodology, Formalisations, and Foundations. The Methodology group has been further subdivided into five areas: Specification Methodology, Design Methodology, Modularity, Object Orientedness, and Processes, Concurrency and Distributed Systems.
Content:
Front Matter....Pages -
Object orientation and formal techniques....Pages 1-11
An algebraic approach to refinement....Pages 12-28
Modal logic programming....Pages 29-40
Z specification of an object manager....Pages 41-71
Correctness in the small....Pages 72-98
A formal approach to hypertext using post-prototype formal specification....Pages 99-121
Programming with VDM domains....Pages 122-134
A buffering system implementation using VDM....Pages 135-149
Formal specifications as reusable frameworks....Pages 150-163
Z and the refinement calculus....Pages 164-188
Modularizing the formal description of a database system....Pages 189-210
Modular extensions to Z....Pages 211-232
Adding abstract datatypes to Meta-IV....Pages 233-243
Towards a semantics for object-Z....Pages 244-261
HOOD and Z for the development of complex software systems....Pages 262-289
Using Z as a specification calculus for object-oriented systems....Pages 290-318
Specifying open distributed systems with Z....Pages 319-339
Refinement of state-based concurrent systems....Pages 340-351
Refining data to processes....Pages 352-369
Two approaches towards the formalisation of VDM....Pages 370-398
Type checking BSI/VDM-SL....Pages 399-425
Type inference in Z....Pages 426-451
Recursive definitions revisited....Pages 452-476
Towards the semantics of the definitional language of MetaSoft....Pages 477-503
On conservative extensions of syntax in the process of system development....Pages 504-525
A formal semantics for Z and the link between Z and the relational algebra....Pages 526-551
A naive domain universe for VDM....Pages 552-579
Back Matter....Pages -
....