|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectescjava.translate.VcToStringPvs
Field Summary | |
protected boolean |
insideNoPats
insideNoPats is really a parameter to *
printTerm . |
protected static java.util.Hashtable |
integralPrintNames
|
static java.util.Vector |
listOfDecl
|
static java.util.Vector |
listOfDeclAdd
|
static java.util.Vector |
listOfDeclFun
|
static java.util.Vector |
listOfDeclFunNbParam
|
protected static long |
MaxIntegral
|
protected static java.lang.Long |
maxThreshold
|
protected static java.lang.Long |
minThreshold
|
protected DefPredVec |
preds
|
protected Set |
stringLiterals
|
protected Set |
symbols
|
Constructor Summary | |
protected |
VcToStringPvs()
|
Method Summary | |
private static int |
add2Decl(java.lang.String s)
|
private static int |
add2DeclFun(java.lang.String s,
int nbParameters)
|
static void |
compute(Expr e,
java.io.PrintStream to)
Prints e as a verification-condition string to
to . |
static void |
computePC(Expr e,
java.io.PrintStream to)
|
static void |
computeTypeSpecific(Expr e,
java.io.PrintStream to)
Prints e as a simple-expression string to to .
|
protected void |
distinctSymbols(java.io.PrintStream to)
|
protected DefPredVec |
getDefpreds(Expr e)
|
protected void |
getDefpredsHelper(Expr e)
|
protected java.lang.String |
integralPrintName(long n)
* Convert an integral # into its printname according to the rules * of ESCJ 23b, part 9. |
protected void |
integralPrintNameOrder(java.io.PrintStream ps)
Generates the inequalities that compare the integral literals that were replaced in integralPrintName by symbolic
names. |
protected boolean |
isEven(int i)
|
protected void |
printDefpreds(java.io.PrintStream to,
DefPredVec preds)
|
protected void |
printDttfsa(java.io.PrintStream out,
java.util.Hashtable subst,
NaryExpr ne)
|
protected void |
printFormula(java.io.PrintStream out,
Expr e)
|
protected void |
printFormula(java.io.PrintStream out,
java.util.Hashtable subst,
Expr e)
|
protected void |
printTerm(java.io.PrintStream out,
java.util.Hashtable subst,
Expr e)
|
protected void |
printVarDecl(java.io.PrintStream out,
GenericVarDecl decl)
|
protected void |
reallyPrintFormula(java.io.PrintStream out,
java.util.Hashtable subst,
Expr e)
|
static java.lang.String |
replaceBadChar(java.lang.String s)
|
static void |
resetTypeSpecific()
Resets any type-specific information that is accumulated through calls to computeTypeSpecific . |
protected void |
stringLiteralAssumptions(java.io.PrintStream to)
|
protected java.lang.String |
vc2Term(Expr e,
java.util.Hashtable subst)
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
public static java.util.Vector listOfDecl
public static java.util.Vector listOfDeclAdd
public static java.util.Vector listOfDeclFun
public static java.util.Vector listOfDeclFunNbParam
protected Set symbols
protected Set stringLiterals
protected static java.util.Hashtable integralPrintNames
protected DefPredVec preds
protected boolean insideNoPats
insideNoPats
is really a parameter to *
printTerm
.
protected static final long MaxIntegral
protected static final java.lang.Long minThreshold
protected static final java.lang.Long maxThreshold
Constructor Detail |
protected VcToStringPvs()
Method Detail |
public static void resetTypeSpecific()
computeTypeSpecific
.
public static void computeTypeSpecific(Expr e, java.io.PrintStream to)
e
as a simple-expression string to to
.
Any symbolic names created for integral literals in e
are
added to a static place (variable integralPrintNames
) so
that successive calls to compute
can produce properties
about these names.
public static void compute(Expr e, java.io.PrintStream to)
e
as a verification-condition string to
to
. Any symbolic names of integral literals stored by the
most recent call to computeTypeBackPred
, if any, will be
considered when producing properties about such symbolic literals.
public static void computePC(Expr e, java.io.PrintStream to)
protected java.lang.String vc2Term(Expr e, java.util.Hashtable subst)
protected void printDefpreds(java.io.PrintStream to, DefPredVec preds)
protected DefPredVec getDefpreds(Expr e)
protected void getDefpredsHelper(Expr e)
protected void distinctSymbols(java.io.PrintStream to)
protected void stringLiteralAssumptions(java.io.PrintStream to)
protected void printFormula(java.io.PrintStream out, Expr e)
protected void printFormula(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
protected void reallyPrintFormula(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
protected boolean isEven(int i)
protected void printTerm(java.io.PrintStream out, java.util.Hashtable subst, Expr e)
protected void printDttfsa(java.io.PrintStream out, java.util.Hashtable subst, NaryExpr ne)
protected void printVarDecl(java.io.PrintStream out, GenericVarDecl decl)
protected java.lang.String integralPrintName(long n)
protected void integralPrintNameOrder(java.io.PrintStream ps)
integralPrintName
by symbolic
names.
private static int add2Decl(java.lang.String s)
private static int add2DeclFun(java.lang.String s, int nbParameters)
public static java.lang.String replaceBadChar(java.lang.String s)
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |