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 VcToStringPvs

java.lang.Object
  extended byescjava.translate.VcToStringPvs

public class VcToStringPvs
extends java.lang.Object


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

listOfDecl

public static java.util.Vector listOfDecl

listOfDeclAdd

public static java.util.Vector listOfDeclAdd

listOfDeclFun

public static java.util.Vector listOfDeclFun

listOfDeclFunNbParam

public static java.util.Vector listOfDeclFunNbParam

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

VcToStringPvs

protected VcToStringPvs()
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)

isEven

protected boolean isEven(int i)

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.


add2Decl

private static int add2Decl(java.lang.String s)

add2DeclFun

private static int add2DeclFun(java.lang.String s,
                               int nbParameters)

replaceBadChar

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

The ESC/Java2 Project Homepage