Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 101) +++ /reasoner/reasoner.tex (revision 102) @@ -52,4 +52,5 @@ \newcommand\tabAlgFollow[0]{ $\rightarrow$ } \newcommand\grayPara[1]{\noindent\adjustbox{bgcolor=gray!20,minipage=[t]{\linewidth}}{#1}\linebreak} +\newcommand\patternDerivation[2]{#1 \leadsto #2} \let\emph\relax % there's no \RedeclareTextFontCommand @@ -196,9 +197,9 @@ 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{assing} 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 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)}$ +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$. 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$. @@ -411,5 +412,5 @@ \begin{itemize} - \item $setRegisterContexts(\variableMapping, bool)$ enabling automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag. + \item $setRegisterContexts(\variableMapping, b)$ enables automatic registration of context frames within the parent frame. The operation returns the previous state of the registration flag. \item $isContextsRegistering(\variableMapping)$ returns whether context registering is currently active. \item $pushContext(\variableMapping, d, r)$ creates and pushes a new context frame for declaration $d$ to the stack. If registration of contexts is enabled, the new frame will be registered with the parent frame for $var$ (unless $var=\undef$) Further, $r$ indicates whether already processed types shall be recorded by this context, which is important for handling recursive types. @@ -422,4 +423,5 @@ \item $activate(\variableMapping, d)$ re-activates, i.e., pushes the registered stack frame for $d$ from the current context frame. As long as the current context frame exists, this operation can be called over and over. If no context frame is registered for $d$, the stack is not modified. \item $deactivate(\variableMapping, d)$ de-activates the registered context frame for $d$, i.e., pops it from the stack but leaves it registered with its parent context frame so that it is available for further activations as long as the parent context frame exists. + \item $size(\variableMapping)$ the number of contexts on the stack. There is at least always one context on the stack representing the containing project. \item $clear(\variableMapping)$ clears the stack and cleans up the default context frame dedicated to the IVML project so that $\variableMapping$ is ready for the translation of the next IVML project. \end{itemize} @@ -556,15 +558,16 @@ Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and respective variable $v$ through their actual type. Basically, the algorithm considers for the given variable, depending on the actual type, derived type constraints, annotation defaults, compound constraints, container constraints, and constraints of overridden slots leading to a deferred default initialization through the global constraints set $\deferredDefaultConstraints$. -At its core, Algorithm \ref{algTranslateDeclaration} instantiates a given variable $v$ (or attribute) with default value $deflt$, basically $default(v)$, by adding a qualifying access prefix expression $ca$ and turning it into a default value assignment constraint. +At its core, Algorithm \ref{algTranslateDeclaration} instantiates a given variable $v$ (or attribute in the second case) with default expression $deflt$, basically $default(v)$ turning it into a default value assignment constraint. The patterns below include a right side access prefix ($ca.$), which may be empty for top-level variables. \grayPara{ -$$ - v \leadsto ca.v = deflt -$$ +\begin{gather*} + \patternDerivation{T \text{ } v = deflt\IVML{;}}{ca.v = deflt} \\ + \patternDerivation{\IVML{annotate } a = deflt \IVML{ to } *\IVML{;} T \text{ } v\IVML{;}}{ca.v.a = deflt} +\end{gather*} } -As this works in a straight forward manner only for basic IVML types, but a given variable $v$ may also be of compound or container type, Algorithm \ref{algTranslateDeclaration} dispatches further on to the other algorithms constituting the reasoner as discssed in the following sections. - -In more detail, Algorithm \ref{algTranslateDeclaration} first declares some local variables in line \ref{algTranslateDeclarationDecl}, including the actual type $t$ (to be overridden by the type of the default value expression if needed), the default value expression $dflt$, the actual set of default constraints ($\defaultConstraints$ or $\deferredDefaultConstraints$) to be utilized for adding the final constraint and the actual value of self $s$ (for compound types only). Then, if $t$ is a derived data type, constraints are translated and collected through Algorithm \ref{algTranslateDerivedDatatypeConstraints}. In non-incremental mode, i.e., we translate default value expressions to assignment constraints as well as the default constraints for annotations can then be translated using \ref{algTranslateAnnotationDeclarations}. Due to potential type interferences with derived types, we determine then the actual type through the type of the default value expression if defined. If $t$ is a compound type, we set the value of self $v$ to the actual variable declaration $d$ and execute the specific translations for compound types using Algorithm \ref{algTranslateCompoundDeclaration}. If $t$ is a container type, we call \ref{algTranslateContainerDeclaration} instead. Otherwise, if there is a default value expression and reasoning is not in incremental mode, i.e., we shall translate default value expressions to assignment constraints, and if there is a compound accessor, we just have to schedule a replacement of \IVML{self} by the compound accessor. Remaining default constraints are taken over as defined as long as the reasoner is not operating incremental mode as there no default value assignments are needed. +For a $v$ of compound or container type, Algorithm \ref{algTranslateDeclaration} dispatches to the other algorithms constituting the reasoner as we will discus in the following sections. Then the patterns can also be applied for initializing compound slots. As a consequence, Algorithm \ref{algTranslateDeclaration} may be called recursively with an incrementally constructed access expression $ca$ that is prefixed before the right side, e.g., let $c$ be the top-level variable of compound type, then $ca=c$ and the pattern $\patternDerivation{v}{ca.v = deflt}$ becomes $c.v=deflt$. In particular in such recursive calls, occurrences of other variables in $deflt$ recorded in $\variableMapping$, e.g., other slots as well as \IVML{self} denoting the actual compound must be substituted properly, i.e., the result is at least $c.v=\varSubstitution{deflt}{\IVML{self}, \variableMapping}$. + +In more detail, Algorithm \ref{algTranslateDeclaration} first declares some local variables in line \ref{algTranslateDeclarationDecl}, including the actual type $t$ (to be overridden by the type of the default value expression if needed), the default value expression $dflt$, the actual set of default constraints ($\defaultConstraints$ or $\deferredDefaultConstraints$) to be utilized for adding the final constraint and the actual value of self $s$ (for compound types only). Then, if $t$ is a derived data type, constraints are translated and collected through Algorithm \ref{algTranslateDerivedDatatypeConstraints}. In non-incremental mode, i.e., we translate default value expressions to assignment constraints as well as the default constraints for annotations can then be translated using \ref{algTranslateAnnotationDeclarations}. Due to potential type interferences with derived types, we determine then the actual type through the type of the default value expression if defined. %parasplit \begin{algorithm}[H] @@ -604,4 +607,6 @@ \end{algorithm} +If $t$ is a compound type, we set the value of self $v$ to the actual variable declaration $d$ and execute the specific translations for compound types using Algorithm \ref{algTranslateCompoundDeclaration}. If $t$ is a container type, we call \ref{algTranslateContainerDeclaration} instead. Otherwise, if there is a default value expression and reasoning is not in incremental mode, i.e., we shall translate default value expressions to assignment constraints, and if there is a compound accessor, we just have to schedule a replacement of \IVML{self} by the compound accessor. Remaining default constraints are taken over as defined as long as the reasoner is not operating incremental mode as there no default value assignments are needed. + If there is finally a default value expression to be recorded in the constraint base, we have to distinguish whether the actual variable is a constraint variable or an usual variable. In the first case, we apply Algorithm \ref{algCreateConstraintVariableConstraint} (cf. Section \ref{sectConstraintVariables}). In the second case, we turn the default value expression into an assignment expression. However, the accessor creation depends on whether $d$ is an annotation or an usual variable. Then, we substitute \IVML{self} and the actual variable mapping on the complete constraint expression and turn the result into a default constraint. We either either it to $\deferredDefaultConstraints$ if the constraint may override a complete value assignment (\IVML{self} is used referring to another variable in the same compound or $d$ is an overridden slot that may accidentally be overriden by a complex compound value) or in all other cases to the usual default constraints set $\defaultConstraints$. @@ -610,5 +615,13 @@ As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined through its base type $base(t)$. A derived type $t$ is a type restriction of $base(t)$, if $t$ defines restricting constraints over $base(t)$ through the local variable $decl(t)$. Type $t$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(t) = \emptySet$. -If a variable $v$ is declared as of a derived type $t$, all constraints defined for $t$ over $base(t)$ and, transitively all constraints over all base types $allBase(t)$ must hold for $v$. Whether these constraints are fullfilled depends on the actual value of $v$. The constraint translation follows this nested type structure and instantiates all constraints defined along the nesting. +If a variable $v$ is declared as of a derived type $t$, all constraints defined for $t$ over $base(t)$ and, transitively all constraints over all base types $allBase(t)$ must hold for $v$. Whether these constraints are fullfilled depends on the actual value of $v$. The constraint translation follows this nested type structure and instantiates all constraints defined along the nesting as shown in the following translation pattern. + +\grayPara{ +\begin{gather*} + \patternDerivation{\IVML{typedef } t_i \IVML{ with }(c_i); T v\IVML{;}}{\bigcup_{t_i \in allBase(T)} \varSubstitution{c_i}{decl(t_i)=deref(t_i, v), \variableMapping}} +\end{gather*} +} + +The constraint defined for all constraints induced by derived types are turned into constraints applying a substitution, which replaces the declaration variable and any cross-referenced variables in the resulting constraint. It is important to mention that reference types may be used in combination with derived types and then appropriate de-referencing on $v$ must apply (indicated by $deref(v)$, which leads to $v$ if no de-referencing is needed. For a given variable $v$ (in terms of declaration $d$ and specific type $t$), Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraint.} all constraints defined for $dref(allBase(t))$, i.e., for all base types also through references types, as constraints of $d$. Thereby, we must consider whether we perform this instantiation for a container variable. If it is a container variable, we create an all-quantifying constraint over all container values, whereby the iterator variable substitutes $decl(t)$. If it is not a container variable, we substitute $decl(t)$ by the actual variable $d$. It is important to note that this substitution is transitive if $d$ is a compound slot, i.e., if $d$ is also mentioned in $\variableMapping$, the previously collected compound accessor for $d$ (in Algorithm \ref{algTranslateCompoundDeclaration}) is used to substitute $decl(t)$. Moreover, if the type $t$ consists of reference types, we need to de-reference $i$ by the number of reference types (through the internal IVML \IVML{refBy} operation). The respective composite expression for $i$ is created through the function $deref(t, ex)$ shown below. The resulting constraints are stored in the set of top-level constraints $\topLevelConstraints$. % shall not make a difference for nested variables as they are already initialized @@ -621,5 +634,5 @@ $cs \assng \bigcup_{t \in deref(allBase(t))} constraints(t)$\; $add(\topLevelConstraints, \setWith{\createConstraint{ - \closedCases{d\rightarrow\IVML{forAll(i}|\text{ }\varSubstitutionOtherVarMapping{c}{decl(t)=\IVML{deref(t, i)}}\IVML{)}, & \text{if } isC \\ + \closedCases{d\rightarrow\IVML{forAll(i}:\text{ }\varSubstitutionOtherVarMapping{c}{decl(t)=\IVML{deref(t, i)}}\IVML{)}, & \text{if } isC \\ \varSubstitutionOtherVarMapping{c}{decl(t)=d}, &\text{else}} }}{c\in cs}, true)$\; @@ -631,7 +644,19 @@ \subsection{Compound types}\label{sectCompoundDefaults} -A compound can define constraints in several places, namely through types and defaults of its slots and annotations (including constraint variables as well as refined slots and annotations), as constraints listed directly within a compound, within assignment-blocks or within eval-blocks. 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. - -Algorithm \ref{algTranslateCompoundDeclaration} collects and translates the constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). No translation happens if type $t$ was already processed, e.g., in case of recursive compound types. The types are related by $type(d) = type(v) \in allRefines^+(t)$. Algorithm \ref{algTranslateCompoundDeclaration} creates a context frame and pushes it onto the variable mapping stack $\variableMapping$. Used types are registered only if there is no variable $v$ given, e.g., we process constraints according to a potentially recursive type structure. In contrast, if a variable $v$ is given, the nested variables are initialized correctly, in particular recursively nested variables terminate correctly based on configured values, i.e., we do not have to take care of recursion in this case. +A compound can define constraints in two differnt places, 1) nested within compound type definitions using qualified slot access expressions or unqualified slot names, and 2) as top-level as constraints with qualified slot access expressions. Both types of constraints imply all-quantification over all instances of the respective compound types \cite{IVML-LS}. We translate compound constraints using the following schema: + +\grayPara{ +\begin{gather*} + \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; } c(s)\IVML{\}; } C v \IVML{;}}{\varSubstitution{c(s)}{\IVML{self}=v, s=v.s,\variableMapping}}\\ + \patternDerivation{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C v \IVML{; } c(v)\IVML{; }}{\varSubstitution{c(v)}{\variableMapping}}\\ +\end{gather*} +} + +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}. + +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. + + +Algorithm \ref{algTranslateCompoundDeclaration} collects and translates the constraints for a compound variable $v$ with declaration $d$, potential compound accessor $ca$ and (default value) type (or $type(d)$ if no default expression is defined for $d$). No translation happens if type $t$ was already processed, e.g., in case of recursive compound types. The types are related by $type(d) = type(v) \in allRefines^+(t)$. Algorithm \ref{algTranslateCompoundDeclaration} creates a context frame and pushes it onto the variable mapping stack $\variableMapping$. Used types are registered only if there is no variable $v$ given, e.g., we process constraints according to a potentially recursive type structure. If a variable $v$ is given, the nested variables are initialized correctly, in particular recursively nested variables terminate correctly based on configured values, i.e., we do not have to take care of recursion in this case. The main two steps are detailed in Algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent} as both Algorithms are reused with different arguments during the translation of compounds in Section \ref{sectCompoundDefaults}. Algorithms \ref{algRegisterCompoundMapping} registers all compound slots and annotations in the variable mapping, using $ca$ or $d$ as basis for access expressions for slots and annotations and casts to the type of the actual value in $v$ if available (else $\undef$ is passed in as argument). Now Algorithm \ref{algTranslateCompoundContent} can translate the entire compound content including slots, annotations, constraints, annotation-blocks and eval-blocks. Finally, Algorithm \ref{algTranslateCompoundDeclaration} pops the context frame for this compound from $\variableMapping$. @@ -707,4 +732,12 @@ \subsection{Container types}\label{sectContainerDefaults} + +\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}} +\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. @@ -748,5 +781,5 @@ % \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) \end{displaymath} % @@ -792,5 +825,5 @@ % \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)) \end{displaymath} % @@ -807,5 +840,5 @@ \ForAll{$s \iterAssng stack(\variableMapping)$} { \If{$container(s) \neq \undef$} { - $c \assng \createExpression{container(s)\rightarrow\IVML{forAll}(iterator(s)|c)}$\; + $c \assng \createExpression{container(s)\rightarrow\IVML{forAll}(iterator(s):c)}$\; } } @@ -825,5 +858,5 @@ 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 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}. +, 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}. \begin{algorithm}[H] @@ -835,10 +868,10 @@ \uIf{$v \neq \undef$}{\label{algTranslateAnnotationDeclarationsTranslateVStart} \ForEach{$a\in annotations(v)$}{ - $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } ca \neq \undef \wedge \neg isContextRegistering(\variableMapping)\\ ca, &\text{else}}$\; + $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } ca \neq \undef \wedge \neg isContextRegistering(\variableMapping) \wedge size(\variableMapping) > 1\\ ca, &\text{else}}$\; $translateDeclaration(decl(a), a, ac)$\;\label{algTranslateAnnotationDeclarationsTranslateDeclV} } }\Else{\label{algTranslateAnnotationDeclarationsTranslateVEnd}\label{algTranslateAnnotationDeclarationsTranslateDStart} \ForEach{$a\in annotations(d)$}{ - $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } ca \neq \undef \wedge \neg isContextRegistering(\variableMapping)\\ ca, &\text{else}}$\; + $ac\assng \closedCases{\IVMLMeta{acc}(ca,a), & \text{if } ca \neq \undef \wedge \neg isContextRegistering(\variableMapping) \wedge size(\variableMapping) > 1\\ ca, &\text{else}}$\; $translateDeclaration(a, \undef, ac)$\;\label{algTranslateAnnotationDeclarationsTranslateDeclD} }