Abstract
This paper presents a transformational approach to the derivation of implementations from model-oriented specifications of abstract data types.
The purpose of this research is to reduce the number of formal proofs required in model refinement, which hinder software development. It is shown to be applicable to the transformation of models written in META-IV (the specification language of VDM) towards their refinement into, for example, Pascal or relational DBMSs. The approach includes the automatic synthesis of retrieve functions between models, and data-type invariants.
The underlying algebraic semantics is the so-calledfinal semantics “à la Wand”: a specification “is” amodel (heterogeneous algebra) which is the final object (up to isomorphism) in the category of all its implementations.
The transformational calculus approached in this paper follows from exploring the properties of finite, recursively defined sets.
This work extends the well-known strategy of program transformation to model transformation, adding to previous work on a transformational style for operation-decomposition in META-IV. The model-calculus is also useful for improving model-oriented specifications.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Backus, J.: Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs.CACM, 21(8), 613–641 (1978).
Bauer, F. L. and Wössner, H.:Algorithmic Language and Program Development. Springer-Verlag, 1982.
Burstall, R. M. and Darlington J.: A Transformation System for Developing Recursive Programs.JACM, 24(1), 44–67 (1977).
Darlington, J.: Program Transformation.Functional Programming and Its Applications: An Advanced Course, Newcastle University, Cambridge University Press, 1982.
Fiadeiro, J. L.: Cálculo de Objectos e Eventos. Ph.D. dissertation, IST-University of Lisbon, Portugal, 1989 (in Portuguese).
Fielding, E.: The Specification of Abstract Mappings and Their Implementation as B+-Trees. PRG-18, Oxford University, September 1980.
Goguen, J. and Meseguer, J.:Unifying Functional, Object-oriented and Relational Programming with Logical Semantics. SRI International, 1987.
Goguen, J., Thatcher, J. W. and Wagner, E. G.:Initial Algebra Approach to the Specification, Correctness and Implementation of Algebraic Data Types. Current Trends in Programming Technology, Vol. IV, Prentice-Hall, 1978.
Guttag, J. V. and Horning, J. J.: The Algebraic Specification of Abstract Data Types.Acta Informatica, 10, 27–52 (1978).
Hayes, I. (Ed.):Specification Case Studies. Series in Computer Science, C. A. R. Hoare (ed.), Prentice-Hall International, 1987.
Henderson, P.: me too: A Languare for Software Specification and Model-Building-Preliminary Report. University of Stirling, December 1984.
Hoare, C. A. R.: Data Refinement in a Categorical Setting. PRG, Oxford University, June 1987.
Hoare, C. A. R., Jifeng, He and Sanders, J. W.: Prespecification in Data Refinement.Information Processing Letters, 25, 71–76 (1987).
Jones, C. B.;Software Development — a Rigorous Approach. Series in Computer Science, C. A. R. Hoare (ed.), Prentice-Hall International, 1980.
Jones, C. B.:Systematic Software Development Using VDM. Series in Computer Science, C. A. R. Hoare (ed.), Prentice-Hall International, 1986.
MacLane, S.:Categories for the Working Mathematician. Springer-Verlag, New-York, 1971.
Manes, E. G. and Arbib, M. A.:Algebraic Approaches to Program Semantics. Texts and Monographs in Computer Science, D. Gries (ed.), Springer-Verlag, 1986.
Manna, Z.:Mathematical Theory of Computation. McGraw-Hill, New York, 1974.
Milner, R.:Communication and Concurrency. Series in Computer Science, C. A. R. Hoare (ed.), Prentice-Hall International, 1989.
Moreira, C., Reis, A., Jesus, R. and Barros, A.: Especificação Formal de um Sistema para Conservatórias de Registo Predial. U. Minho, Technical Report CCES-OP3:R1/88, May 1988 (in Portuguese).
Nipkow, T.: Nondeterministic Data Types: Models and Implementations.Acta Informatica, 22, 629–661 (1986).
Oliveira, J. N.: The Transformational Paradigm as a Means of Smoothing Abrupt Software Design Steps. U. Minho, Technical Report CCES-JNO:R2/85, December 1985.
Oliveira, J. N.: Refinamento Transformacional de Especificações (Terminais).Proc. XII Iberian “Jornadas” on Mathematics, May 1987, Braga, Portugal (in Portuguese).
Oliveira, J. N.: Transformational Refinement of Formal (Model-oriented) Specifications. Internal Report CCES-JNO:R1/87, University of Minho, Braga, Portugal (updated: June 1988).
Oliveira, J. N.:SETS — Uma Linguagem de Especificação Quase Centenária. CCES Seminar (1988/89 series), University of Minho, July 1988 (in Portuguese).
Oliveira, J. N.: Transforming Specifications: Between the Model-oriented and the Object-oriented Style. CCES, U. Minho, Technical Report (in preparation).
Oliveira, J. N.: Algebraic Specification in a CCS-Extension to Modular-VDM. Invited communication, Section C4 (Computing Science Foundations), 1989National Meeting of the Portuguese Mathematical Society, Oporto, 3 April 1989.
Sernadas, A., Fiadeiro, J., Sernadas, C. and Ehrich, H.-D.: Abstract Object Types: A Temporal Perspective.Colloquium on Temporal Logic and Specification, A. Pnueli, H. Barringer and Banieqbal, B. (eds), Springer-Verlag.
Spivey, J. M.:The Z Notarion — A Reference Manual. Series in Computer Science, C. A. R. Hoare (ed.), Prentice-Hall International, 1989.
Valença, J. M.: Formal Programming: an Algebraic Approach — Part 1: An Algebra of Functions and a Semantics for Imperative Languages. Invited paper,Proc. XII Iberian “Jornadas” on Mathematics, May 1987, Braga, Portugal.
Wand, M.: Final Algebraic Semantics and Data Type Extensions.JCSS, 19, 27–44 (1979).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Oliveira, J.N. A reification calculus for model-oriented software specification. Formal Aspects of Computing 2, 1–23 (1990). https://doi.org/10.1007/BF01888215
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF01888215