{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T17:03:51Z","timestamp":1694624631793},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1990,3,1]],"date-time":"1990-03-01T00:00:00Z","timestamp":636249600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1990,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper presents a transformational approach to the derivation of implementations from model-oriented specifications of abstract data types.<\/jats:p>\n          <jats:p>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.<\/jats:p>\n          <jats:p>\n            The underlying algebraic semantics is the so-called\n            <jats:italic>final<\/jats:italic>\n            semantics \u201c\u00e0 la Wand\u201d: a specification \u201cis\u201d a\n            <jats:italic>model<\/jats:italic>\n            (heterogeneous algebra) which is the final object (up to isomorphism) in the category of all its implementations.\n          <\/jats:p>\n          <jats:p>The transformational calculus approached in this paper follows from exploring the properties of finite, recursively defined sets.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/bf01888215","type":"journal-article","created":{"date-parts":[[2005,7,4]],"date-time":"2005-07-04T21:23:27Z","timestamp":1120512207000},"page":"1-23","source":"Crossref","is-referenced-by-count":22,"title":["A reification calculus for model-oriented software specification"],"prefix":"10.1145","volume":"2","author":[{"given":"J. N.","family":"Oliveira","sequence":"first","affiliation":[{"name":"Grupo de C. Computa\u00e7\u00e3o, Universidade do Minho\/INESC, Rua D. Pedro V, 88-3, 4700, Braga, Portugal"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359579"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bauer F. L. and W\u00f6ssner H.: Algorithmic Language and Program Development . Springer-Verlag 1982.","DOI":"10.1007\/978-3-642-61807-9"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"key":"e_1_2_1_2_4_2","unstructured":"Darlington J.: Program Transformation. Functional Programming and Its Applications: An Advanced Course Newcastle University Cambridge University Press 1982."},{"key":"e_1_2_1_2_5_2","volume-title":"C\u00e1lculo de Objectos e Eventos. Ph.D. dissertation","author":"Fiadeiro J. L.","year":"1989"},{"key":"e_1_2_1_2_6_2","unstructured":"Fielding E.: The Specification of Abstract Mappings and Their Implementation as B + -Trees. PRG-18 Oxford University September 1980."},{"key":"e_1_2_1_2_7_2","unstructured":"Goguen J. and Meseguer J.: Unifying Functional Object-oriented and Relational Programming with Logical Semantics . SRI International 1987."},{"key":"e_1_2_1_2_8_2","unstructured":"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."},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260922"},{"key":"e_1_2_1_2_10_2","unstructured":"Hayes I. (Ed.): Specification Case Studies . Series in Computer Science C. A. R. Hoare (ed.) Prentice-Hall International 1987."},{"key":"e_1_2_1_2_11_2","unstructured":"Henderson P.: me too: A Languare for Software Specification and Model-Building-Preliminary Report. University of Stirling December 1984."},{"key":"e_1_2_1_2_12_2","unstructured":"Hoare C. A. R.: Data Refinement in a Categorical Setting. PRG Oxford University June 1987."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(87)90224-9"},{"key":"e_1_2_1_2_14_2","unstructured":"Jones C. B.; Software Development \u2014 a Rigorous Approach . Series in Computer Science C. A. R. Hoare (ed.) Prentice-Hall International 1980."},{"key":"e_1_2_1_2_15_2","unstructured":"Jones C. B.: Systematic Software Development Using VDM. Series in Computer Science C. A. R. Hoare (ed.) Prentice-Hall International 1986."},{"key":"e_1_2_1_2_16_2","volume-title":"Categories for the Working Mathematician","author":"MacLane S.","year":"1971"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Manes E. G. and Arbib M. A.: Algebraic Approaches to Program Semantics . Texts and Monographs in Computer Science D. Gries (ed.) Springer-Verlag 1986.","DOI":"10.1007\/978-1-4612-4962-7"},{"key":"e_1_2_1_2_18_2","volume-title":"Mathematical Theory of Computation","author":"Manna Z.","year":"1974"},{"key":"e_1_2_1_2_19_2","unstructured":"Milner R.: Communication and Concurrency . Series in Computer Science C. A. R. Hoare (ed.) Prentice-Hall International 1989."},{"key":"e_1_2_1_2_20_2","unstructured":"Moreira C. Reis A. Jesus R. and Barros A.: Especifica\u00e7\u00e3o Formal de um Sistema para Conservat\u00f3rias de Registo Predial. U. Minho Technical Report CCES-OP3:R1\/88 May 1988 (in Portuguese)."},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263649"},{"key":"e_1_2_1_2_22_2","unstructured":"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."},{"key":"e_1_2_1_2_23_2","unstructured":"Oliveira J. N.: Refinamento Transformacional de Especifica\u00e7\u00f5es (Terminais). Proc. XII Iberian \u201cJornadas\u201d on Mathematics May 1987 Braga Portugal (in Portuguese)."},{"key":"e_1_2_1_2_24_2","volume-title":"Internal Report CCES-JNO:R1\/87","author":"Oliveira J. N.","year":"1988"},{"key":"e_1_2_1_2_25_2","unstructured":"Oliveira J. N.: SETS \u2014 Uma Linguagem de Especifica\u00e7\u00e3o Quase Centen\u00e1ria. CCES Seminar (1988\/89 series) University of Minho July 1988 (in Portuguese)."},{"key":"e_1_2_1_2_26_2","unstructured":"Oliveira J. N.: Transforming Specifications: Between the Model-oriented and the Object-oriented Style. CCES U. Minho Technical Report (in preparation)."},{"key":"e_1_2_1_2_27_2","volume-title":"Invited communication, Section C4 (Computing Science Foundations)","author":"Oliveira J. N.","year":"1989"},{"key":"e_1_2_1_2_28_2","unstructured":"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."},{"key":"e_1_2_1_2_29_2","unstructured":"Spivey J. M.: The Z Notarion \u2014 A Reference Manual . Series in Computer Science C. A. R. Hoare (ed.) Prentice-Hall International 1989."},{"key":"e_1_2_1_2_30_2","unstructured":"Valen\u00e7a J. M.: Formal Programming: an Algebraic Approach \u2014 Part 1: An Algebra of Functions and a Semantics for Imperative Languages. Invited paper Proc. XII Iberian \u201cJornadas\u201d on Mathematics May 1987 Braga Portugal."},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90011-4"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01888215.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01888215\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01888215","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:20:08Z","timestamp":1641482408000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01888215"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,3]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1990,3]]}},"alternative-id":["10.1007\/BF01888215"],"URL":"https:\/\/doi.org\/10.1007\/bf01888215","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,3]]}}}