escjava.vcGeneration
Class VcGenerator

java.lang.Object
  escjava.vcGeneration.VcGenerator

public class VcGenerator

extends java.lang.Object

Field Summary

private boolean	computationDone
private TFunction	currentParent This attribute is used by the next function to save the current parent of the node we may create.
private boolean	firstNotSkipped
private TNode	newRootNode
private java.lang.StringBuffer	oldDot
private ASTNode	oldRootNode
private ProverType	prover README : This class is an interface to the vc generation suite (this is done this way to be able to put all the other classes in a new package.)

Constructor Summary

VcGenerator(ProverType p, ASTNode e, boolean err, boolean warn, boolean info, boolean colors)

Method Summary

private void	generateIfpTree(ASTNode n, boolean dot) The main goal of this method is to translate the gc tree (which is still independant from simplify) to a new tree (classes of this new tree are in escjava/vcGeneration which is, by far, easier to manipulate that the one which is given here (parameter e).
private static java.lang.String	getNameASTNode(ASTNode e) Utility method for creating dot representation of gc tree
void	getProof(java.io.Writer out, java.lang.String proofName)
java.lang.String	old2Dot()
void	printInfo() Debugging purpose only.
java.lang.String	toDot()

Methods inherited from class java.lang.Object

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

Field Detail

prover

private ProverType prover

README : This class is an interface to the vc generation suite (this is done this way to be able to put all the other classes in a new package.) Usage : You have to supply the root node of the vc tree you want to translate. Then you can call any of the public finction to get what you want. It has been designed in a way that makes sure we won't do the work two times. I.e., if you call the constructor and never call old2Dot(), we never compute the dot file. Most of the time (ie except for development and debugging), you have to do : 1/ vcg = new VcGenerator(p,e,..); // p is the prover type and e is the root node of the vc tree 2/ vcg.getProof(vc); // return, as a string, proof script for the given vc

oldRootNode

private ASTNode oldRootNode

newRootNode

private TNode newRootNode

oldDot

private java.lang.StringBuffer oldDot

computationDone

private boolean computationDone

currentParent

private TFunction currentParent

This attribute is used by the next function to save the current parent of the node we may create. Before any call to generateIfpTree, and after the last call has returned this field is always null. This is bizarre, but avoids to add a parameter to this function and makes the code more concise.

firstNotSkipped

private boolean firstNotSkipped

Constructor Detail

VcGenerator

public VcGenerator(ProverType p,
                   ASTNode e,
                   boolean err,
                   boolean warn,
                   boolean info,
                   boolean colors)

Parameters:

e - the root node of the gc tree.

Method Detail

getProof

public void getProof(java.io.Writer out,
                     java.lang.String proofName)
              throws java.io.IOException

Throws:

java.io.IOException

old2Dot

public java.lang.String old2Dot()

toDot

public java.lang.String toDot()
                       throws java.io.IOException

Throws:

java.io.IOException

generateIfpTree

private void generateIfpTree(ASTNode n,
                             boolean dot)

The main goal of this method is to translate the gc tree (which is still independant from simplify) to a new tree (classes of this new tree are in escjava/vcGeneration which is, by far, easier to manipulate that the one which is given here (parameter e). The code is divided in this way : 1/ declarations 2/ switch on the type of the node currently looked at 3/ a/ depending on the type, create a new node for the translation of the tree b/ if dot output is asked (ie parameter dot != null), do the job 4/ call the method on the sons of the current node.

Parameters:

dot - if true, generate the dot representation of the old tree.

getNameASTNode

private static java.lang.String getNameASTNode(ASTNode e)

Utility method for creating dot representation of gc tree

Returns:

transform escjava.prover.sammy to sammy, ie escjava.x.y to y

printInfo

public void printInfo()

Debugging purpose only.