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

escjava.translate
Class VcToString

java.lang.Object
  extended byescjava.translate.VcToString

public class VcToString
extends java.lang.Object


Field Summary
protected  boolean insideNoPats
          insideNoPats is really a parameter to * printTerm.
protected static java.util.Hashtable integralPrintNames
           
protected static long MaxIntegral
           
protected static java.lang.Long maxThreshold
           
protected static java.lang.Long minThreshold
           
protected  DefPredVec preds
           
static int quantifierNumber
           
protected  Set stringLiterals
           
protected  Set symbols
           
static int termNumber
           
static int variableNumber
           
 
Constructor Summary
protected VcToString()
           
 
Method Summary
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  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 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

quantifierNumber

public static int quantifierNumber

termNumber

public static int termNumber

variableNumber

public static int variableNumber

symbols

protected Set symbols

stringLiterals

protected Set stringLiterals

integralPrintNames

protected static java.util.Hashtable integralPrintNames

preds

protected DefPredVec preds

insideNoPats

protected boolean insideNoPats
insideNoPats is really a parameter to * printTerm.


MaxIntegral

protected static final long MaxIntegral
See Also:
Constant Field Values

minThreshold

protected static final java.lang.Long minThreshold

maxThreshold

protected static final java.lang.Long maxThreshold
Constructor Detail

VcToString

protected VcToString()
Method Detail

resetTypeSpecific

public static void resetTypeSpecific()
Resets any type-specific information that is accumulated through calls to computeTypeSpecific.


computeTypeSpecific

public static void computeTypeSpecific(Expr e,
                                       java.io.PrintStream to)
Prints 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.


compute

public static void compute(Expr e,
                           java.io.PrintStream to)
Prints 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.


computePC

public static void computePC(Expr e,
                             java.io.PrintStream to)

vc2Term

protected java.lang.String vc2Term(Expr e,
                                   java.util.Hashtable subst)

printDefpreds

protected void printDefpreds(java.io.PrintStream to,
                             DefPredVec preds)

getDefpreds

protected DefPredVec getDefpreds(Expr e)

getDefpredsHelper

protected void getDefpredsHelper(Expr e)

distinctSymbols

protected void distinctSymbols(java.io.PrintStream to)

stringLiteralAssumptions

protected void stringLiteralAssumptions(java.io.PrintStream to)

printFormula

protected void printFormula(java.io.PrintStream out,
                            Expr e)

printFormula

protected void printFormula(java.io.PrintStream out,
                            java.util.Hashtable subst,
                            Expr e)

reallyPrintFormula

protected void reallyPrintFormula(java.io.PrintStream out,
                                  java.util.Hashtable subst,
                                  Expr e)

printTerm

protected void printTerm(java.io.PrintStream out,
                         java.util.Hashtable subst,
                         Expr e)

printDttfsa

protected void printDttfsa(java.io.PrintStream out,
                           java.util.Hashtable subst,
                           NaryExpr ne)

printVarDecl

protected void printVarDecl(java.io.PrintStream out,
                            GenericVarDecl decl)

integralPrintName

protected java.lang.String integralPrintName(long n)
* Convert an integral # into its printname according to the rules * of ESCJ 23b, part 9.


integralPrintNameOrder

protected void integralPrintNameOrder(java.io.PrintStream ps)
Generates the inequalities that compare the integral literals that were replaced in integralPrintName by symbolic names.


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

The ESC/Java2 Project Homepage