Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

## escjava.translate
Class VcToStringPvs

    java.lang.Object
      escjava.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)

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

The ESC/Java2 Project Homepage