escjava.vcGeneration
Class TNode

java.lang.Object
  escjava.vcGeneration.TNode

Direct Known Subclasses:

TFunction, TVariable

public abstract class TNode

extends java.lang.Object

Field Summary

static TypeInfo	_boolean
static TypeInfo	_char
static TypeInfo	_double
static TypeInfo	_DOUBLETYPE
static TypeInfo	_Field
static TypeInfo	_float
static TypeInfo	_integer
static TypeInfo	_INTTYPE
static TypeInfo	_Path
static TypeInfo	_Reference We add some types that we know will be used to avoid looking at the map typesName when we want to add it.
static TypeInfo	_String
static TypeInfo	_Time
static TypeInfo	_Type
protected static int	counter
protected static java.io.PrintStream	dotPs
protected int	id
protected boolean	isroot
(package private) java.lang.String	label
protected static int	lastType
TFunction	parent
static ProverType	prover
TypeInfo	type
protected static boolean	typeProofSet
static java.util.HashMap	typesName map containing all the types used in the proof.
protected static java.util.HashMap	variablesName map containing the variables names When the tree is created, old name are entered as keys with a new VariableInfo(oldName, type) associated as value.

Constructor Summary

TNode()

Method Summary

abstract void	accept(TVisitor v)
static VariableInfo	addName(java.lang.String oldName, java.lang.String type)
static VariableInfo	addName(java.lang.String oldName, java.lang.String type, java.lang.String def) This function add variable to the global map name.
static TypeInfo	addType(java.lang.String oldType)
static TypeInfo	addType(java.lang.String oldType, java.lang.String def) This function add type to the global map .
protected java.lang.String	dotId() dot id which is unique because of adding 'id' to the name of the node
protected void	generateDeclarations(java.io.Writer s, ProverType p)
protected java.lang.String	getShortName()
java.lang.String	getType() return the type of the node according to the type of proof asked or "?"
TypeInfo	getTypeInfo() Return the typeInfo associated with this node.
(package private) VariableInfo	getVariableInfo() return the VariableInfo object associated of the caller which must be an instance of TName.
static VariableInfo	getVariableInfo(java.lang.String name) return the VariableInfo object associated with this name
static void	init(ProverType prover)
static void	printInfo()
protected void	setType(java.lang.String s, boolean sure) Add the type if not present to the global map of type and fill the correct field with it.
protected void	setType(TypeInfo type, boolean sure)
java.lang.String	toString()
protected abstract void	typeTree()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

dotPs

protected static java.io.PrintStream dotPs

id

protected int id

counter

protected static int counter

isroot

protected boolean isroot

type

public TypeInfo type

lastType

protected static int lastType

typeProofSet

protected static boolean typeProofSet

parent

public TFunction parent

label

java.lang.String label

variablesName

protected static java.util.HashMap variablesName

map containing the variables names When the tree is created, old name are entered as keys with a new VariableInfo(oldName, type) associated as value. When the vc are generated, each time a variable is looked at, we look at this map. We look into the VariableInfo object associated. If the renaming hasn't been done into this object, we do it. If present, we use the already existing name. Thus we will only rename one time and use previous value for next acccess. It handles multiple renaming because each VariableInfo object contains multiples fields for renaming (take a look at it).

typesName

public static java.util.HashMap typesName

map containing all the types used in the proof. After calling typeTree, each node has his TypeInfo field not null. It points on a TypeInfo object which is a value of this HashMap. Each TypeInfo object contains the old type, the pvs corresponding type, and the sammy corresponding type. The old type can be {reference, integer, boolean, type}. The tree is typechecked after call to SetOutputType and this map is filled with only the type asked. Ie if you call setOutputType("unsortedPvs"), the tree will be typed with the old type and the types for the unsorted logic of pvs. If you make another call to setOutputType, it will add type the tree for the new tree etc...

_Reference

public static TypeInfo _Reference

We add some types that we know will be used to avoid looking at the map typesName when we want to add it.

_Type

public static TypeInfo _Type

_DOUBLETYPE

public static TypeInfo _DOUBLETYPE

_boolean

public static TypeInfo _boolean

_char

public static TypeInfo _char

_double

public static TypeInfo _double

_Field

public static TypeInfo _Field

_INTTYPE

public static TypeInfo _INTTYPE

_integer

public static TypeInfo _integer

_float

public static TypeInfo _float

_String

public static TypeInfo _String

_Time

public static TypeInfo _Time

_Path

public static TypeInfo _Path

prover

public static ProverType prover

Constructor Detail

TNode

public TNode()

Method Detail

init

public static void init(ProverType prover)

generateDeclarations

protected void generateDeclarations(java.io.Writer s,
                                    ProverType p)
                             throws java.io.IOException

Throws:

java.io.IOException

addName

public static VariableInfo addName(java.lang.String oldName,
                                   java.lang.String type,
                                   java.lang.String def)

This function add variable to the global map name.

Parameters:

oldName - the old name.

type - the type of the variable which has been infered from the old tree.

Returns:

the VariableInfo object representing this variables name

addName

public static VariableInfo addName(java.lang.String oldName,
                                   java.lang.String type)

getVariableInfo

public static VariableInfo getVariableInfo(java.lang.String name)

return the VariableInfo object associated with this name

getVariableInfo

VariableInfo getVariableInfo()

return the VariableInfo object associated of the caller which must be an instance of TName.

addType

public static TypeInfo addType(java.lang.String oldType,
                               java.lang.String def)

This function add type to the global map .

Returns:

the node pointing on that variable (can already exist if this add is useless, in this case we return the previous TypeInfo representing this type).

addType

public static TypeInfo addType(java.lang.String oldType)

dotId

protected java.lang.String dotId()

dot id which is unique because of adding 'id' to the name of the node

getShortName

protected java.lang.String getShortName()

typeTree

protected abstract void typeTree()

setType

protected void setType(java.lang.String s,
                       boolean sure)

Add the type if not present to the global map of type and fill the correct field with it.

setType

protected void setType(TypeInfo type,
                       boolean sure)

getType

public java.lang.String getType()

return the type of the node according to the type of proof asked or "?" if type isn't known.

getTypeInfo

public TypeInfo getTypeInfo()

Return the typeInfo associated with this node. It can just be the 'type' field for non instance of TName. Or in the case of TName node, we retrieve it in the global map.

toString

public java.lang.String toString()

accept

public abstract void accept(TVisitor v)
                     throws java.io.IOException

Throws:

java.io.IOException

printInfo

public static void printInfo()