CooML is an object-oriented modeling language where specifications are theories in a constructive logic designed to handle incomplete information. In this logic we view snapshots as a formal counterpart of object populations, which are associated with specifications via the constructive interpretation of logical connectives. In this paper, we introduce the “snapshot semantics” of CooML and we describe a snapshot generation (SG) algorithm, which can be applied to validate specifications in the spirit of OCL-like constraints over UML models. Differently from the latter and from the standard BHK semantics, the logic allows us to exploit a notion of partial validation that is appropriate to encodings characterised by incomplete information. SG is akin to model generation in answer set programming. We show that the algorithm is sound and complete so that its successful termination implies consistency of the system.
Snapshot generation in a constructive object-oriented modeling language / M. Ferrari, C. Fiorentini, A. Momigliano, M. Ornaghi - In: Logic-based program synthesis and transformation : 17th international symposium, LOPSTR 2007 : Kongens Lyngby, Denmark, august 23-24, 2007 : revised selected Papers / [a cura di] A. King. - Berlin : Springer, 2008. - ISBN 9783540787686. - pp. 169-184 (( Intervento presentato al 17. convegno International Symposium LOPSTR tenutosi a Kongens Lyngby, Denmark nel 2007.
Snapshot generation in a constructive object-oriented modeling language
C. Fiorentini;A. Momigliano;M. Ornaghi
2008
Abstract
CooML is an object-oriented modeling language where specifications are theories in a constructive logic designed to handle incomplete information. In this logic we view snapshots as a formal counterpart of object populations, which are associated with specifications via the constructive interpretation of logical connectives. In this paper, we introduce the “snapshot semantics” of CooML and we describe a snapshot generation (SG) algorithm, which can be applied to validate specifications in the spirit of OCL-like constraints over UML models. Differently from the latter and from the standard BHK semantics, the logic allows us to exploit a notion of partial validation that is appropriate to encodings characterised by incomplete information. SG is akin to model generation in answer set programming. We show that the algorithm is sound and complete so that its successful termination implies consistency of the system.File | Dimensione | Formato | |
---|---|---|---|
sg.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
558.8 kB
Formato
Adobe PDF
|
558.8 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.