Specification of Properties
Data space signatures have been used to specify the static structure of transformation systems, i.e., their data states and their actions. Beyond that it is important to have means for the specification of their semantic properties, such that the desired properties of the systems can be modelled. These properties can be classified according to the structure of transformation systems. Their data states are given by partial algebras, whose properties are described by equations, more precisely conditional existence equations (see [Rei87, CGW95] and Appendix A). A data state transformation T : C ⇒ D is given by the commencing and the ending states C and D and a label T = 〈act, ~〉 that consists of an action set and a tracking relation. The two data states can be specified by a pair of sets of equations, describing pre- and postconditions of the transformation. Together with a formal action expression for the specification of the action set act this yields a transformation rule. The relation of the elements of the data states C and D is given by the tracking relation ~ that now allows the evaluation of the common variables of the two sets of equations of the transformation rule by identified (=related) elements in the two different algebras. In this way relations between the values of functions and constants before and after the execution of the actions of the transformation can be expressed. Note that this concept of transformation rules also allows the specification of dynamic properties w.r.t. mutable carrier sets, for instance in the case of creation and deletion of elements.
Unable to display preview. Download preview PDF.