Book contents
- Frontmatter
- Contents
- Prologue: Faultless systems – yes we can!
- Acknowledgments
- 1 Introduction
- 2 Controlling cars on a bridge
- 3 A mechanical press controller
- 4 A simple file transfer protocol
- 5 The Event-B modeling notation and proof obligation rules
- 6 Bounded re-transmission protocol
- 7 Development of a concurrent program
- 8 Development of electronic circuits
- 9 Mathematical language
- 10 Leader election on a ring-shaped network
- 11 Synchronizing a tree-shaped network
- 12 Routing algorithm for a mobile agent
- 13 Leader election on a connected graph network
- 14 Mathematical models for proof obligations
- 15 Development of sequential programs
- 16 A location access controller
- 17 Train system
- 18 Problems
- Index
15 - Development of sequential programs
Published online by Cambridge University Press: 05 March 2013
- Frontmatter
- Contents
- Prologue: Faultless systems – yes we can!
- Acknowledgments
- 1 Introduction
- 2 Controlling cars on a bridge
- 3 A mechanical press controller
- 4 A simple file transfer protocol
- 5 The Event-B modeling notation and proof obligation rules
- 6 Bounded re-transmission protocol
- 7 Development of a concurrent program
- 8 Development of electronic circuits
- 9 Mathematical language
- 10 Leader election on a ring-shaped network
- 11 Synchronizing a tree-shaped network
- 12 Routing algorithm for a mobile agent
- 13 Leader election on a connected graph network
- 14 Mathematical models for proof obligations
- 15 Development of sequential programs
- 16 A location access controller
- 17 Train system
- 18 Problems
- Index
Summary
In this chapter, we shall see how to develop sequential programs. We present the approach we shall use, and then we propose a large number of examples.
Sequential programs (e.g. loops), when formally constructed, are usually developed gradually by means of a series of progressively more refined “sketches” starting with the formal specification and ending in the final program. Each such sketch is already (although often in a highly non-deterministic form) a monolithic description which resumes the final intended program in terms of a single formula. This is precisely that initial “formula”, that is gradually transformed into the final program.
We are not going to use this approach here. After all, in order to prove a large formula, a logician usually breaks it down into various pieces, on which he performs some simple manipulations before putting them together again in a final proof.
A systematic approach to sequential program development
Components of a sequential program
A sequential program is essentially made up of a number of individual assignments that are glued together by means of various constructs. Typical constructs are sequential composition (;), loop (while), and condition (if). Their role is to explicitly schedule these assignments in a proper order so that the execution of the program can achieve its intended goal.
- Type
- Chapter
- Information
- Modeling in Event-BSystem and Software Engineering, pp. 446 - 480Publisher: Cambridge University PressPrint publication year: 2010