Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 201) +++ /reasoner/consTranslation.tex (revision 202) @@ -119,8 +119,8 @@ \grayPara{ \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundDefault} - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; } c(s)\IVML{\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} - \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} - \patternDerivation{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C\ v \IVML{; } c(v.s)\IVML{;}}{\varSubstitution{c(v.s)}{\variableMapping}} + \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; } \constraintWith{c}{s}\IVML{\}; } C\ v \IVML{;}}{\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} + \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} + \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} \constraintWith{c}{s}\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{s}}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}} + \patternDerivation{\IVML{compound } C \IVML{\{} T s \IVML{\}; } C\ v \IVML{; } \constraintWith{c}{v.s}\IVML{;}}{\varSubstitution{\constraintWith{c}{v.s}}{\variableMapping}} } @@ -129,7 +129,7 @@ \begin{itemize} - \item \emph{Compound slot with default value expression:} The default value is instantiated into a default value assignment constraint as shown in Pattern \ref{forCompoundDefault}. For a top-level compound variable $v$, the actual value for \IVMLself{} is determined by $access(v)$ and the accessor for slot $s$ by $access(v.s)$. For nested slots of compound types, Algorithm \ref{algTranslateDeclaration} is called recursively with the respective access expression. - - \item \emph{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 $C$, i.e., a concrete instance of a compound type is declared. A contained constraint is instantiated by qualifying all compound-scoped variable occurrences, i.e., by replacing \IVMLself{} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings including remaining slots. Thus, the variable mapping for a compound must be created before any slot is translated. Nested compounds are implicitly considered through the $access$ function, i.e., by respective access prefix expressions. Moreover, compound instances and, thus, constraints induced by compound types, may occur in containers. In Section \ref{sectContainerDefaults}, we will discuss the translations of containers, which recursively utilizes the translation of variables, i.e., Algorithm \ref{algTranslateDeclaration} and, thus, of compound types. + \item \emph{Compound slot with default value expression:} The default value is instantiated into a default value assignment constraint as shown in Pattern \ref{forCompoundDefault}. When translating a top-level compound variable $v$, the actual value for \IVMLself{} is determined by $access(v)$ and the accessor for slot $s$ by $access(v.s)$. For nested slots of compound types, Algorithm \ref{algTranslateDeclaration} is called recursively with the respective access expression. + + \item \emph{Constraint $c(s)$ defined on compound slot $s$:} For a compound variable $v$ of type $C$, contained constraints are instantiated by qualifying all compound-scoped variable occurrences, i.e., by replacing \IVMLself{} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings including remaining slots. Thus, the variable mapping for a compound must be created before any slot is translated. Nested compounds are implicitly considered through the $access$ function, i.e., by respective access prefix expressions. Moreover, compound instances and, thus, constraints induced by compound types, may occur in containers. In Section \ref{sectContainerDefaults}, we will discuss the translations of containers, which recursively utilizes the translation of variables, i.e., Algorithm \ref{algTranslateDeclaration} and, thus, of compound types. \item \emph{Eval blocks:} Here nesting becomes transparent and constraints are translated as if they were defined directly in the containing compound type, i.e., according to the second pattern. However, eval blocks require a higher constraint evaluation priority in the compound scope as we will detail below. Index: /reasoner/notation.tex =================================================================== --- /reasoner/notation.tex (revision 201) +++ /reasoner/notation.tex (revision 202) @@ -144,5 +144,5 @@ -As usual in IVML, we denote collection operations using the arrow and iterator notation, which involves the $|$ symbol for separating iterator variables from iterator expressions. However, as we use in this document the '$|$' symbol for variable substitutions, also using the same symbol in IVML collection expressions may be confusing. Thus, we use in collection expressions in this document ':' instead of '$|$', e.g., instead of \IVML{o->forall(x|$c(\IVML{x})$)} we denote \IVML{o->forall(x:$c(\IVML{x})$)} to indicate an all-quantized expression over a collection \IVML{o} applying the iterator variable \IVML{x} to some constraint $c(\IVML{x})$. +As usual in IVML, we denote collection operations using the arrow and iterator notation, which involves the $|$ symbol for separating iterator variables from iterator expressions. However, as we use in this document the '$|$' symbol for variable substitutions, also using the same symbol in IVML collection expressions may be confusing. Thus, we use in collection expressions in this document ':' instead of '$|$', e.g., instead of \IVML{o->forall(x|$\constraintWith{c}{\IVML{x}}$)} we denote \IVML{o->forall(x:$\constraintWith{c}{\IVML{x}}$)} to indicate an all-quantized expression over a collection \IVML{o} applying the iterator variable \IVML{x} to some constraint $\constraintWith{c}{\IVML{x}}$. %In summary, let \IVML{o} be an IVML collection of Integers, then \IVML{o->forall(i:i>20);} requires that all values in $o$ must be greater than 20. To create such a constraint with $o$ being an algorithm variable, we denote $\createConstraint{o\IVML{->forall(i:i>20)}}$. @@ -260,5 +260,5 @@ This is in particular important if $isCompound(nested^*(type(c)))$ holds for a container $c$, as then also values of refined types of $nested^*(type(c))$ may occur in $usedTypes(c)$. -For containers, element \emph{access expressions} frequently occur in terms of the iterator variable of container operations, e.g., quantors, or through index access to sequence elements. For example, let \IVML{seq} be a sequence of compounds, all having a common slot \IVML{slot}. Then $\IVML{seq->forAll(e|}c(\IVML{e.slot})\IVML{)}$ is a quantorized expression based on the iterator variable \IVML{e}. As \IVML{seq[1]} is an index-based access for the second element in the container\footnote{In contrast to OCL, IVML indexes are 0-based.}, accessing \IVML{slot} on the second element happens through \IVML{seq[1].slot}. For creating the respective expression within an algorithm, we denote $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. +For containers, element \emph{access expressions} frequently occur in terms of the iterator variable of container operations, e.g., quantors, or through index access to sequence elements. For example, let \IVML{seq} be a sequence of compounds, all having a common slot \IVML{slot}. Then $\IVML{seq->forall(e|}\constraintWith{c}{\IVML{e.slot}}\IVML{)}$ is a quantorized expression based on the iterator variable \IVML{e}. As \IVML{seq[1]} is an index-based access for the second element in the container\footnote{In contrast to OCL, IVML indexes are 0-based.}, accessing \IVML{slot} on the second element happens through \IVML{seq[1].slot}. For creating the respective expression within an algorithm, we denote $\createExpression{\IVMLMeta{acc}(\IVML{seq[1]}, \IVML{slot})}$. Akin to compounds, containers can be initialized by complex values, so called \emph{container initializers}, here as a listing of possible complex values. If the container is a sequence, the given order of values in the container initializer used as (initial) order of the sequence elements. Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 201) +++ /reasoner/reasoner.tex (revision 202) @@ -21,4 +21,6 @@ \newcommand\IVMLnull[0]{\texttt{null}} \newcommand\IVMLMeta[1]{\texttt{#1}} %\underline{} +\newcommand\IVMLforalla[4]{#1\rightarrow\IVML{forall(}#2#3#4\IVML{(}} +\newcommand\IVMLforall[3]{\IVMLforall{#1}{#2}{:}{#3}} \newcommand\addSet[0]{\cup} \newcommand\addSeq[0]{\oplus} @@ -43,4 +45,5 @@ \newcommand\createConstraint[1]{\langle #1 \rangle} \newcommand\createDefaultConstraint[1]{\langle #1 \rangle_d} +\newcommand\constraintWith[2]{#1(#2)} \newcommand\isDefaultConstraintName[0]{isDefault} \newcommand\isDefaultConstraint[1]{\isDefaultConstraintName(#1)}