Index: /reasoner/consTranslation.tex =================================================================== --- /reasoner/consTranslation.tex (revision 212) +++ /reasoner/consTranslation.tex (revision 213) @@ -78,9 +78,9 @@ As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined as a restriction or an alias of its base type $base(t)$. A derived type $t$ is a type restriction of $base(t)$, if $t$ defines constraints over $base(t)$ using the local variable $decl(t)$ of type $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$. In particular, $base(t)$ can be another derived type. If variable $v$ is of derived type $t$, all constraints defined for $t$ must hold for $v$. Moreover, if $base(t)$ is a derived type, all constraints defined for all base types $allBase(t)$ of $t$ must hold transitively. %Whether these constraints are fullfilled depends on the actual value of $v$. -The constraint translation follows this chained structure of base types and instantiates all constraints as shown in the following translation patterns: +The constraint translation follows this chained structure of base types and instantiates all constraints as shown in the translation patterns: \grayPara{ \patternDerivationLabel{\IVML{typedef } T \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{c}{decl(u)=deref(u, v), \variableMapping}}{formDerivedDatatypeConstraints} - \patternDerivationLabel{\IVML{typedef } containerOf(T) \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{\IVMLforall{v}{i}{c}}{decl(u)=deref(u, i), \variableMapping}}{formDerivedDatatypeConstraintsContainer} + \patternDerivationLabel{\IVML{typedef } \IVMLcontainer{T} \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{\IVMLforall{v}{i}{c}}{decl(u)=deref(u, i), \variableMapping}}{formDerivedDatatypeConstraintsContainer} } @@ -278,15 +278,18 @@ \grayPara{ \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}}{\nonumber\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}\IVMLforall{f(v, t)}{\IVML{i}}{\varSubstitution{\constraintWith{c}{x}}{x=\IVML{i}, \IVMLself{}=\IVML{i}, \variableMapping}}}{forContainerQuant} - \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}{forContainerTop} + \patternDerivationLabel{\IVMLcontainer{\IVML{Constraint}}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\nonumber\\\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}{forConstraintContainer} + \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}{forContainerTop} } -There are two basic translation patterns for containers: Pattern \ref{forContainerQuant} considers all used element types in $v$ and Pattern \ref{forContainerTop} illustrates the transformation for top-level container variables. +There are three basic translation patterns for containers: Pattern \ref{forContainerQuant} considers all used element types in $v$, Pattern \ref{forConstraintContainer} handles containers containing constraints and Pattern \ref{forContainerTop} illustrates the transformation for top-level container variables. \begin{itemize} -\item For each constraint defined for the element types used in the actual value of container $v$, Pattern \ref{forContainerQuant} creates an all-quantified constraint over $v$. Let $t$ be a used element type in $v$. Then we can apply the constraints defined for $t$ by a quantification over all container elements (of type $t$). Let $c(x)$ be a constraint defined for type $t$, i.e., the constraint is expressed over variable $x$ of type $t$. If we want to apply $c(x)$ to all container elements of type $t$, we all-quantify the container and express $c(x)$ over the iterator variable $i$ of type $t$, i.e., substitute in particular $x$ and \IVMLself{} by $i$. However, if $v$ is a nested container, we may have to flatten $v$, i.e., remove all nested containers, to apply the constraint to the individual elements. Further, if $\subTypeOf{t}{T}$, accessing specific compound slots requires type casting / selection on the element values. Whether we need these additional container operations depends on the actual types of $v$ and $t$. We generivally represent these operations in Pattern \ref{forContainerQuant} by $f(v, t)$. Although indivdual quantified constraints may appear superfluous, i.e., we might aim at creating joined quantified expressions for individual types, the individual constraints are needed to provide detailed reasoning error messages. - -\item Pattern \ref{forContainerTop} defines the usual translation for top-level constraints over collection variables, i.e., the potential need to substitute top-level variables by the actual access expressions collected in $\variableMapping$. +\item For each constraint defined for the element types used in the actual value of container $v$, Pattern \ref{forContainerQuant} creates an all-quantified constraint over $v$. Let $t$ be a used element type in $v$. Then we can apply the constraints defined for $t$ by a quantification over all container elements (of type $t$). Let $c(x)$ be a constraint defined for type $t$, i.e., the constraint is expressed over variable $x$ of type $t$. If we want to apply $c(x)$ to all container elements of type $t$, we all-quantify the container and express $c(x)$ over the iterator variable $i$ of type $t$, i.e., substitute in particular $x$ and \IVMLself{} by $i$. However, if $v$ is a nested container, we may have to flatten $v$, i.e., remove all nested containers, to apply the constraint to the individual elements. Further, if $\subTypeOf{t}{T}$, accessing specific compound slots requires type casting / selection on the element values. Whether we need these additional container operations depends on the actual types of $v$ and $t$. We generically represent these operations in Pattern \ref{forContainerQuant} by $f(v, t)$. Although individual quantified constraints may appear superfluous, i.e., we might aim at creating joined quantified expressions for individual types, the individual constraints are needed to provide detailed reasoning error messages. + +\item Constraint containers are containers containing of constraints. The particular transformation required here is to extract all element values, to turn them into constraints and to add them to the constraint base as indicated by Pattern \ref{forConstraintContainer}. If the values in the constraint container change, the constraint re-scheduling must change the constraint base accordingly. As no further constraints can be attached to the constraint type (cf. Section \ref{sectNotationOthers}), Pattern \ref{forContainerQuant} and Pattern \ref{forConstraintContainer} do not need to be combined. + +\item Pattern \ref{forContainerTop} defines the usual translation for top-level constraints over collection variables, i.e., the potential need to substitute top-level variables by the actual access expressions collected in $\variableMapping$. In fact, Pattern \ref{forContainerTop} can be combined with Pattern \ref{forConstraintContainer} or Pattern \ref{forContainerQuant}. \end{itemize} -We will focus here on Pattern \ref{forContainerQuant}, as Pattern \ref{forContainerTop} is implicitly handled by the translation of top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}. First, we detail $f(v,t)$ in Section \ref{sectAdjContainer}. Then, we discuss Algorithm \ref{algTranslateContainerDeclaration} in Section \ref{sectTranslContainer} as well as subsequent algorithms. +We will focus here on Pattern \ref{forContainerQuant}, as Pattern \ref{forContainerTop} is implicitly handled by the translation of top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}. First, we detail $f(v,t)$ in Section \ref{sectAdjContainer}. Then, we discuss Algorithm \ref{algTranslateContainerDeclaration} in Section \ref{sectTranslContainer} as well as subsequent algorithms, namely the translation of compound containers in Section \ref{sectCompoundContainer} and the incremental container quantification in Section \ref{sectContainerQuantification}. \subsubsection{Adjusting Containers}\label{sectAdjContainer} @@ -307,8 +310,8 @@ \subsubsection{Translating Containers}\label{sectTranslContainer} -Algorithm \ref{algTranslateContainerDeclaration} translates a container variable declaration. The core idea of this algorithm is to determine the used types for all container elements and for each type to instantiate the constraints as explained above. However, used types are only availabe if a container value has been assigned. If no container value is available, we resort to the static type of the declaration of the container variable. During constraint translation, we distinguish between constraint containers, for which we directly turn the values into constraints, and container types that may imply further constraints such as containers over compounds or containers over derived types. - -Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable declaration $d$ of variable $v$, if nested with given access expression $ca$ and actual type $t$. First, we create a new variable mapping context in $\variableMapping$ in line \ref{algTranslateContainerDeclarationPushContext} in order to keep marking processed types local to the actual container translation. Then, in line \ref{algTranslateContainerDeclarationInitTypes}, we determine the innermost nested type $t_n$ and its base type $t_b$ (i.e., ignoring intermediate derived types) as well as the relevant value $val$ (cf. Section \ref{sectNotationValues}). If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we translate all container constraints, i.e., (flattened) element values representing constraints in line \ref{algTranslateContainerDeclarationConstraintContainer}. If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the (actual) types used in the container. If there is a compound value, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. As the translation algorithm traverses the refinement hierarchy a given type, we prune all general compound types and continue operating only on the most specific types in line \ref{algTranslateContainerDeclarationUsedTypesPrune}. If there is no value, we fall back to the innermost nested base (compound) type $t_b$ as the only used type (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). Then, we iterate over all (pruned) used types and apply Algorithm \ref{algTranslateCompoundContainer}. Independently of constraint or compound container, we finally translate and collect all constraints stemming from derived type definitions in line \ref{algTranslateContainerDeclaration} and pop the initially created context in line \ref{algTranslateContainerDeclarationDerivedTypes}. - +Algorithm \ref{algTranslateContainerDeclaration} translates a container variable declaration. The core idea of this algorithm is to determine the used types for all container elements and for each type to instantiate the constraints as shown in Pattern \ref{forContainerQuant}. However, used types are only available if a container value has been assigned. If no container value is given\footref{fnVariableNull}, we resort to the static type from the declaration of the container variable. Containers consisting of constraints (Pattern \ref{forConstraintContainer}) are treated as a special case in Algorithm \ref{algTranslateContainerDeclaration}. Moreover, the element type may be a derived type, so we also have to consider constraints attached to a potential chain of derived types. + +Algorithm \ref{algTranslateContainerDeclaration} performs the transformation for a container variable $v$ of declaration $d$, if nested with given access expression $ca$ and actual type $t$. + \begin{algorithm}[H] \SetAlgoLined @@ -344,4 +347,14 @@ \end{algorithm} +In line \ref{algTranslateContainerDeclarationPushContext}, we create a new variable mapping context in $\variableMapping$ in order to keep accessor expressions and processed types local to the actual container translation. In line \ref{algTranslateContainerDeclarationInitTypes}, we determine the innermost nested type $t_n$, its base type $t_b$ (ignoring intermediate derived types) as well as the relevant value $val$ (cf. Section \ref{sectNotationValues}). + +If $v$ is a constraint container, i.e., the innermost nested base type is a constraint, we apply Pattern \ref{forConstraintContainer}. We translate all (flattened) element values to individual container constraints applying a respective substitution and add the resulting constraints to the other constraints sequence $\otherConstraints$ (line \ref{algTranslateContainerDeclarationConstraintContainer}). + +If $v$ is a compound container, i.e., the innermost nested base type is a compound, we consider the (actual) types used in the container. As nested containers are handled through $f(v, t)$, we apply here Pattern \ref{forContainerQuant} except for basic IVML types that cannot have constraints (cf. Section \ref{sectNotationOthers}). If there is a container value in $v$, we determine the used contained compound types in line \ref{algTranslateContainerDeclarationUsedTypesDefault}. As the translation algorithm will traverse the refinement hierarchy for each type in $used$, we can focus on the most specific types, i.e., skip less specific types in the respective refinement hierarchy (line \ref{algTranslateContainerDeclarationUsedTypesPrune}). If there is no value for $v$, we use the innermost nested base (compound) type $t_b$ as fallback, i.e., the only (known) used type in the container (line \ref{algTranslateContainerDeclarationUsedTypesFallback}). Then, we iterate over all (most specific) used types and apply Algorithm \ref{algTranslateCompoundContainer}. + +Independently whether $v$ is a constraint or a compound container, the element type may be a (chained) derived type. To handle the implied constraints, we translate and collect all constraints stemming from $t_n$ in line \ref{algTranslateContainerDeclaration}. It is important to recall here that Algorithm \ref{algTranslateDerivedDatatypeConstraints}, which is called here, handles container quantification. Finally, we pop the context frame created at the beginning of the algorithm in line \ref{algTranslateContainerDeclarationDerivedTypes}. + +\subsubsection{Translating Compound Containers}\label{sectCompoundContainer} + Algorithm \ref{algTranslateCompoundContainer} translates a compound container declaration $d$ with access expression $ca$ based on a given actual element type $t$ and the declared elemnt type $t_d$. The idea of Algorithm \ref{algTranslateCompoundContainer} is to $f(v, t)$ in order to quantify the constraints in $t$ over all container elements in $d$ and to translate the individual constraints using the compound translation algorithms \ref{algRegisterCompoundMapping} and \ref{algTranslateCompoundContent}. As several constraints may need to be translated for $t$, Algorithm \ref{algTranslateCompoundContainer} creates the quantification prefix expression including $f(v, t)$ once and applies it for all constraints defined by $t$. As containers and compounds may be nested, Algorithm \ref{algTranslateCompoundContainer} stores the relevant information for the quantification prefix in the actual context frame of $\variableMapping$ and composes the complete quantification prefix when adding a translated constraint to the constraint base. Adding constraints happens by calling Algorithm \ref{algTranslateCompoundContent}, i.e., dependent on the type structure, this may cause a recursion involving also the general translation of declarations in Algorithm \ref{algTranslateDeclaration}. @@ -383,4 +396,6 @@ Akin to the translation of compounds in Algorithm \ref{algTranslateCompoundDeclaration}, the algorithm creates in line \ref{algTranslateCompoundPushContext} a context frame (always linked to the parent container frame) for the following compound transformation. As mentioned above, the algorithm stores in the new context frame the incrementally build-up quantification information, i.e., the iterator variable $l$ and the quantification prefix $e$ (without actual quantifier). This information is needed for creation of a potentially nested quantification for nested containers when adding individual constraints within this context frame. As for compounds, the algorithm creates in line \ref{algTranslateCompoundContainerMapping} the mapping using Algorithm \ref{algRegisterCompoundMapping}, the iterator variable $l$ as access expression and the actual type $t$ to avoid unnecessary type casts. Then, we call Algorithm \ref{algTranslateCompoundContent} to translate the compound slots also using the quantor iterator $l$ as access expression. As mentioned above, calling Algorithm \ref{algTranslateCompoundContent} implies a potential recursion over nested compounds and containers. Finally, the algorithm pops in line \ref{algTranslateCompoundContainerPopContext} the context frame created for the compound transformation. + +\subsubsection{Incremental Container Quantification}\label{sectContainerQuantification} So far, we focused on the translation algorithm rather than the creation of the quantification prefix expressions also for nested container structures. Although the actual creation happens when adding constraints to the constaint base, i.e., in the $add$ function (cf. Algorithm \ref{algAddConstraint} in Section \ref{sectContainerBase}), we explain the approach and the required function for the variable mapping $\variableMapping$ in this section. The base case was already explained above in Formula \ref{fSimpleContainerQuantorPrefix} and requires after the creation of the prefix expression in Algorithm \ref{algTranslateCompoundContainer} just the addition of an all-quantor over $l$ and a constraint using $l$ as access expression. We derive the respective algorithm from the expression for a nested compound container such as \IVML{setOf(C)} over a compound type \IVML{C}, which, in turn, declares a slot \IVML{s} of some compound container. The derived quantification prefix is illustrated below by Formula \ref{fNestedContainerQuantorPrefix}. As the creation of a nested prefix expression happens in several recursive calls of Algorithm \ref{algTranslateCompoundContainer}, we indicate in Formula \ref{fNestedContainerQuantorPrefix} the recursion level and the respective parameter / variable from Algorithm \ref{algTranslateCompoundContainer} below the created partial expression. @@ -521,7 +536,9 @@ \patternDerivation{\IVML{Constraint}~v = ex\IVML{;}}{\varSubstitution{ex}{\variableMapping}} \patternDerivation{\IVML{Compound}~C =~\IVML{\{Constraint } s = ex\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}}{\varSubstitution{ex}{\IVMLself{}=v, \variableMapping}} - \patternDerivation{\IVML{containerOf(Constraint)}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}} + \patternDerivation{\IVMLcontainer{\IVML{Constraint}}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}} \patternDerivation{\IVML{Compound}~C =~\IVML{\{containerOf(Constraint) } s = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}\nonumber\\}{\varSubstitution{ex_1}{\IVMLself{}=v, \variableMapping}, \ldots, \varSubstitution{ex_n}{\IVMLself{}=v, \variableMapping}} } + +% CONSTRAINT CONTAINER REPEATED!!! In more details, Algorithm \ref{algCreateConstraintVariableConstraint}\footnote{Here we abstract two implementation parameters for the self value/expression into one parameter and omit the parameter indicating the parent instance of the constraint to be created.} takes a constraint expression (e.g., the default value of a variable or a nested variable through Algorithm \ref{algTranslateDeclaration}), an optional expression $e_f$ representing \IVMLself{} and the variable $v$ the translation is applied to. Algorithm \ref{algCreateConstraintVariableConstraint} performs in line \ref{algCreateConstraintVariableConstraintCreate} a variable substitution with $\variableMapping$ and, if given, $e_f$, and turns the resulting expression into a (constraint variable) constraint. In line \ref{algCreateConstraintVariableConstraintAdd}, the algorithm adds the created constraint to the set of other constraints $\otherConstraints$. The third parameter of the $add$ function (will be discussed in Section \ref{sectContainerBase}) indicates whether the constraint be analyzed for complex value assignments that contain constraints as values for constraint variables. This is not required (and may sometimes lead to endless recursions) if the constraint here is a constant value. Finally, in line \ref{algCreateConstraintVariableConstraintRegister}, the relationship between the underlying variable $v$ and the constraint is recorded to enable efficient updates of the constraint base upon value change (cf. Algorithm \ref{algVarChange}).