1991 | ReviewPaper | Buchkapitel
Reasoning about VDM developments using the VDM support tool in mural
verfasst von : J. C. Bicarregui, B. Ritchie
Erschienen in: VDM'91 Formal Software Development Methods
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Mural is an interactive mathematical reasoning environment designed to assist the kind of theorem proving tasks that arise when following a formal methods approach to software engineering. It is the result of work carried out at Manchester University and the Rutherford Appleton Laboratory under the Alvey IPSE 2.5 project.Considerable design emphasis has been placed upon the user interface, using the power of workstation technology to present information and to give the user freedom of action backed up by careful dependency tracking. Through this emphasis on the user interface it is hoped to enable users to maintain their intuition of the problem domain and hence guide the proof in the right direction, whilst the mechanical symbolic manipulation of the machine can maintain the integrity of the proof.The Mural proof assistant is generic in that it can be instantiated for reasoning in a variety of logics. Logical theories are constructed in a hierarchical store where collections of declarations and axioms are structured along with derived rules and their proofs. Some effort has been spent on the instantiation of the proof assistant for the formal method VDM. This instantiation includes theories of the logic LPF upon which VDM is based, and of the basic types and functions of VDM.The system includes tools for the construction of VDM specifications and reifications between them and for the generation of the proof obligations that provide the basis of the formal verification of the refinement relationship. It also supports the construction of theories in the proof assistant where it is possible to reason about specifications, reifications and proof obligations. Though there are many more features that would be desirable in a complete environment for VDM, this degree of support has shown that the Mural proof assistant could be used as an integral part of a generic support environment including provision for the formal development of software.This paper concentrates upon the VDM support aspects of Mural: how users can build specifications and reifications between them; and how these are “translated” into Mural theories including the generation of the corresponding proof obligations.