Ebook: VDM '88 VDM — The Way Ahead: 2nd VDM-Europe Symposium Dublin, Ireland, September 11–16, 1988 Proceedings

This volume presents the proceedings of the 2nd VDM-Europe Symposium held in Dublin, Ireland, September 12-16, 1988. VDM, the Vienna Development Method, is a formal method for software engineering. It is being applied to an increasing number of projects by companies throughout Europe and there is an active international research programme supporting this process. "VDM - The Way Ahead" is the second of a series of symposia sponsored by the Commission of the European Communities (CEC) and organised by VDM-Europe. The term "formal method" refers to mathematically formal software specification and production methods. These methods aim to increase the quality of software in two related ways: by improving the specification and by making verification during the software production process more effective and easier to audit. The symposium proceedings focus on five areas of interest: education and technology transfer, experience and use of VDM, tools and support environments, method development and foundation at work, the standardisation of VDM. The proceedings are of interest to all those concerned with the application of more rigorous approaches to software development and the associated theoretical foundations.

---

This volume presents the proceedings of the 2nd VDM-Europe Symposium held in Dublin, Ireland, September 12-16, 1988. VDM, the Vienna Development Method, is a formal method for software engineering. It is being applied to an increasing number of projects by companies throughout Europe and there is an active international research programme supporting this process. "VDM - The Way Ahead" is the second of a series of symposia sponsored by the Commission of the European Communities (CEC) and organised by VDM-Europe. The term "formal method" refers to mathematically formal software specification and production methods. These methods aim to increase the quality of software in two related ways: by improving the specification and by making verification during the software production process more effective and easier to audit. The symposium proceedings focus on five areas of interest: education and technology transfer, experience and use of VDM, tools and support environments, method development and foundation at work, the standardisation of VDM. The proceedings are of interest to all those concerned with the application of more rigorous approaches to software development and the associated theoretical foundations.

---

This volume presents the proceedings of the 2nd VDM-Europe Symposium held in Dublin, Ireland, September 12-16, 1988. VDM, the Vienna Development Method, is a formal method for software engineering. It is being applied to an increasing number of projects by companies throughout Europe and there is an active international research programme supporting this process. "VDM - The Way Ahead" is the second of a series of symposia sponsored by the Commission of the European Communities (CEC) and organised by VDM-Europe. The term "formal method" refers to mathematically formal software specification and production methods. These methods aim to increase the quality of software in two related ways: by improving the specification and by making verification during the software production process more effective and easier to audit. The symposium proceedings focus on five areas of interest: education and technology transfer, experience and use of VDM, tools and support environments, method development and foundation at work, the standardisation of VDM. The proceedings are of interest to all those concerned with the application of more rigorous approaches to software development and the associated theoretical foundations.
Content:
Front Matter....Pages -
Computing is a physical science....Pages 1-1
Structuring for the VDM specification language....Pages 2-25
Correctness for beginners....Pages 26-47
Understanding an informal description: Office documents architecture, an ISO standard....Pages 48-63
Towards a formal definition of GKS and other graphics standards....Pages 64-73
Report from the BSI panel for the standardisation of VDM (IST/5/50)....Pages 74-78
Formal methods in standards—A report from the BCS working group....Pages 79-85
The B tool (Abstract)....Pages 86-87
Specification of an operating system kernel forest and VDM compared....Pages 88-100
Compiler prototyping with VDM and standard ML....Pages 101-115
VDM development with Ada as the target language....Pages 116-123
NUSL: An executable specification language based on data abstraction....Pages 124-138
A support system for formal reasoning: Requirements and status....Pages 139-152
The use of VDM within the Alvey Flagship project....Pages 153-166
The formal definition of modula-2 and its associated interpreter....Pages 167-177
Test case selection using VDM....Pages 178-186
The VIP VDM Specification Language....Pages 187-201
Sample — A functional language....Pages 202-217
A three-valued logic for software specification and validation....Pages 218-242
Three-valued predicates for software specification and validation....Pages 243-266
A set-theoretic model for a typed polymorphic lambda calculus a contribution to MetaSoft....Pages 267-298
Mutually recursive algebraic domain equations....Pages 299-317
Proof rules for VDM statements....Pages 318-336
Muffin: A user interface design experiment for a Theorem Proving Assistant....Pages 337-375
The RAISE language, method and tools....Pages 376-405
Correctness proofs for META IV written code generator specifications using term rewriting....Pages 406-433
Using VDM with rely and guarantee-conditions....Pages 434-458
Software support for the refinement of VDM specifications....Pages 459-475
The use of VDM in the specification of Chinese characters....Pages 476-499

---

This volume presents the proceedings of the 2nd VDM-Europe Symposium held in Dublin, Ireland, September 12-16, 1988. VDM, the Vienna Development Method, is a formal method for software engineering. It is being applied to an increasing number of projects by companies throughout Europe and there is an active international research programme supporting this process. "VDM - The Way Ahead" is the second of a series of symposia sponsored by the Commission of the European Communities (CEC) and organised by VDM-Europe. The term "formal method" refers to mathematically formal software specification and production methods. These methods aim to increase the quality of software in two related ways: by improving the specification and by making verification during the software production process more effective and easier to audit. The symposium proceedings focus on five areas of interest: education and technology transfer, experience and use of VDM, tools and support environments, method development and foundation at work, the standardisation of VDM. The proceedings are of interest to all those concerned with the application of more rigorous approaches to software development and the associated theoretical foundations.
Content:
Front Matter....Pages -
Computing is a physical science....Pages 1-1
Structuring for the VDM specification language....Pages 2-25
Correctness for beginners....Pages 26-47
Understanding an informal description: Office documents architecture, an ISO standard....Pages 48-63
Towards a formal definition of GKS and other graphics standards....Pages 64-73
Report from the BSI panel for the standardisation of VDM (IST/5/50)....Pages 74-78
Formal methods in standards—A report from the BCS working group....Pages 79-85
The B tool (Abstract)....Pages 86-87
Specification of an operating system kernel forest and VDM compared....Pages 88-100
Compiler prototyping with VDM and standard ML....Pages 101-115
VDM development with Ada as the target language....Pages 116-123
NUSL: An executable specification language based on data abstraction....Pages 124-138
A support system for formal reasoning: Requirements and status....Pages 139-152
The use of VDM within the Alvey Flagship project....Pages 153-166
The formal definition of modula-2 and its associated interpreter....Pages 167-177
Test case selection using VDM....Pages 178-186
The VIP VDM Specification Language....Pages 187-201
Sample — A functional language....Pages 202-217
A three-valued logic for software specification and validation....Pages 218-242
Three-valued predicates for software specification and validation....Pages 243-266
A set-theoretic model for a typed polymorphic lambda calculus a contribution to MetaSoft....Pages 267-298
Mutually recursive algebraic domain equations....Pages 299-317
Proof rules for VDM statements....Pages 318-336
Muffin: A user interface design experiment for a Theorem Proving Assistant....Pages 337-375
The RAISE language, method and tools....Pages 376-405
Correctness proofs for META IV written code generator specifications using term rewriting....Pages 406-433
Using VDM with rely and guarantee-conditions....Pages 434-458
Software support for the refinement of VDM specifications....Pages 459-475
The use of VDM in the specification of Chinese characters....Pages 476-499
....