Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 80) +++ /reasoner/reasoner.tex (revision 81) @@ -31,4 +31,6 @@ \newcommand\seqEmpty[0]{\set{\text{}}} \newcommand\seqWith[2]{[#1:#2]} +\newcommand\subTypeOf[2]{t \succ s} +\newcommand\subTypeEqOf[2]{t \succeq s} \newcommand\createConstraint[1]{\langle #1 \rangle} \newcommand\createDefaultConstraint[1]{\langle_d\text{ } #1 \rangle} @@ -41,4 +43,7 @@ \newcommand\varSubstitutionOtherVarMapping[2]{\varSubstitution{#1}{#2, \variableMapping}} \newcommand\varSubstitutionSelfVarMapping[2]{\varSubstitutionOtherVarMapping{#1}{\IVMLself = #2}} +\newcommand\tabAlgLine[2]{Alg.\ref{#1},\ref{#2}} +\newcommand\tabAlgLines[3]{Alg.\ref{#1},\ref{#2}-\ref{#3}} +\newcommand\tabAlgFollow[0]{$\rightarrow$} \let\emph\relax % there's no \RedeclareTextFontCommand @@ -218,5 +223,7 @@ \end{cases}$$ % -as the set of all refined compounds along the compound refinement / inheritance hierarchy of $t$ including $t$. Based on these functions, the set of all slots for compound type $t$ can be derived by +as the set of all refined compounds along the compound refinement / inheritance hierarchy of $t$ including $t$. We denote for $t$ and $s$ compounds $\subTypeOf{t}{s}$ if $t\in allRefines(s)$, i.e., $s$ is a subtype of $t$. Similarly, $\subTypeEqOf{t}{s}$ if $t\in allRefines^+(s)$. + +Based on the functions above, the set of all slots for compound type $t$ can be derived by % $$slots^+(t) = \setWith{slots(r)}{r\in allRefines^+(t)}$$ @@ -541,7 +548,7 @@ }\lElseIf{$inc$}{$ dflt \assng \undef $} \If{$ deflt \neq \undef $}{ - \uIf{$isConstraint(type(d))$}{ + \uIf{$isConstraint(type(d))$}{ \label{algTranslateDeclarationTranslateConstraintDefaultStart} $createConstraintVariableConstraint(dflt, s, v)$\; \label{algTranslateDeclarationConstraintVariableConstraint} - }\Else{ + }\Else{ \label{algTranslateDeclarationTranslateConstraintDefaultEnd} \uIf{$isAnnotation(v)$}{ $ac\assng \closedCases{\IVMLMeta{acc}(d,a), & \text{if } ca = \undef \\ \IVMLMeta{acc}(ca,a), &\text{else}}$\;\label{algTranslateDeclarationTranslateAnnotationAccess} @@ -687,6 +694,12 @@ \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{asType} operation to have access to specific operations, slots or annotations. - +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$. +% +$$ +d\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if nested}}\underbrace{\IVML{selectByKind}(t)\rightarrow}_{\text{if } \subTypeOf{t}{nested(c)}}\IVML{forAll}(l|c) +$$ +% Thus, the core idea of this algorithm is to consider all elements over all used types. If no value is available, we resort to the static type of the declaration of the containser variable. We create all-quantized constraints for all used types and distinguish between constraint containers, where the values directly turn into constraints, compound containers, where slots, constraints and annotations lead to further constraints, and derived types. @@ -722,8 +735,8 @@ % $$ -\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}|\varSubstitutionOtherVarMapping{c}{l_2})) +\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)) $$ % -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. If we now want to create a constraint $c$ in this context, we perform a variable substitution in particular injecting $l_2$ as $ca$ into $c$ and pass $\varSubstitutionOtherVarMapping{c}{l_2}$ on to the $add$ algorithm (details in Section \ref{algAddConstraints}). As a first step, the $add$ algorithm executes Algorithm \ref{algComposeExpression}, which composes the full constraint. +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. @@ -898,10 +911,12 @@ \begin{adjustbox}{angle=90} \centering -\begin{tabular}{|l|c||p{8cm}|p{6cm}|} +\begin{tabular}{|l|c||p{6cm}|p{5cm}|} \hline -\textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation} & textbf{Test}\\ +\textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation} & \textbf{Test}\\ \hline -Decision variable & 2.1.4 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTranslationDeclaration} $\rightarrow$ Alg. \ref{algTranslateDeclaration}, \ref{algTranslateDeclarationTranslateDefault}; annotation defaults in line \ref {algTranslateDeclarationAnnotationDefault} $\rightarrow$ Alg. \ref{algTranslateAnnotationDefaults} & \\ -Constraint & & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelConstraints} & \\ +Decision variable & 2.1.4 & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLine{algTranslateDeclaration}{algTranslateDeclarationTranslateDefault} & \\ +Constraint & & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTopLevelConstraints} & \\ +Constraint variable & & \tabAlgLine{algTranslateConstraints}{algTranslateConstraintsTranslationDeclaration}\tabAlgFollow\tabAlgLines{algTranslateDeclaration}{algTranslateDeclarationTranslateConstraintDefaultStart}{algTranslateDeclarationTranslateConstraintDefaultEnd} & \\ +Annotation variable & & annotation defaults in line \ref {algTranslateDeclarationAnnotationDefault} $\rightarrow$ Alg. \ref{algTranslateAnnotationDefaults} & \\ Annotation assignment & 2.2.2 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelAnnotationAssignments} $\rightarrow$ Alg. \ref{algTranslateAnnotationAssignments} & \\ Partial evaluation & 2.2.5.3 & Alg. \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals} & \\ @@ -933,7 +948,7 @@ \begin{adjustbox}{angle=90} \centering -\begin{tabular}{|l|c||p{8cm}|p{6cm}|} +\begin{tabular}{|l|c||p{6cm}|p{5cm}|} \hline -\textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation} & textbf{Test}\\ +\textbf{IVML concept} & \textbf{Spec} & \textbf{Transformation} & \textbf{Test}\\ \hline + Constraint & 2.1.3.5 & & \\