The B Method is a complete formal development process for mathematically transforming software systems from specification into code. This thesis provides the reader with an overview of that method, including a description of the development notation (Abstract Machine Notation) and its application on a case study. The main part of the thesis considers ways in which the B Method may be used and extended so as to provide a platform for the generation of SPARK code. SPARK is a subset of Ada recommended for implementing safety-critical software. Details are given on how this translation process is achieved and how it is implemented by a set of rule bases which can be executed by a theorem proving environment called the B-Tool. The current tool support for the B Method (the B Toolkit) contains a translator from B into C code. The translation process from B to C is compared with the B to SPARK translation process outlined in this thesis and conclusions are drawn as to how user-confidence is increased by translation into a programming language which is type rich, supports the structuring of programs and may be statically analysed.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:618640 |
| Date | January 1995 |
| Creators | Storey, A. C. |
| Publisher | London South Bank University |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0016 seconds