This Article 
 Bibliographic References 
 Add to: 
A VDM Case Study in Mural
April 1992 (vol. 18 no. 4)
pp. 279-295

The application of an interactive theorem-proving assistant and specification support tool called mural in the specification and verification of a small Vienna development method (VDM) development is described. It is the authors' intention to give a feel for how mural works and of mural's applicability as a tool in specifying and verifying software.

[1] H. Barringer, J. H. Cheng, and C. B. Jones, "A logic covering undefinedness in program proofs,"Acta Informatica, vol. 21, pp. 251-269, 1984.
[2] R. E. Bloomfield and P. K. D. Froome, "The application of formal methods to the development of high integrity software,"IEEE Trans. Software Eng., vol. SE-12, pp. 988-993, 1986.
[3] J. H. Cheng and C. B. Jones, "On the usability of logics which handle partial functions," inProc. 3rd Refinement Workshop, C. Morgan and J. Woodcock, Eds. Berlin: Springer-Verlag, 1990.
[4] O. J. Dahl, D. F. Langmyhr, and O. Owe, "Preliminary report on the specification and programming language ABEL," Dept. Informatics, Univ. Oslo, Res. Rep. 106, 1986.
[5] S. J. Garland and J. V. Guttag, "Using LP to debug specifications," inProc. IFIP TC2 Working Conf. Program. Concepts and Methodol.(Israel), 1990.
[6] D. I. Good, "Mechanical proofs about computer programs," inMathematical Logic and Programming Languages, C.A.R. Hoare and J. C. Shepherdson, Eds. Englewood Cliffs, NJ: Prentice-Hall Int., 1985, pp. 55-75.
[7] M. J. Gordon, "HOL: a machine-oriented formulation of higher-order logic," Univ. Cambridge, Computer Lab., Tech. Rep. 68, 1985.
[8] M. J. Gordon, A. J. Milner, and C. P. Wadsworth, "Edinburgh LCF (Lecture Notes in Computer Sci., vol. 78). Berlin: Springer-Verlag, 1979.
[9] R. Harper, F. Honsell, and G. Plotkin, "A framework for defining logics," inProc. Symp. Logic in Computer Sci.(Ithaca, NY), 1987.
[10] C. B. Jones.Systematic Software Development Using VDM, 2nd ed. Englewood Cliffs, NJ: Prentice-Hall, 1990.
[11] C. B. Jones, K. D. Jones, P. A. Lindsay, and R. Moore, "MURAL: AFormal Development Support System. Berlin: Springer-Verlag, 1991.
[12] C. Lafontaine, "Formalization of the VDM reification in the DEVA meta-calculus: the Human-Leucocyte-Antigen case study," inProc. IFIP TC2 Working Conf. Program. Concepts and Method.(Israel), 1990, pp. 321-356.
[13] P. G. Larsenet al."The dynamic semantics of the BSI/VDM specification language," Instit. Applied Computer Sci. (IFAD), Odense, Denmark, Tech. Rep., Aug. 1990.
[14] P. A. Lindsay, "A survey of mechanical support for formal reasoning,"Software Eng., J., vol. 3, no. 1, 1988.
[15] C. A. Middelburg, "Syntax and semantics of VVSL--a language for structured VDM specifications," Ph.D. thesis, Univ. Amsterdam, 1989.
[16] O. Owe, "An approach to program reasoning based on a first-order logic for partial functions," Dept. Informatics, Univ. Oslo, Res. Rep. 89, 1985.
[17] L. C. Paulson, "The foundations of a generic theorem prover,"J. Auto. Reasoning, vol. 5, pp. 363-397, 1989.
[18] D. Prawitz,Natural Deduction: A Proof Theoretic Study. Stockholm: Almqvist and Wiskell, 1965.
[19] S. Sokolowski, "A note on tactics in LCF," Dept. Computer Sci., Univ. Edinburgh, Int. Rep. CSR-140-83, Aug. 1983.
[20] K. Stølen, "Development of parallel programs on shared data structures," Ph.D. thesis, Dept. Computer Sci. Univ. Manchester, 1990.
[21] J. C. P. Woodcock and B. Dickinson, "Using VDM with rely and guarantee conditions: experiences from a real project," inProc. VDM '88-VDM--The Way Ahead(Lecture Notes in Computer Sci., vol. 328), R. Bloomfield, L. Marshall, and R. Jones, Eds. Berlin: Springer-Verlag, 1988, pp. 434-458.

Index Terms:
VDM; interactive theorem-proving assistant; specification support tool; mural; specification; verification; Vienna development method; formal specification; interactive systems; program verification; software tools; theorem proving
B. Fields, M. Elvang-Goransson, "A VDM Case Study in Mural," IEEE Transactions on Software Engineering, vol. 18, no. 4, pp. 279-295, April 1992, doi:10.1109/32.129217
Usage of this product signifies your acceptance of the Terms of Use.