org.jmlspecs.jmlrac.qexpr.Translator
org.jmlspecs.jmlrac.qexpr.StaticAnalysis
|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||
java.lang.Object
An abstract class for translating JML quantified expressions into Java source code. The translation is based on the static analysis of the expression's structures.
| Nested Class Summary | |
private static class |
StaticAnalysis.EnumerationBased
A concrete class for translating JML quantified expressions into Java source code. |
private static class |
StaticAnalysis.IntervalBased
A concrete class for translating JML quantified expressions into Java source code. |
private static class |
StaticAnalysis.SetBased
A concrete class for translating JML quantified expressions into Java source code. |
| Field Summary | |
protected RacContext |
context
current translation context |
protected static TokenReference |
NO_REF
|
protected JmlSpecQuantifiedExpression |
quantiExp
taget quantified expression to translate |
protected String |
resultVar
variable name to have the value of quantified expression in the translated code |
protected AbstractExpressionTranslator |
transExp
|
protected VarGenerator |
varGen
variable generator for generating unique local variables |
| Fields inherited from interface org.jmlspecs.jmlrac.RacConstants |
MN_CHECK_HC, MN_CHECK_INV, MN_CHECK_POST, MN_CHECK_PRE, MN_CHECK_XPOST, MN_EVAL_OLD, MN_GHOST, MN_INIT, MN_INTERNAL, MN_MODEL, MN_MODEL_PUBLIC, MN_RESTORE_FROM, MN_SAVE_TO, MN_SPEC, MN_SPEC_PUBLIC, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_SURROGATE, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_OLD_VAR, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_XRESULT |
| Constructor Summary | |
protected |
StaticAnalysis(VarGenerator varGen,
RacContext ctx,
JmlSpecQuantifiedExpression expr,
String resultVar,
AbstractExpressionTranslator transExp)
Constructs a StaticAnalysis object. |
| Method Summary | |
private String |
applySumOrProduct(String strResultVar,
String strOptr,
String strV2,
CType vType)
|
RacNode |
generateLoop(RacNode body)
Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range. |
protected abstract RacNode |
generateLoop(JVariableDefinition varDef,
JExpression qexpr,
String cond,
RacNode result)
Returns a loop code evaluating the body of the quantified predicate. |
static StaticAnalysis |
getInstance(VarGenerator varGen,
RacContext ctx,
JmlSpecQuantifiedExpression expr,
String resultVar,
AbstractExpressionTranslator transExp)
Returns an instance of StaticAnalysis, that
translates JML quantified expressions into Java source code. |
private JExpression |
rangePredicate()
Returns the range predicate of the quantified expression. |
protected RacNode |
transExpression(JExpression expr,
String var)
Returns code for evaluating expression expr and
storing the result to the variable var. |
private RacNode |
transForAllOrExists()
Returns Java source code for evaluating the JML quantified expression, which is either a universal or existential quantifier. |
RacNode |
translate()
Translate a JML quantified expression into Java source code and return the result. |
private RacNode |
translateExists()
Return Java source code for evaluating a JML quantified expression of an existential quantifier. |
private RacNode |
translateForAll()
Return Java source code for evaluating a JML quantified expression of a univeral quantifier. |
private RacNode |
translateMax()
Return Java source code for evaluating a JML quantified expression of a generalized quantifier \max. |
private RacNode |
translateMin()
Return Java source code for evaluating a JML quantified expression of a generalized quantifier \min. |
private RacNode |
translateNumOf()
Returns code for evaluating numerical quantifiers \num_of. |
private RacNode |
translateProduct()
Return Java source code for evaluating a JML quantified expression of a generalized quantifier \product. |
private RacNode |
translateSum()
Return Java source code for evaluating a JML quantified expression of a generalized quantifier \sum. |
private RacNode |
transMinOrMax()
Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \min
or \max. |
private RacNode |
transSumOrProduct()
Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \sum
or \product. |
private static JExpression |
unwrapJmlExpression(JExpression expr)
Unwraps a given JML expression if it is an instance of JmlPredicate or JmlSpecExpression. |
| Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
| Field Detail |
protected static final TokenReference NO_REF
protected VarGenerator varGen
protected RacContext context
protected JmlSpecQuantifiedExpression quantiExp
protected String resultVar
protected AbstractExpressionTranslator transExp
| Constructor Detail |
protected StaticAnalysis(VarGenerator varGen,
RacContext ctx,
JmlSpecQuantifiedExpression expr,
String resultVar,
AbstractExpressionTranslator transExp)
StaticAnalysis object.
varGen - variable generator to be used in translation for
generating unique local variables.expr - quantified expression to be translated.resultVar - variable name to have the value of quantified
expression in the translated code.transExp - translator to use for translating subexpressions of
the quantified expression.| Method Detail |
public static StaticAnalysis getInstance(VarGenerator varGen,
RacContext ctx,
JmlSpecQuantifiedExpression expr,
String resultVar,
AbstractExpressionTranslator transExp)
StaticAnalysis, that
translates JML quantified expressions into Java source code.
varGen - variable generator to be used in translation for
generating unique local variables.expr - quantified expression to be translated.resultVar - variable name to store the result value of quantified
expression in the translated code.transExp - translator to use for translating subexpressions.
public RacNode translate()
throws NonExecutableQuantifierException
NonExecutableQuantifierExceptionNonExecutableQuantifierException
private RacNode translateForAll()
throws NonExecutableQuantifierException
[[(\forall T x1, ..., xn; P; Q), r]] =
r = true;
Collection c1 = null;
[[S, c1]] // S is the qset of P ==> Q
Iterator iter1 = c1.iterator();
while (r && iter1.hasNext()) {
T x1 = iter1.next();
...
Collection cn = null;
[[S, cn]]
Iterator itern = cn.iterator();
while (r && itern.hasNext()) {
T xn = itern.next();
[[P ==> Q, r]]
}
...
}
If the type (T) of the quantified variables is
byte, char, short,
int, or long. The following rule is
applied:
[[(\forall T x1, ..., xn; P; Q), r]] =
r = true;
T l1 = 0;
T u1 = 0;
[[l1 and u1 calculation from P]]
while (r && l < u) {
T x1 = l1;
...
T ln = 0;
T un = 0;
[[ln and un calculation from P]]
while (r && ln < un) {
T xn = ln;
[[P ==> Q, r]]
ln = ln + 1;
}
...
l1 = l1 + 1;
}
NonExecutableQuantifierExceptionNonExecutableQuantifierException
private RacNode translateExists()
throws NonExecutableQuantifierException
[[(\exists T x1, ..., xn; P; Q), r]] =
r = false;
Collection c1 = null;
[[S, c1]] // S is the qset of P ==> Q
Iterator iter1 = c1.iterator();
while (!r && iter1.hasNext()) {
T x1 = iter1.next();
...
Collection cn = null;
[[S, cn]]
Iterator itern = cn.iterator();
while (!r && itern.hasNext()) {
T xn = itern.next();
[[P && Q, r]]
}
...
}
If the type (T) of the quantified variables is
byte, char, short,
int, or long. The following rule is
applied:
[[(\exists T x1, ..., xn; P; Q), r]] =
r = false;
T l1 = 0;
T u1 = 0;
[[l1 and u1 calculation from P]]
while (!r && l < u) {
T x1 = l1;
...
T ln = 0;
T un = 0;
[[ln and un calculation from P]]
while (!r && ln < un) {
T xn = ln;
[[P && Q, r]]
ln = ln + 1;
}
...
l1 = l1 + 1;
}
NonExecutableQuantifierExceptionNonExecutableQuantifierException
private RacNode translateSum()
throws NonExecutableQuantifierException
\sum.
The returned code has the following general form:
[[(\sum T x1, ..., xn; P; Q), r]] =
r = 0;
Collection c1 = null;
[[S1, c1]] // S1 is the qset of P for x1
Iterator iter1 = c1.iterator();
while (iter1.hasNext()) {
T x1 = iter1.next();
...
Collection cn = null;
[[Sn, cn]] // Sn is the qset of P for xn
Iterator itern = cn.iterator();
while (itern.hasNext()) {
T xn = itern.next();
boolean v1 = false;
[[P, v1]]
if (v1) {
T_Q v2 = T_init;
[[Q, v2]]
resultVar = resultVar + v2;
}
}
...
}
If the type (T) of the quantified variables is
byte, char, short,
int, or long. The following rule is
applied:
[[(\sum T x1, ..., xn; P; Q), r]] =
r = 0;
T l1 = 0;
T u1 = 0;
[[calculation of l1 and u1 from P]]
while (l1 < u1) {
T x1 = l1;
...
T ln = 0;
T un = 0;
[[calculation of ln and un from P]]
while (ln < un) {
T xn = ln;
boolean v1 = false;
[[P, v1]]
if (v1) {
T_Q v2 = T_init;
[[Q, v2]]
resultVar = resultVar + v2;
}
ln = ln + 1;
}
...
l1 = l1 + 1;
}
NonExecutableQuantifierExceptionNonExecutableQuantifierException
private RacNode translateProduct()
throws NonExecutableQuantifierException
\product.
The returned code has the following general form:
[[(\product T x1, ..., xn; P; Q), r]] =
r = 1;
Collection c1 = null;
[[S1, c1]] // S1 is the qset of P for x1
Iterator iter1 = c1.iterator();
while (iter1.hasNext()) {
T x1 = iter1.next();
...
Collection cn = null;
[[Sn, cn]] // Sn is the qset of P for xn
Iterator itern = cn.iterator();
while (itern.hasNext()) {
T xn = itern.next();
boolean v1 = false;
[[P, v1]]
if (v1) {
T_Q v2 = T_init;
[[Q, v2]]
resultVar = resultVar * v2;
}
}
...
}
If the type (T) of the quantified variables is
byte, char, short,
int, or long. The following rule is
applied:
[[(\product T x1, ..., xn; P; Q), r]] =
r = 0;
T l1 = 0;
T u1 = 0;
[[calculation of l1 and u1 from P]]
while (l1 < u1) {
T x1 = l1;
...
T ln = 0;
T un = 0;
[[calculation of ln and un from P]]
while (ln < un) {
T xn = ln;
boolean v1 = false;
[[P, v1]]
if (v1) {
T_Q v2 = T_init;
[[Q, v2]]
resultVar = resultVar * v2;
}
ln = ln + 1;
}
...
l1 = l1 + 1;
}
NonExecutableQuantifierExceptionNonExecutableQuantifierException
private RacNode translateMin()
throws NonExecutableQuantifierException
\min.
The returned code has the following general form:
[[(\min T x1, ..., xn; P; Q), r]] =
r = Integer.MAX_VALUE;
Collection c1 = null;
[[S1, c1]] // S1 is the qset of P for x1
Iterator iter1 = c1.iterator();
while (iter1.hasNext()) {
T x1 = iter1.next();
...
Collection cn = null;
[[Sn, cn]] // Sn is the qset of P for xn
Iterator itern = cn.iterator();
while (itern.hasNext()) {
T xn = itern.next();
boolean v1 = false;
[[P, v1]]
if (v1) {
T_Q v2 = T_init;
[[Q, v2]]
resultVar = Math.min(resultVar, v2);
}
}
...
}
If the type (T) of the quantified variables is
byte, char, short,
int, or long. The following rule is
applied:
[[(\max T x1, ..., xn; P; Q), r]] =
r = Integer.MAX_VALUE;
T l1 = 0;
T u1 = 0;
[[calculation of l1 and u1 from P]]
while (l1 < u1) {
T x1 = l1;
...
T ln = 0;
T un = 0;
[[calculation of ln and un from P]]
while (ln < un) {
T xn = ln;
boolean v1 = false;
[[P, v1]]
if (v1) {
T_Q v2 = T_init;
[[Q, v2]]
resultVar = Math.min(resultVar, v2);
}
ln = ln + 1;
}
...
l1 = l1 + 1;
}
NonExecutableQuantifierExceptionNonExecutableQuantifierException
private RacNode translateMax()
throws NonExecutableQuantifierException
\max.
The returned code has the following general form:
[[(\max T x1, ..., xn; P; Q), r]] =
r = Integer.MIN_VALUE;
Collection c1 = null;
[[S1, c1]] // S1 is the qset of P for x1
Iterator iter1 = c1.iterator();
while (iter1.hasNext()) {
T x1 = iter1.next();
...
Collection cn = null;
[[Sn, cn]] // Sn is the qset of P for xn
Iterator itern = cn.iterator();
while (itern.hasNext()) {
T xn = itern.next();
boolean v1 = false;
[[P, v1]]
if (v1) {
T_Q v2 = T_init;
[[Q, v2]]
resultVar = Math.max(resultVar, v2);
}
}
...
}
If the type (T) of the quantified variables is
byte, char, short,
int, or long. The following rule is
applied:
[[(\max T x1, ..., xn; P; Q), r]] =
r = Integer.MIN_VALUE;
T l1 = 0;
T u1 = 0;
[[calculation of l1 and u1 from P]]
while (l1 < u1) {
T x1 = l1;
...
T ln = 0;
T un = 0;
[[calculation of ln and un from P]]
while (ln < un) {
T xn = ln;
boolean v1 = false;
[[P, v1]]
if (v1) {
T_Q v2 = T_init;
[[Q, v2]]
resultVar = Math.max(resultVar, v2);
}
ln = ln + 1;
}
...
l1 = l1 + 1;
}
NonExecutableQuantifierExceptionNonExecutableQuantifierException
private RacNode translateNumOf()
throws NonExecutableQuantifierException
\num_of.
The returned code has the following general form:
[[(\num_of T x1, ..., xn; P; Q), r]] =
r = 0;
Collection c1 = null;
[[S1, c1]] // S1 is the qset of P for x1
Iterator iter1 = c1.iterator();
while (iter1.hasNext()) {
T x1 = iter1.next();
...
Collection cn = null;
[[Sn, cn]] // Sn is the qset of P for xn
Iterator itern = cn.iterator();
while (itern.hasNext()) {
T xn = itern.next();
boolean v1 = false;
[[P, v1]]
boolean v2 = false;
[[Q, v2]]
if (v1 && v2) {
resultVar++;
}
}
...
}
If the type (T) of the quantified variables is
byte, char, short,
int, or long. The following rule is
applied:
[[(\num_of T x1, ..., xn; P; Q), r]] =
r = 0;
T l1 = 0;
T u1 = 0;
[[calculation of l1 and u1 from P]]
while (l1 < u1) {
T x1 = l1;
...
T ln = 0;
T un = 0;
[[calculation of ln and un from P]]
while (ln < un) {
T xn = ln;
boolean v1 = false;
[[P, v1]]
boolean v2 = false;
[[Q, v2]]
if (v1 && v2) {
resultVar++;
}
ln = ln + 1;
}
...
l1 = l1 + 1;
}
NonExecutableQuantifierExceptionNonExecutableQuantifierException
private RacNode transForAllOrExists()
throws NonExecutableQuantifierException
translateForAll
and translateExists for the structure of the
returned code.
requires quantiExp.isForAll() || quantiExp.isExists(); ensures \result != null;
NonExecutableQuantifierExceptiontranslateForAll(),
translateExists()private JExpression rangePredicate()
requires quantiExp.isForAll() || quantiExp.isExists(); ensures (* \result maybe null *);
transForAllOrExists()private static JExpression unwrapJmlExpression(JExpression expr)
private RacNode transSumOrProduct()
throws NonExecutableQuantifierException
\sum
or \product.
requires quantiExp.isSum() || quantiExp.isProduct();
NonExecutableQuantifierExceptiontranslateProduct(),
translateSum()
private String applySumOrProduct(String strResultVar,
String strOptr,
String strV2,
CType vType)
private RacNode transMinOrMax()
throws NonExecutableQuantifierException
\min
or \max.
requires quantiExp.isMin() || quantiExp.isMax();
NonExecutableQuantifierExceptiontranslateMax(),
translateMin()
public RacNode generateLoop(RacNode body)
throws NonExecutableQuantifierException
{
T l = 0;
T u = 0;
[[eval of l and u from predicate part]]
while (l < u) {
T x = l;
result
l = l + 1;
}
}
where x is the quantified variable.
body - code to be executed as the loop body
NonExecutableQuantifierException - if not executable.
protected abstract RacNode generateLoop(JVariableDefinition varDef,
JExpression qexpr,
String cond,
RacNode result)
throws NonExecutableQuantifierException
varDef - quantified variableqexpr - target expression for interval calculation (i.e.,
normally, the predicate part of the quantified
expression)cond - additional condition to be conjoined (&&)
to the loop condition; null for no
conjoinable condition.result - code for evaluating expression part (or inner loop)
NonExecutableQuantifierExceptionNonExecutableQuantifierException
protected RacNode transExpression(JExpression expr,
String var)
expr and
storing the result to the variable var.
As a special case, returns var = true;
if expr is null.
|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||