Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 54) +++ /reasoner/reasoner.tex (revision 55) @@ -32,4 +32,9 @@ \newcommand\createExpression[1]{\langle\langle #1 \rangle\rangle} \newcommand\closedCases[1]{\left.\begin{cases}#1\end{cases}\right\}} +\newcommand\variableMapping[0]{vm} +\newcommand\varSubstitution[2]{#1|_{#2}} +\newcommand\varSubstitutionVarMapping[1]{\varSubstitution{#1}{\variableMapping}} +\newcommand\varSubstitutionOtherVarMapping[2]{\varSubstitution{#1}{#2, \variableMapping}} +\newcommand\varSubstitutionSelfVarMapping[2]{\varSubstitutionOtherVarMapping{#1}{\IVMLself = #2}} \let\emph\relax % there's no \RedeclareTextFontCommand @@ -162,4 +167,6 @@ 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 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 set of $\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}$. + 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)}$ @@ -256,5 +263,4 @@ \newcommand\otherConstraints[0]{c_{o}} \newcommand\topLevelConstraints[0]{c_{t}} -\newcommand\variableMapping[0]{vm} \newcommand\relevantConstraints[0]{r_t} \newcommand\scopeAssignments[0]{a} @@ -430,22 +436,19 @@ $translateDerivedDatatypeConstraints(d)$\; \label{algTranslateDeclarationDerivedDatatype} - \If{$\neg inc$} { - $translateAnnotationDefaults(cfg, d, \undef)$\; \label{algTranslateDeclarationAnnotationDefault} - } -\MISSING{Here}\; - $t \assng type(d)$; $dflt \assng default(d)$; $dfltS \assng \defaultConstraints$\; + \lIf{$\neg inc$} { + $translateAnnotationDefaults(cfg, d, \undef)$ \label{algTranslateDeclarationAnnotationDefault} + } +\MISSING{CHECKING: Here}\; + $t \assng type(d)$; $dflt \assng default(d)$; $dfltS \assng \defaultConstraints$; $s \assng \undef$\; \uIf{$isCompound(t)$}{ - \lIf{$ dflt \neq \undef $}{$t = type(dflt)$} + \lIf{$ dflt \neq \undef $}{$t = type(dflt)$; $s = \createExpression{v}$} $translateCompoundDefaults(d, v, ca, t)$\; - \lIf{$ dflt \neq \undef $}{$ dflt \assng deflt|_{\IVMLself{}=d, \variableMapping}$} + %\lIf{$ dflt \neq \undef $}{$ dflt \assng \varSubstitutionSelfVarMapping{deflt}{d}$} } \uElseIf{$ dflt \neq \undef \wedge \neg inc$}{ \label{algTranslateDeclarationHasDefault} \uIf{$ isContainer(type(d)) $}{ - \ForAll{$u \iterAssng usedTypes(dflt)$}{ - \MISSING{derived types: coCompoundConstraints, translateCollIntConstraints here?} - $translateDefaultsCompoundsContainer(d, u)$\; - } + $translateDefaultsCompoundsContainer(d);$\; }\ElseIf{$ca \neq \undef$}{ \lIf{$\IVMLself{} \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng \deferredDefaultConstraints$} - $dflt \assng dflt|_{\IVMLself =ca, \variableMapping}$\; + $dflt \assng \varSubstitutionSelfVarMapping{dflt}{ca}$\; } } \uElse{$ dflt \assng \undef $\;} @@ -457,8 +460,9 @@ \uIf{$isConstraint(t)$}{ \lIf{$ ca == \undef $}{ + \MISSING{substitution here?}\; $add(\otherConstraints, \createConstraint{dflt}, true)$\; $\relevantConstraints \assng \relevantConstraints \cup (\createConstraint{dflt}, v)$} }\Else{ - $add(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, deflt)})$\; \label{algTranslateDeclarationTranslateDefault} + $add(dfltS, \createDefaultConstraint{\IVML{assign}(\closedCases{ca, & \text{if } dfltS == \defaultConstraints \\ d, &\text{else}}, \varSubstitutionSelfVarMapping{deflt}{s})})$\; \label{algTranslateDeclarationTranslateDefault} } } @@ -477,5 +481,5 @@ $cs \assng \bigcup_{t \in allBase(type(d))} constraints(t)$\; - $add(\topLevelConstraints, \setWith{\createConstraint{c|_{decl(c)=d}}}{c\in cs}, true)$\; + $add(\topLevelConstraints, \setWith{\createConstraint{\varSubstitution{c}{decl(c)=d}}}{c\in cs}, true)$\; \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints} \end{algorithm} @@ -489,5 +493,5 @@ $cs \assng \bigcup_{t \in allBase(t} constraints(t)$\; - $add(\topLevelConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }c|_{decl(c)=d})}}{c \in cs}, true)$\; + $add(\topLevelConstraints, \setWith{\createConstraint{\closedCases{d, & \text{if } ca = \undef \\ ca, &\text{else}}\rightarrow\IVML{forAll}(i|\text{ }\varSubstitution{c}{decl(c)=d})}}{c \in cs}, true)$\; \caption{Translating constraints for derived container types (\IVML{translateContainerDerivedDatatypeConstraints}).}\label{algTranslateContainerDerivedDatatypeConstraints} \end{algorithm} @@ -567,8 +571,8 @@ \ForAll{s \iterAssng slots(v)} { %actual slots \If{$isConstraintContainer(type(s))$} { - $add(\otherConstraints, \setWith{\createConstraint{value(e)|_{\IVMLself =d, \variableMapping}}}{e \in elements(value(s))}, true)$\; + $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{value(e)}{d}}}{e \in elements(value(s))}, true)$\; } \If{$isConstraint(type(s)) \wedge default(s) \neq \undef$}{ - $add(\otherConstraints, \set{\createConstraint{default(s)|_{\IVMLself =d, \variableMapping}}}, true)$\; + $add(\otherConstraints, \set{\createConstraint{\varSubstitutionSelfVarMapping{default(s)}{d}}}, true)$\; } $add(\otherConstraints, translateContainerCompoundConstraints(s, v, \variableMapping[s]), true)$\; @@ -579,6 +583,6 @@ } } - $add(\otherConstraints, \setWith{\createConstraint{c|_{\IVMLself =d, \variableMapping}}}{c\in allCompoundConstraints(t, false)}, true)$\; - $add(\otherConstraints, \setWith{\createConstraint{c|_{vm}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\; + $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionSelfVarMapping{c}{d}}}{c\in allCompoundConstraints(t, false)}, true)$\; + $add(\otherConstraints, \setWith{\createConstraint{\varSubstitutionVarMapping{c}}}{c\in \bigcup_{r\in allRefines^+(t)} allEvalConstraints(r)}, true)$\; \caption{Translating annotation defaults (\IVML{translateCompoundDefaults}).}\label{algTranslateCompoundDefaults} @@ -632,5 +636,17 @@ \subsection{Container default constraints}\label{sectContainerDefaults} -Constraints defined on types that are implicitly instantiated within a container must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundContainer} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested container). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the container using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVMLself{} substituted by the iterator variable $i$. +Constraints defined on types that are implicitly instantiated within a container must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algTranslateDefaultsCompoundContainer} performs this transformation by identifying the actual types used in a container and by deriving all constraints for this container. In turn, it calls Algorithm \ref{algTranslateDefaultsCompoundContainer2}. + +Algorithm \ref{algTranslateDefaultsCompoundContainer2} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested container). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the container using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVMLself{} substituted by the iterator variable $i$. + +\begin{algorithm}[H] + \SetAlgoLined + + \ForAll{$u \iterAssng usedTypes(default(d))$}{ + \MISSING{derived types?} + $translateDefaultsCompoundsContainer(d, u)$\; + } + \caption{Translating defaults in compound containers (\IVML{translateDefaultsCompoundContainer}).}\label{algTranslateDefaultsCompoundContainer} +\end{algorithm} \begin{algorithm}[H] @@ -639,8 +655,8 @@ \KwData{deferred default constraints $\deferredDefaultConstraints$} \ForAll{$s \iterAssng \setWith{dfltSlots(u)}{u \in allRefines^+(t)}$}{ - $add(\deferredDefaultConstraints, \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), default(s)|_{\IVMLself =i, \variableMapping})})$\; + $add(\deferredDefaultConstraints, \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(\IVMLMeta{var}(i,t)|\IVML{assign}(i.name(s), \varSubstitutionSelfVarMapping{default(s)}{i})})$\; } - \caption{Translating defaults in compound containers (\IVML{translateDefaultsCompoundContainer}).}\label{algTranslateDefaultsCompoundContainer} + \caption{Translating defaults in compound containers (\IVML{translateDefaultsCompoundContainer}).}\label{algTranslateDefaultsCompoundContainer2} \end{algorithm} @@ -679,5 +695,5 @@ $coll \assng\createExpression{\closedCases{ca, & \text{if } ca = \undef \\ d, &\text{else}}}$\; $coll \assng\createExpression{coll.\closedCases{\IVML{selectByKind}(a, t), & \text{if } t \neq dt \\ &\text{else}}}$\; - $c\assng c \cup \createConstraint{coll\rightarrow\IVML{forAll}(i|\text{ }e|_{\variableMapping})}$\; + $c\assng c \cup \createConstraint{coll\rightarrow\IVML{forAll}(i|\text{ }\varSubstitutionVarMapping{e})}$\; } @@ -692,7 +708,7 @@ \If{$check$}{ \If{$isContainerInitializer(c)$} { - $\otherConstraints \assng \otherConstraints \addSeq checkCompoundInitializer(c, m)$\; + $\otherConstraints \assng \otherConstraints \addSeq checkCompoundInitializer(c, \variableMapping)$\; }\ElseIf{$isCompoundInitializer(c)$}{ - $\otherConstraints \assng \otherConstraints \addSeq checkCompoundInitializer(c, m)$\; + $\otherConstraints \assng \otherConstraints \addSeq checkCompoundInitializer(c, \variableMapping)$\; } } @@ -710,9 +726,10 @@ %\end{align*} \begin{align*} -checkContainerInitializer(c, m) = \seqWith{\closedCases{e|_m, & \text{if } m \ne \undef \\ e &\text{else}}}{e\in expr(c)} +checkContainerInitializer(c, \variableMapping) = \seqWith{\closedCases{\varSubstitutionVarMapping{e}, & \text{if } \variableMapping \ne \undef \\ e &\text{else}}}{e\in expr(c)} \end{align*} \begin{align*} -check&CompoundInitializer(c, m) =\\ - &\seqWith{\closedCases{checkContainerInitializer(e, m), & \text{if } isContainerInitializer(e) \\ checkCompoundInitializer(e, m) &\text{if } isCompoundInitializer(e)\\ \setEmpty, & \text{else}}}{e\in expr(c)} +check&CompoundInitializer(c, \variableMapping) =\\ + &\seqWith{\closedCases{checkContainerInitializer(e, \variableMapping), & \text{if } isContainerInitializer(e) \\ + checkCompoundInitializer(e, \variableMapping) &\text{if } isCompoundInitializer(e)\\ \setEmpty, & \text{else}}}{e\in expr(c)} \end{align*}