Sciweavers

LOPSTR
2007
Springer

Snapshot Generation in a Constructive Object-Oriented Modeling Language

13 years 9 months ago
Snapshot Generation in a Constructive Object-Oriented Modeling Language
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.
Mauro Ferrari, Camillo Fiorentini, Alberto Momigli
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where LOPSTR
Authors Mauro Ferrari, Camillo Fiorentini, Alberto Momigliano, Mario Ornaghi
Comments (0)