×

Domain-specific semantics and data refinement of object models. (English) Zbl 1279.68184

Moreira, Anamaria Martins (ed.) et al., Proceedings of the Brazilian symposium on formal methods (SBMF 2006), Natal, Rio Grande de Norte, Brazil, September 17–23, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 195, 151-170 (2008).
Summary: This paper shows how a domain-specific semantics for object models can be used to support the development of transformations that reflect a particular implementation strategy. The semantics captures model constraints and domain assumptions in terms of abstract data types, and a transformation is correct if and only if it corresponds to a data refinement. The transformations represent development steps, involving the completion of method descriptions, and validity checks, addressing issues of definedness and consistency. The paper shows how compositions of transformations may be used for the automatic generation of working systems from formal, object-oriented designs.
For the entire collection see [Zbl 1276.68022].

MSC:

68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Simula 67; Eiffel
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Leino, K. R.M., A logic of object-oriented programs, (Verification: Theory and Practice (2003)), 11-41 · Zbl 1274.68055
[2] Abrial, J.-R., The B-book: assigning programs to meanings (1996), Cambridge University Press · Zbl 0915.68015
[3] Dahl, O.; Nygaard, K., Simula, an Algol-based simulation language, Communications of the ACM, 9, 671-678 (1966) · Zbl 0139.32903
[4] Davies, J.; Crichton, C.; Crichton, E.; Neilson, D.; Sørensen, I. H.; Mota, A.; Moura, A., Formality, evolution, and model-driven software engineering, SBMF 2004. SBMF 2004, ENTCS, 130, 39-55 (2005)
[5] Duke, R.; Rose, G., Formal Object-Oriented Specification Using Object-Z (2000), Macmillan Press
[6] Faitelson, D., Welch, J., and Davies, J. (2006). From predicates to programs. In Sampaio, A., editor, Proceedings of SBMF 2005; Faitelson, D., Welch, J., and Davies, J. (2006). From predicates to programs. In Sampaio, A., editor, Proceedings of SBMF 2005 · Zbl 1279.68054
[7] Fowler, M.; Beck, K.; Brant, J.; Opdyke, W.; Roberts, D., Refactoring: Improving the Design of Existing Code (1999), Addison-Wesley
[8] Griffiths, A. (1995). An Extended Semantic Foundation For Object-Z. Technical report, SVRC, University of Queensland; Griffiths, A. (1995). An Extended Semantic Foundation For Object-Z. Technical report, SVRC, University of Queensland
[9] Hall, A., Using Z as a Specification Calculus for Object-Oriented Systems, (Proceedings of VDM ’90 (1990), Springer-Verlag), 290-318
[10] Jifeng, H.; Li, X.; Liu, Z., rcos: a refinement calculus of object systems, Theor. Comput. Sci., 365, 1, 109-142 (2006) · Zbl 1118.68049
[11] Kleppe, A.; Warmer, J.; Bast, W., MDA Explained, The Model Driven Architecture: Practice and Promise (2003), Addison-Wesley
[12] Liskov, B., Data abstraction and hierarchy, (Proceedings of OOPSLA ’87 (1987), ACM Press), 17-34
[13] Liskov, B.; Wing, J., A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems, 16, 6, 1811-1841 (1994)
[14] McComb, T.; Smith, G., Compositional class refinement in object-z, (FM 2006. FM 2006, LNCS, volume 4085 (2006), Springer)
[15] Meyer, B., Object-Oriented Software Construction (1997), Prentice Hall · Zbl 0987.68516
[16] Morgan, C. C., Programming From Specifications (1998), Prentice Hall
[17] OMG, UML 2.0 superstructure specification (2005)
[18] Smith, G., The Object-Z Specification Language (2000), Kluwer · Zbl 0944.68124
[19] Spivey, J. M., The Z Notation (1992), Prentice Hall · Zbl 0777.68003
[20] van den Berg, J., Breunesse, C.-B., Jacobs, B., and Poll, E. (2001). On the role of invariants in reasoning about object-oriented languages. In Proceedings of ECOOP’2001; van den Berg, J., Breunesse, C.-B., Jacobs, B., and Poll, E. (2001). On the role of invariants in reasoning about object-oriented languages. In Proceedings of ECOOP’2001
[21] Warmer, J.; Kleppe, A., The Object Constraint Language: Getting Your Models Ready for MDA (2003), Addison Wesley
[22] Welch, J.; Faitelson, D.; Davies, J., Automatic maintenance of association invariants, (Proceedings of SEFM 2005 (2005), IEEE Press)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.