Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 102) +++ /reasoner/reasoner.tex (revision 103) @@ -195,11 +195,11 @@ Moreover, \IVML{Constraint} is an IVML type, indicating that a variable actually holds a constraint. From the reasoning point of view, a constraint stored as a value in a constraint variable is evaluated as any other constraint. However, the value in such a variable may, as for all other variables, be undefined, frozen, or re-defined (once per project scope) implying that the old constraint must be discarded or even replaced by the new constraint value and considered by the reasoning process. -We define two basic functions for constraints: $isConstraint(t)$ indicates whether type $t$ is a constraint type. $isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} in IVML notation \IVML{x = 25;}. - -As we will discuss in Section \ref{sectTranslation}, various constraints must be instantiated, complemented and rewritten during the constraint translation process, which is executed per project directly before the reasoning step in order to populate the constraint base. For this purpose, we use a specific notation indicating constraint creation combining algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (stated in teletype) used to build up the constraint expression. For example, for creating the IVML constraint \IVML{x = 25;}, we denote in algorithms $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the expression representing the constraint. Here, \IVML{assng} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}), which returns a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may denote $\createConstraint{\IVML{assign}(x, 25)}$, whereby $x$ is determined by the algorithm and used to generically describe a constraint instantiation. As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. Let $c$ be an IVML collection of Integers, then \IVML{c->forall(i|i>20);} requires that all values in $c$ are greater than 20. To create such a constraint with $c$ being an algorithm variable, we denote $\createConstraint{c\IVML{->forall(i|i>20)}}$. - -As part of the constraint instantiation, variables must be replaced. Let $c=\createConstraint{\IVML{assign(x, 25)}}$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{x}, i.e., for the example effectively to \IVML{y = 25}. If such substitutions are stored in a mapping, i.e., a $\variableMapping=\set{\mapEntry{e_s, e_t}}$ with $e_s$ being the expression to be replaced and $e_t$ the replacing expression, we can apply this mapping to a constraint $c$ using $\varSubstitutionVarMapping{c}$. Moreover, we can combine a specific mapping and already stored mappings using $\varSubstitutionOtherVarMapping{c}{x = y}$. Please note that such substitutions are transitive, i.e., if $\mapEntry{y}{z}\in \variableMapping$, $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. - -For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, i.e., for creating a default constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$. As we use the '$|$' symbol for variable substitutions, we denote IVML quantors by ':', e.g., \IVML{forall(x:c(x))} instead of the correct IVML notation \IVML{forall(x|c(x))} denoting $c(x)$ as a constraint using variable $x$. +We define two basic functions for constraints: $isConstraint(t)$ indicates whether type $t$ is a constraint type. $isAssignmentConstraint(c)$ indicates whether constraint $c$ is supposed to change the value of a variable through an assignment, e.g., for an integer variable \IVML{x} in IVML notation \IVML{x = 25;} + +As we will discuss in Section \ref{sectTranslation}, various constraints must be instantiated, complemented and rewritten during the constraint translation process, which is executed per project directly before the reasoning step in order to populate the constraint base. For this purpose, we use a specific notation indicating constraint creation combining algorithm elements carrying actual values/elements (written in mathematical notation) and IVML expression operation (stated in teletype) used to build up the constraint expression. For example, for creating the IVML constraint \IVML{x = 25;}, we denote in algorithms $\createConstraint{\IVML{assign(x, 25)}}$. The angle brackets indicate a constraint creation, the contents of the brackets the expression representing the constraint. Here, \IVML{assng} is the assign operation defined by IVML (actually implementing the equals in \IVML{x = 25;}), which returns a Boolean value indicating whether the execution of the operation succeeded. In an algorithm, we may denote $\createConstraint{\IVML{assign}(x, 25)}$, whereby $x$ is determined by the algorithm and used to generically describe a constraint instantiation. Moreover, to indicate some generic use of constraints, e.g., in transformation patterns, we denote a constraint $c$ using a certain variable $v$ by $c(v)$. + +As part of the constraint instantiation, variables must be replaced. Let $c=\createConstraint{\IVML{assign(x, 25)}}$ be a constraint and \IVML{y} be some IVML variable. Then $\varSubstitution{c}{x = y}$ leads to the substitution of all variables named \IVML{x} by \IVML{x}, i.e., for the example effectively to \IVML{y = 25}. If such substitutions are stored in a mapping, i.e., a $\variableMapping=\set{\mapEntry{e_s, e_t}}$ with $e_s$ being the expression to be replaced and $e_t$ the replacing expression, we can apply this mapping to a constraint $c$ using $\varSubstitutionVarMapping{c}$. Moreover, we can combine a specific mapping and already stored mappings using $\varSubstitutionOtherVarMapping{c}{x = y}$. Please note that such substitutions are transitive, i.e., if $\mapEntry{y}{z}\in \variableMapping$, $x$ will be replaced by $z$. If the right side of a substitution is $\undef$, no substitution happens, e.g., in $\varSubstitution{c}{x = \undef}$. As usual in IVML, we denote the creation of collection operations using the arrow and iterator notation. As we use the '$|$' symbol for variable substitutions, using the same symbol in some transformations in IVML quantor expressions would be confusing. Thus, we use in this document the respective syntax parts ':' as introduced for sets in Section \ref{sectGeneralNotation} instead of the syntactically correct '$|$', e.g., \IVML{forall(x:c(x))} instead of the correct IVML notation \IVML{forall(x|c(x))}. Let $c$ be an IVML collection of Integers, then \IVML{c->forall(i:i>20);} requires that all values in $c$ are greater than 20. To create such a constraint with $c$ being an algorithm variable, we denote $\createConstraint{c\IVML{->forall(i:i>20)}}$. + +For some purpose, the reasoning mechanism must classify constraints, in particular default value assignments over usual constraints. We indicate this information as a `$d$' in the constraint creation notation, i.e., for creating a default constraint, we denote $\createDefaultConstraint{\IVML{assign}(x, 25)}$. In some cases, expressions used to build up a constraint are created before the actual constraint and stored in structures for lookup. We denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for calculating the sum of $x$ and 25. A specific type of expression is the constant, which holds an IVML value. The operation $const(e)$ returns the value of $e$ if $e$ is a constant expression or $\undef$ otherwise. When creating expressions, sometimes a temporary (local) variable is needed, e.g., for an IVML let-expression or a container iterator. We state this by $\IVMLMeta{var}(t)$, i.e., create the temporary variable of type $t$ (we don't care for the name of the variable here). For a variable $v=\IVMLMeta{var}(t)$ holds $isLocal(v) = true$. @@ -653,5 +653,5 @@ } -The first pattern indicates that an IVML compound type $C$ with declared slot $s$ and contained constraint $c(s)$ over slot $s$. The translation is applied if a variable $v$ of type $T$, i.e., a concrete instance of a compound type is declared and, however, receives a value. In this case, each contained constraint is instantiated by qualifying all relevant variable occurrences, i.e., replacing \IVML{self} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings, in particular including qualified access expression known for other slots in $C$. The second case indicates a top-level constraint defined over the compound variable $v$. In contrast, this translation can happen as part of translating all top-level constraints, as due to the use of only qualified slot access expressions, just the (top-level) variable mapping is relevant for the substitution. The patterns show, that in both cases, the respective variable mapping including top-level and type-level cross-reference accesses must be created before the respective translation. However, compounds may contain assignment and eval blocks. Assignment blocks are discussed in Section \ref{sectAnnotationDefaults}, but mainly differ in the treatment of the default value assignments rather than the contained constraints. Constraints in eval blocks can be transformed as shown by the patterns, but require differnt constraint evaluation priority. Moreover, compound instances may occur in containers, which we will discuss in more detail in Section \ref{sectContainerDefaults}. We will now focus on the first pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}. +The first pattern indicates that an IVML compound type $C$ with declared slot $s$ and contained constraint $c(s)$ over slot $s$. The translation is applied if a variable $v$ of type $T$, i.e., a concrete instance of a compound type is declared and, however, receives a value. In this case, each contained constraint is instantiated by qualifying all relevant variable occurrences, i.e., replacing \IVML{self} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings, in particular including qualified access expression known for other slots in $C$. More complex access expressions also allow for translating nested compounds. The second case indicates a top-level constraint defined over the compound variable $v$. In contrast, this translation can happen as part of translating all top-level constraints, as due to the use of only qualified slot access expressions, just the (top-level) variable mapping is relevant for the substitution. The patterns show, that in both cases, the respective variable mapping including top-level and type-level cross-reference accesses must be created before the respective translation (including annotations, to handle constraints on annotations similarly). However, compounds may contain assignment and eval blocks. Assignment blocks are discussed in Section \ref{sectAnnotationDefaults}, but mainly differ in the treatment of the default value assignments rather than the contained constraints. Constraints in eval blocks can be transformed as shown by the patterns, but require different constraint evaluation priority. Moreover, compound instances may occur in containers, which we will discuss in more detail in Section \ref{sectContainerDefaults}. We will now focus on the first pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}. For slots and annotations we can resort to Algorithm \ref{algTranslateDeclaration}, i.e., compound types, derived types, constraint variables and collections, while for the remaining constraints, we must visit these structures, instantiate and collect the respective constraints. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. In particular, if the IVML keyword \IVMLself{} is used within a constraint, it must be substituted by the actual variable of the respective compound type. Moreover, it is important to recall that a variable $v$ of type $type(v)$ can contain instances of any refined type $allRefines^+(t)$, and in this case the translation must consider the default values of the potentially larger slot, additional constraints and nested structures. @@ -733,13 +733,18 @@ \subsection{Container types}\label{sectContainerDefaults} +Per se, a container variable can only declare the contained type and the respective element values through its default, i.e., there is no direct opportunity to define constraints for a container. However, constraints are indirectly defined through the contained type and the types used for the individual elements. Here, compounds, derived types, constraint types and, transitively, nested containers can introduce constraints further characterizing (the contents of) a container variable. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. Due to refinement, all relevant types may be more specific than the (generic) container type given for the initial container variable. + +Containers differ from the other IVML types as a container may contain an arbitrary number of elements. Thus, for specifying a constraint over a container, we must apply all-quantification or, as an alternative, unroll the container, create constraints for the individual container entries and take care of the changes of the elements. Currently, unrolling is not possible for all IVML container types, e.g., set-based types do not offer index-based access. Thus, for the translation pattern, we generically use quantification. + \grayPara{ \begin{gather*} - \patternDerivation{\IVML{setOf(}T\IVML{) } v\IVML{;}}{\bigcup_{t_\in used(v), c\in constraints(t)}\IVML{typeSelect}(\IVML{flatten}(v), t)\rightarrow \IVML{forall}(w:\varSubstitution{c}{\ldots, \variableMapping})}\\ - \patternDerivation{\IVML{setOf(}T\IVML{) } v\IVML{;} c(v)\IVML{;}}{\varSubstitution{c(v)}{\variableMapping}} + \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}}{\bigcup_{t\in usedTypes(v), c\in constraints(t)}f(v, t)\rightarrow \IVML{forall}(w:\varSubstitution{c(x)}{x=w.x, \variableMapping})}\\ + \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;} c(v)\IVML{;}}{\varSubstitution{c(v)}{\variableMapping}} \end{gather*} } - -Per se, a container variable can only declare the contained type and the respective element values through its default, i.e., there is no direct opportunity to define constraints for a container. However, constraints are indirectly defined through the contained type and the types used for the individual elements. Here, compounds, derived types, constraint types and, transitively, nested containers can introduce constraints further characterizing (the contents of) a container variable. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. Due to refinement, all relevant types may be more specific than the (generic) container type given for the initial container variable. +There are two basic translation patterns for containers, 1) constraints induced by used types and 2) top-level constraints for collection variables. We will focus here on the first pattern, as the second pattern comes for free as part of the translation of the top-level constraints. + +As shown for the first pattern, given a container variable $v$, we consider all potential (declared) as well as used types in the actual value and create for each constraint implied by these types an all-quantified constraint over $v$. Please note that individual constraints are needed to provide detailed error messages, but also to keep the re-evaluation effort low. However, if the container is nested, i.e., $T$ is again a container over a certain type, we must take flattening into account to apply the constraints to the individual elements. Moreover, if $\subTypeOf{t}{T)}$, accessing specific properties such as compound slots requires some form of type casting / selection on the elements of the container. These additional container transformations depend on the actual container type and are represented in the schema by $f(v, t)$, which we will detail below in this section. Finally, the constraint must be substituted adequately, using the quantifier iterator to access the elements, including slot access expressions for compound element types as well as known access expressions to other variables and slots. \begin{algorithm}[H] @@ -776,10 +781,8 @@ \end{algorithm} -However, containers are different than usual variables as the may contain an arbitrary number of elements. Thus, for specifying a constraint over a container, we must apply all-quantification (the IVML \IVML{forAll} operation) for all constraints defined on contained types. Moreover, for nested collections we must apply the IMVL \IVML{flatten} operation to gain access to the individual elements, and for refined types even explicit IVML type casts using the \IVML{selectByKind} operation to have access to specific operations, slots or annotations. - -Below we illustrate the translation schema: $d$ denotes the variable declaration containing the compound (may alternatively be a compound or container accessor). \IVML{flatten} provides access even to deeply nested container entries. \IVML{selectByKind} if we translate for slots of a specific given type $t$ with $\subTypeEqOf{t}{s}$. Finally, we apply an all quantor over the elements of the collection using the temporary iterator variable $l$ to the respective constraint $c$ after appropriate variable substitution, in particular replacing \IVMLself{} by $l$. +We detail now the generic translation schema, i.e., the function $f(v, t)$ mentioned above by using the IMVL \IVML{flatten} and the \IVML{selctByKind} operations: Let $d$ denote the variable declaration containing the compound (may alternatively be a compound or container accessor). The \IVML{flatten} resolves all nested containers and implicitly provides access even to deeply nested container entries. \IVML{selectByKind} is needed if we translate for slots of a specific given type $t$ with $\subTypeEqOf{t}{s}$, as otherwise the slots defined on specific types are not accessible. Finally, we apply an all quantor over the elements of the collection using the temporary iterator variable $l$ to the respective constraint $c$ after appropriate variable substitution, in particular replacing \IVMLself{} by $l$. % \begin{displaymath} -d\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if nested}}\underbrace{\IVML{selectByKind}(t)\rightarrow}_{\text{if } \subTypeOf{t}{nested(c)}}\IVML{forAll}(l:c) +d\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if nested}}\underbrace{\IVML{selectByKind}(t)\rightarrow}_{\text{if } \subTypeOf{t}{nested(c)}}\IVML{forAll}(l:c(l)) \end{displaymath} % @@ -825,10 +828,10 @@ % \begin{displaymath} -\underbrace{\underbrace{ca}_{1: ca}\rightarrow \IVML{flatten}}_{1:e}\rightarrow\IVML{forAll}(\underbrace{l}_{1:l}:\underbrace{\underbrace{l.s}_{2: ca}\rightarrow\IVML{flatten}}_{2:e}\rightarrow\IVML{forAll}(\underbrace{l_2}_{2:l}:c)) +\underbrace{\underbrace{ca}_{1: ca}\rightarrow \IVML{flatten}}_{1:e}\rightarrow\IVML{forAll}(\underbrace{l}_{1:l}:\underbrace{\underbrace{l.s}_{2: ca}\rightarrow\IVML{flatten}}_{2:e}\rightarrow\IVML{forAll}(\underbrace{l_2}_{2:l}:c(l_2))) \end{displaymath} % -In the first iteration, we start with $ca$ (indicated by $1:ca$, may also be some $d$) and append flatten/typeSelect as needed to form $e$ (indicated by $1:e$, i.e., recursion level and parameter/variable name). In the first iteration, we also create a temporary variable $l$ as iterator variable. We store $l$ and $e$ on the stack of $\variableMapping$ and pass $l$ on as accessor to the translation of compound content in Algorithm \ref{algTranslateCompoundContent}. There, we create an accessor for a slot, let's say $s$, i.e. $l.s$, which is then passed on in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} or \ref{algTranslateCompoundDeclarationTranslateSlotsT}, respectively, to the translation of declarations in Algorithm \ref{algTranslateDeclaration}. As a further compound container is nested into the initial compound container, we end up again in Algorithm \ref{algTranslateCompoundContainer}. Now $l.s$ is considered as accessor (indicated by $2:ca$), flatten(typeSelect are added as needed to form $e$ (now $2:e$), which is stored along with the temporary iterator variable $l_2$ on the stack. In this context, we apply the constraint $c$ within an all-quantor (after appropriate variable substitution, in particular \IVMLself{} by $l_2$). The quantor expressions for completing the full constraint are created by the $add$ algorithm (details in Section \ref{algAddConstraints}). - -Let us assume that $stack(\variableMapping)$ returns the contex frames of the stack starting with the top frame, $container(s)$ returns the container expression assigned to context frame $s$ and $iterator(s)$ the iterator variable for $s$. The, Algorithm \ref{algComposeExpression} creates a constraint of the form shown above inside out, starting with $c$ after correct variable substition. For each stack element that has a container (we assume also an iterator variable) assigned, which is not the case for context frames created for compounds, we surround the actual $c$ by an all-quantor, running over $container(s)$ using $iterator(s)$ as iterator variable and $c$ as quantor expression. +In the first iteration, we start with $ca$ (indicated by $1:ca$, may also be some $d$) and append flatten/typeSelect as needed to form $e$ (indicated by $1:e$, i.e., recursion level and parameter/variable name). In the first iteration, we also create a temporary variable $l$ as iterator variable. We store $l$ and $e$ on the stack of $\variableMapping$ and pass $l$ on as accessor to the translation of compound content in Algorithm \ref{algTranslateCompoundContent}. There, we create an accessor for a slot, let's say $s$, i.e. $l.s$, which is then passed on in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} or \ref{algTranslateCompoundDeclarationTranslateSlotsT}, respectively, to the translation of declarations in Algorithm \ref{algTranslateDeclaration}. As a further compound container is nested into the initial compound container, we end up again in Algorithm \ref{algTranslateCompoundContainer}. Now $l.s$ is considered as accessor (indicated by $2:ca$), flatten(typeSelect are added as needed to form $e$ (now $2:e$), which is stored along with the temporary iterator variable $l_2$ on the stack. In this context, we apply the constraint $c$ within an all-quantor (after appropriate variable substitution, in particular \IVMLself{} by $l_2$). The quantor expressions for completing the full constraint are created by the $add$ algorithm (details in Section \ref{sectContainerBase}). + +Let us assume that $stack(\variableMapping)$ returns the contex frames of the stack starting with the top frame, $container(s)$ returns the container expression assigned to context frame $s$ and $iterator(s)$ the iterator variable for $s$. The, Algorithm \ref{algComposeExpression} creates a constraint of the form shown above inside out, starting with $c$ after correct variable substation. For each stack element that has a container (we assume also an iterator variable) assigned, which is not the case for context frames created for compounds, we surround the actual $c$ by an all-quantor, running over $container(s)$ using $iterator(s)$ as iterator variable and $c$ as quantor expression. \begin{algorithm}[H] @@ -852,11 +855,14 @@ \subsection{Annotations}\label{sectAnnotationDefaults} -In IVML, annotations are orthogonal typed variables that can be attached to a variable. For all those ortogonal variables, the reasoner must create constraints to perform the evaluation and assignment of the default values before all other constraints are considered for reasoning. It is important to recall that IVML annotations are not recursive~\cite{IVML-LS}, although the reasoner algorithms could support this. Moreover, we must translate assignment-blocks, i.e., blocks assigning specific values to all variables declared within that block. In this section, we discuss first the translation of annotations, then the translation of annotation blocks. - -Algorithm \ref{algTranslateAnnotationDeclarations} receives the declaration of the actual variable and a potential compound access expression $ca$ to $d$ if the algorithm is called for slots of a compound value. The actual access expression is either $ca$ if given or $d$ if $ca$ is not given (line \ref{algTranslateAnnotationDeclarationsCa}). Annotations are translated based on $v$ if given (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}), for configuration initialization also based on $d$ if $v$ is not given (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). - -For all annotations of $v$ -%(as for $v$ here all inherited annotations are available) -, the algorithm creates the respective constraints by creating a specific access expression (only if we are not actually translating top-level annotation blocks implying context registering) through calling Algorithm \ref{algTranslateDeclaration}. For top-level annotation assignments , no specific access expressions except for the one created in line \ref{algTranslateAnnotationDeclarationsCa} are needed, as they are created in Algorithm \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateAnnotationAccess}. +In IVML, annotations are orthogonal typed variables that can be attached to a variable. For all those orthogonal variables, the reasoner must create constraints to perform the evaluation and assignment of the default values before all other constraints are considered for reasoning. It is important to recall that IVML annotations are not recursive~\cite{IVML-LS}, although the reasoner algorithms could support this. Moreover, we must translate assignment-blocks, i.e., blocks assigning specific values to all variables declared within that block. In this section, we discuss first the translation of annotations, then the translation of annotation blocks. + +The first transformation pattern for the direct translation of annotations is the second pattern from Section \ref{sectTranslationDeclarationTypesDefaults}. More specifically, Algorithm \ref{algTranslateDeclaration} from \ref{sectTranslationDeclarationTypesDefaults} calls the algorithms in this section, which in turn call Algorithm \ref{algTranslateDeclaration}, i.e., the algorithms here prepare the application of Algorithm \ref{algTranslateDeclaration} by composing specific accessor expressions. The second pattern relates to annotation blocks, i.e., specific assignment constraints (accessor expression $ca$ is determined by the top-level or compound context of the annotation block) is created for the variables declared in the assignment block for values mentioned in the assignment data (clause). It is important to note that annotation blocks may be nested in order to indicate orthogonal annotations, i.e., the constraint translation mist take this nesting and the respective precedence of the assignment data due to their nesting into account. + +\grayPara{ +\begin{gather*} + \patternDerivation{\IVML{annotate } a = deflt \IVML{ to } *\IVML{;} T \text{ } v\IVML{;}}{ca.v.a = deflt}\\ + \patternDerivation{\IVML{assign (} a = deflt \IVML{) to \{} T v \IVML{ assign} \ldots \IVML{\}}}{ca.v.a = deflt \ldots} +\end{gather*} +} \begin{algorithm}[H] @@ -883,7 +889,13 @@ \end{algorithm} +Algorithm \ref{algTranslateAnnotationDeclarations} receives the declaration of the actual variable and a potential compound access expression $ca$ to $d$ if the algorithm is called for slots of a compound value. The actual access expression is either $ca$ if given or $d$ if $ca$ is not given (line \ref{algTranslateAnnotationDeclarationsCa}). Annotations are translated based on $v$ if given (lines \ref{algTranslateAnnotationDeclarationsTranslateVStart}-\ref{algTranslateAnnotationDeclarationsTranslateVEnd}), for configuration initialization also based on $d$ if $v$ is not given (lines \ref{algTranslateAnnotationDeclarationsTranslateDStart}-\ref{algTranslateAnnotationDeclarationsTranslateDEnd}). + +For all annotations of $v$ +%(as for $v$ here all inherited annotations are available) +, the algorithm creates the respective constraints by creating a specific access expression (only if we are not actually translating top-level annotation blocks implying context registering) through calling Algorithm \ref{algTranslateDeclaration}. For top-level annotation assignments , no specific access expressions except for the one created in line \ref{algTranslateAnnotationDeclarationsCa} are needed, as they are created in Algorithm \ref{algTranslateDeclaration} line \ref{algTranslateDeclarationTranslateAnnotationAccess}. + We turn now to the translation of annotation assignment-blocks. In IVML, an assignment-block is used on top-level or within compounds to declare compound slots with an implicit assignment of a value to each declared annotation. Further, assignment-blocks can be nested and the assignments defined for the outer blocks must be applied also to the inner blocks. -The translation of assignment-blocks on top-level is triggered by Algorithm \ref{algTranslateConstraints} in line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. The translation of assignment-blocks within compounds is caused by Algorithm \ref{algTranslateCompoundDeclaration} in line \ref{algTranslateCompoundDeclarationCompoundAssignments} (variable mapping in lines \ref{algTranslateCompoundDeclarationVarMappingStart}-\ref{algTranslateCompoundDeclarationVarMappingEnd} and slot translation in line \ref{algTranslateCompoundDeclarationTranslateSlots} along with the decision variables of the compound value). In both cases, Algorithm \ref{algTranslateAnnotationAssignments} is called. +The translation of assignment-blocks on top-level is triggered by Algorithm \ref{algTranslateConstraints} in line \ref{algTranslateConstraintsTopLevelAnnotationAssignments}. The translation of assignment-blocks within compounds is caused by Algorithm \ref{algTranslateCompoundDeclaration} in line \ref{algTranslateCompoundDeclarationCompoundAssignments} (variable mapping in Algorithm \ref{algRegisterCompoundMapping} line \ref{algRegisterCompoundMappingVarMapping} and slot translation in line \ref{algTranslateCompoundDeclarationTranslateSlotsV} or \ref{algTranslateCompoundDeclarationTranslateSlotsT} in Algorithm \ref{algTranslateCompoundDeclaration} along with the decision variables of the compound value). In both cases, Algorithm \ref{algTranslateAnnotationAssignments} is called. Algorithm \ref{algTranslateAnnotationAssignments} first builds up (incrementally) the set of effective assignments data $ea$ that is relevant for the actual assignment-block $a$ (initially $ea=\emptySet$ for a top-level assignment-block). @@ -934,4 +946,11 @@ Constraint variables can be created by taking the respective default/actual variable, performing the variable substitution with $\variableMapping$ and, if available, a respective value for \IVMLself, turning the resulting expression into a constraint and adding it to the set of other constraints $\otherConstraints$. Moreover, the relationship between the underlying variable $v$ and the constraint must be recorded for efficient update of the constraint base upon value change (cf. Algorithm \ref{algVarChange}). Recording happens only if $v$ is defined, which may not be the case if this algorithm is called while processing container values. + +\grayPara{ +\begin{gather*} + \patternDerivation{v}{v} +\end{gather*} +} + \begin{algorithm}[H]