| Summary: | Refinement is a long-established technique that is widely used in the rigorous development of software. It can be argued that refinement has limitations that prevent it being used effectively in a wide range of system implementations. These claims led to the introduction of a liberalized form of refinement known as retrenchment. Whilst, when using retrenchment, we lose some of refinement's guarantees, we are able to describe the construction of specifications in situations where refinement struggles to provide a clear and concise picture. It is hoped therefore, that the use of retrenchment - alongside refinement - will increase the scope of system developments to which formal methods can be successfully applied. It has been generally recognized that it is not feasible to apply formal methods to the development of complex systems without suitable tool support. Following an attempt to integrate retrenchment into the B-Toolkit where the inflexibility of the application made change difficult - we decided to create a new tool that was capable not only of supporting the specification and proof of refinement and retrenchment, but any similar relationship. Our aim was to make the notion of the model and the relationship between models fully configurable, allowing the user to specify and prove with existing formal techniques, but also to be able to experiment in the creation of new techniques. vVe chose to use the Z notation as the principal syntax for expressing our models and relationships. As the international standard for Z had only recently been published, we were also required to create one of the first Z tools that conformed (loosely) to this standard.
|
|---|
