×

From predicates to programs: the semantics of a method language. (English) Zbl 1279.68054

Sampaio, Augusto (ed.), Proceedings of the second Brazilian symposium on formal methods (SBMF 2005), Porto Alegre, RS, Brazil, November 30, 2005. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 184, 171-187 (2007).
Summary: This paper explains how a declarative method language, based upon the formal notations of Z and B, can be used as a basis for automatic code generation. The language is used to describe the intended effect of operations, or methods, upon the components of an object model; each method is defined by a pair of predicates: a precondition, and a post-condition. Following the automatic incorporation of model invariants, including those arising from class associations, these predicates are extended – again, automatically – to address issues of consistency, definition, and dependency, before being translated into imperative programs. The result is a formal method for transforming object models into complete, working systems.
For the entire collection see [Zbl 1275.68031].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Spec#
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrial, J.-R., The B-book: assigning programs to meanings (1996), Cambridge University Press · Zbl 0915.68015
[2] Barnett, Mike; Leino, K. Rustan M.; Schulte, Wolfram, The Spec# programming system: An overview, (CASSIS 2004. CASSIS 2004, LNCS (2004), Springer)
[3] Barnett, Mike; Naumann, David A., Friends need a bit more: Maintaining invariants over shared state, (MPC 2004. MPC 2004, LNCS (2004), Springer) · Zbl 1106.68338
[4] Cavalcanti, A.; Woodcock, J., A Weakest Precondition Semantics for Z, The Computer Journal, 41, 1 (1998) · Zbl 0906.68093
[5] Davies, J.; Crichton, C.; Crichton, E.; Neilson, D.; Sørensen, Ib H., Formality, evolution, and model-driven software engineering, (Mota, Alexandre; Moura, Arnaldo, Proceedings of SBMF 2004. Proceedings of SBMF 2004, ENTCS (2005))
[6] Dijkstra, E. W.; Feijen, W. H., A Method of Programming (1988), Addison-Wesley · Zbl 0681.68001
[7] Greenfield, J.; Short, K.; Cook, S.; Kent, S., Software Factories: assembling applications with patterns, models, frameworks, and tools (2004), Wiley
[8] Kleppe, A.; Warmer, J.; Bast, W., MDA Explained, The Model Driven Architecture: Practice and Promise (2003), Addison-Wesley
[9] Lucas, J.-Y.; Dormoy, J.-L.; Ginoux, B.; Jimenez-Dominguez, C.; Pierre, L., How to reconcile formal specifications and automatic programming: The Descartes system, (APSEC ’98 (1998), IEEE Press)
[10] Manna, Z.; Waldinger, R. J., Toward automatic program synthesis, Commun. ACM, 14, 3 (1971) · Zbl 0214.43006
[11] Morgan, C. C., Programming From Specifications (1998), Prentice Hall
[12] Nelson, G., A generalization of Dijkstra’s calculus, ACM Trans. Program. Lang. Syst., 11, 4 (1989)
[13] Prywes, N.; Amir, S.; Shastry, S., Use of a nonprocedural specification language and associated program generator in software development, ACM Trans. Program. Lang. Syst., 1, 2 (1979) · Zbl 0452.68039
[14] Smith, G., The Object-Z Specification Language (2000), Kluwer · Zbl 0944.68124
[15] C. Snook and M. Butler. UML-B: Formal modelling and design aided by UML. Technical report, Electronics and Computer Science, Southampton, 2004; C. Snook and M. Butler. UML-B: Formal modelling and design aided by UML. Technical report, Electronics and Computer Science, Southampton, 2004
[16] Spivey, J. M., The Z Notation (1992), Prentice Hall · Zbl 0777.68003
[17] Warmer, J.; Kleppe, A., The Object Constraint Language: Getting Your Models Ready for MDA (2003), Addison Wesley
[18] J. Welch, D. Faitelson, and J. Davies. Automatic maintenance of association invariants. In Proceedings of SEFM 2005. IEEE Press, 2005. To appear; J. Welch, D. Faitelson, and J. Davies. Automatic maintenance of association invariants. In Proceedings of SEFM 2005. IEEE Press, 2005. To appear
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.