Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 41) +++ /reasoner/reasoner.tex (revision 42) @@ -166,4 +166,6 @@ $$ +as the set of all refined compounds along the compound refinement / inheritance hierarchy of $t$ and + $$allRefines^+(t) = \begin{cases} @@ -171,6 +173,10 @@ \emptySet, & \text{else} \end{cases}$$ + +as the set of all refined compounds along the compound refinement / inheritance hierarchy of $t$ including $t$. All inherited slots can then be derived by $$inheritedSlots(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$$ + +In some constraint transformations it is important to determine, whether a variable declaration, i.e., in particular for a compound slot is overridden. Let $d$ be a declaration, in particular $d\in slots(t) \wedge isCompund(t)$, then the parent compound of $d$ is $$parentCompound(d) = @@ -181,7 +187,8 @@ \end{cases}$$ +and we can determine whether $d$ is overridden by + $$isOverridden(d) = d \in \setWith{slots(r)}{r\in allRefines(parentCompound(d))}$$ - Akin to projects, $assignments(t)$ is defined for a compound type $t$ and returns the annotation assignment blocks. Similar functions apply to access the constraints, the variable declarations and the assignment data. @@ -190,11 +197,19 @@ \subsubsection{Containers} -A container is a parameterized structure that holds an arbitrary number of variables / values. IVML ships with two default container types, namely sequence (duplicates allowed, order important) and set (no duplicates allowed, order irrelevant). Let $c$ be a container, then $elements(c)$ denotes is the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$ and $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} $contained(t)$ returns \IVML{setOf(Integer)}. We define $isNested(t) = isContainer(contained(t))$ and +A container is a parameterized structure that holds an arbitrary number of variables / values. IVML ships with two default container types, namely sequence (duplicates allowed, order important) and set (no duplicates allowed, order irrelevant). + +Let $c$ be a container, then $elements(c)$ denotes the set or sequence of all element values in $c$, respectively. Let type $t$ be a container type, then $isContainer(t)$ returns $true$. Further, $contained(t)$ returns the directly contained type, e.g., for a \IVML{setOf(setOf(Integer))} $contained(t)$ returns \linebreak \IVML{setOf(Integer)}. We define $isNested(t) = isContainer(contained(t))$ and $$nested(c)=\begin{cases}nested(contained(t)), & \text{if } isNested(t) \\ contained(t), & \text{else} \\ \end{cases}$$ -returns the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. In some situations, we must identify whether a container contains constraints, i.e., $isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$. More generally, we also define a function that returns the set of all (contained) types used in a container, i.e., $usedTypes(c) = \setWith{contained(type(e))}{e\in elements(c)}$. - -For containers, access expressions usually occur only if the collection has a compound as nested type and if the collection is a sequence. Then accessing an element by an index happens through the IVML index access function for sequences \IVML{seq[1]} and the accessor to \IVML{slot} would then be the combined expression \IVML{seq[1].slot}, for creating an expression $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. +to return the (innermost) nested type, i.e., for \IVML{setOf(setOf(Integer))} $nested(t)$ returns \IVML{Integer}. In some situations, we must identify whether a container consists of constraints, i.e., + +$$isConstraintContainer(t) = isNested(t) \wedge isConstraint(nested(t))$$. + +In other situations, we need to know all types that are used in a container (value), i.e., + +$$usedTypes(c) = \setWith{contained(type(e))}{e\in elements(c)}$$ + +For containers, access expressions usually occur only if the collection has a compound as nested type and if the collection is a sequence. Then accessing an element by an index happens through the IVML index access function for sequences. For example, \IVML{seq[1]} accesses an indexed element of the sequence \IVML{seq} and the accessor to \IVML{slot} on \IVML{seq[1]} is then the combined expression \IVML{seq[1].slot}. For creating the respective expression within an algorithm, we denote $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. \subsubsection{Derived types} @@ -202,5 +217,7 @@ In IVML, a derived type creates a new type based on an existing type. A derived type can restrict the base type by specifiying constraints, as well as a type alias if no further constraints are given. -For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ \TBD{only base or most basic base type?} returns the type $t$ is derived from. For specifying constraints, a base type implicitly declares a variable $decl(d)$ of type $t$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type is relevant. For constraint translation in reasoning, it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define +For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ \TBD{only base or most basic base type?} returns the type $t$ is derived from. + +For specifying constraints, a derived type $t$ implicitly declares a variable $decl(t)$ of type $base(t)$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type is relevant. For constraint translation in reasoning it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define $$allBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge base(t) = \undef \\ \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$$ @@ -208,5 +225,5 @@ \subsection{Miscellaneous} -No specific functions are required for translating constraints for / reasoning on \textit{basic types} (Boolean, Integer, Real String). The available functions for these types, such as adding two integer values, are subject to the creation of the model and, therefore, if specified, already part of constraint expressions before reasoning. +No specific functions are required for translating constraints for / reasoning on \textit{basic types} (Boolean, Integer, Real String). The available functions for these types, such as adding two integer values, are subject to the creation of the IVML model, e.g., through a parser, and are, therefore, if specified, already part of constraint expressions before reasoning. In IVML, a \textit{configuration reference} points to a variable defined in the same or another project (if made available through imports). As the actual IVML specification \cite{IVML-LS} does not define specific properties or operations for reference types, we can safely assume that variables of reference types are transparent and just provide access to the referenced variable. In particular, this holds even if constraints are defined on that variable, as they are translated for / evaluated on the referenced variable.