Predefined Collection

[EagleoutIce]

Somewhat related to #7.

• Numerical Sets (\N, \Z, ...)
• Set Operators (\P, \union, \intersect, ...)
• Galois (\alpha, arrows, ...)
• Type Groups (\Bool)
• Readability helpers (\For, \Given, \isAbstract)
• Evaluate* (\EvaluateStatement, \SetOfStates)
• Operators (\intmul, \intadd, ...)
• Intervals, Lattice Wrapper, etc.

[schuler-henry]

For Evaluate* i have defined the related statement/... elements:

\def\statement{s}
\def\statementLong{stat}
\def\expression{e}
\def\expressionLong{expr}
\def\condition{c}
\def\conditionLong{cond}

[schuler-henry]

FYI - Aktuell sind das alle Commands die ich on top definiert hab:

%%% Abstract Interpretation Formula Notation (based on tex-notations) %%%

% Domain unspecific commands
\def\EvaluateStatementInDomain#1#2{\RawEvaluateStatement#1\llbracket\,#2\,\rrbracket}
\def\EvaluateExpressionInDomain#1#2{\RawEvaluateExpr#1\llbracket\,#2\,\rrbracket}
\def\EvaluateConditionInDomain#1#2{\RawEvaluateCond#1\llbracket\,#2\,\rrbracket}

\newcommand*{\galois}[2]{\xlongleftrightarrows{#1}{#2}}
\newcommand*{\xlongleftrightarrows}[2]{\mathrel{\raise1.5ex\hbox{\oalign{%
  \(\scriptstyle\hfil\smash#1\hfil\)\cr%
  \(\scriptstyle\leftarrow\joinrel\relbar\joinrel\relbar\joinrel\relbar\hfil\)\cr%
  \vrule width0pt height.25ex\(\scriptstyle\hfil\relbar\joinrel\relbar\joinrel\relbar\joinrel\smash\rightarrow\)\cr%
  \(\scriptstyle\hfil#2\hfil\)\cr%
}}}}

\def\Variable{V}
\def\Value{x}
\def\Statement{s}
\def\Statements{stat}
\def\Expression{e}
\def\Expressions{expr}
\def\Condition{c}
\def\Conditions{cond}

% Domain type specific commands

%% Concrete State Domain
\def\ConcreteStateDomain{\SetOfStates}
\def\ConcreteState{\Environment}
\def\ConcreteStates{R}

%% Concrete Value Domain
\def\ConcreteValueDomain{\Universe}
\def\ConcreteValue{c}

%% Abstract Domain
\def\isAbstract{^\#}
\def\AbstractDomain{\mathcal{D}\isAbstract}
\def\ConcretizationFunction{\gamma}
\def\AbstractionFunction{\alpha}
\def\widen{\triangledown}
\def\narrow{\triangle}

%% Abstract State Domain
\def\AbstractStateDomain{\mathcal{D}\isAbstract}
\def\AbstractState{R\isAbstract}
\def\AbstractStateTwo{S\isAbstract}

%% Abstract Value Domain
\def\isValue{_b}
\def\AbstractValueDomain{\mathcal{B}\isAbstract}
\def\AbstractValue{b}

%% Cartesian Product
\def\ProductElem#1{\langle#1\rangle}%
\def\CartesianOperator{\times}
\def\isCartesianProduct{_{\CartesianOperator}}

%% Reduced Cartesian Product
\def\ReducedCartesianOperator{\otimes}
\def\isReducedCartesianProduct{_{\ReducedCartesianOperator}}
\def\ReductionOperator{\sigma}
\def\ReductionFixpoint{\sigma^*}
\def\Equivalence{\equiv}%
\def\EquivalenceClass#1#2{#1/{#2}}%

% Domains

%% Abstract Interval Value Domain
\def\AbstractIntervalValueDomain{\mathcal{B}\isAbstract}
\def\isInterval{_b}
\def\AbstractIntervalValue{b}

%% Abstract Interval State Domain
\def\AbstractIntervalStateDomain{\mathcal{D}\isAbstract}
\def\AbstractIntervalState{R\isAbstract}
\def\ApplyIntervalStatement#1{\EvaluateStatementInDomain{\isAbstract}{#1}\AbstractIntervalState}
\def\ApplyIntervalExpression#1{\EvaluateExpressionInDomain{\isAbstract}{#1}\AbstractIntervalState}
\def\ApplyIntervalCondition#1{\EvaluateConditionInDomain{\isAbstract}{#1}\AbstractIntervalState}

%% Abstract Upper Bounds Domain
\def\AbstractUpperBoundsDomain{\mathcal{U}\isAbstract}
\def\isUpperBound{_u}
\def\AbstractUpperBoundsState{M\isAbstract}
\def\ApplyUpperBoundsStatement#1{\EvaluateStatementInDomain{\isAbstract\isUpperBound}{#1}\AbstractUpperBoundsState}
\def\ApplyUpperBoundsCondition#1{\EvaluateConditionInDomain{\isAbstract\isUpperBound}{#1}\AbstractUpperBoundsState}

%% Abstract Pentagon Domain
\def\AbstractPentagonDomain{\mathcal{CP}\isAbstract}
\def\isPentagon{_{cp}}
\def\AbstractPentagonState{\ProductElem{\AbstractIntervalState, \AbstractUpperBoundsState}}%
\def\ApplyPentagonStatement#1{\EvaluateStatementInDomain{\isAbstract\isPentagon}{#1}\AbstractPentagonState}
\def\ApplyPentagonCondition#1{\EvaluateConditionInDomain{\isAbstract\isPentagon}{#1}\AbstractPentagonState}

%%% Refinement of the Interval semantics when applied on the pentagon domain
\def\isPentagonInterval{_{cp(b)}}
\def\ApplyPentagonIntervalStatement#1{\EvaluateStatementInDomain{\isAbstract\isPentagonInterval}{#1}\AbstractPentagonState}
\def\ApplyPentagonIntervalCondition#1{\EvaluateConditionInDomain{\isAbstract\isPentagonInterval}{#1}\AbstractPentagonState}
\def\ApplyPentagonIntervalExpression#1{\EvaluateExpressionInDomain{\isAbstract\isPentagonInterval}{#1}\AbstractPentagonState}

%%% END %%%