Please use this identifier to cite or link to this item:

TitleA reification calculus for model-oriented software specification
Author(s)Oliveira, José Nuno Fonseca
Algebraic specification
Formal methods
Software engineering
Transformational design
Issue dateApr-1990
PublisherSpringer Verlag
JournalFormal Aspects of Computing
Citation"Formal aspects of computing : the international journal of formal methods". ISSN 0934-5034. 2 (1990) 1-23.
Abstract(s)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 appli- cable to the transformation of models written in Meta-iv (the specification lan- guage 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-called final semantics “`a la Wand”: a specification “is” a model (heterogeneous algebra) which is the final ob ject (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.
Appears in Collections:DI/CCTC - Artigos (papers)
HASLab - Artigos em revistas internacionais

Files in This Item:
File Description SizeFormat 
fac90.pdfDocumento principal260,37 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu Currículo DeGóis