escjava.vcGeneration.xml
Class XmlProver

java.lang.Object
  escjava.vcGeneration.ProverType
      escjava.vcGeneration.xml.XmlProver

public class XmlProver

extends ProverType

This class provides a simple mechanism by which new prover plugins to the VC generator may be implemented.

All one has to do is to provide a stylesheet within the escjava.vcGeneration.xml package or located on the system property search path XMLPROVERPATH for the targeted prover (eg. simplify.xslt). This stylesheet transforms XML terms, conforming to the DTD defined by escjava/vcGeneration/xml/xmlprover.dtd (as we are compiling with JDK 1.4 this can not be checked!!), into terms of the targeted prover.

Calling ESC/Java with the nvcg option xml.<prover> enables the target prover VC terms to be generated (eg. -nvcp xml.simplify will enable VC's for the targeted prover to be generated using the stylesheet escjava/vcGeneration/xml/simplify.xslt - supplied by default with ESC/Java).

Using this XML based prover interface should make it easier to build and debug new prover interfaces to the VC generator.

Author:

Carl Pulley

Field Summary

private org.w3c.dom.Document	dom
private org.w3c.dom.Element	node
private java.lang.String	stylesheet This field defines the prover based stylesheet that will be used to translate our generated XML VC terms with calls to getProof(java.io.Writer, java.lang.String, escjava.vcGeneration.TNode)
private TXmlVisitor	visitor

Constructor Summary

XmlProver()

Method Summary

Expr	addTypeInfo(InitialState initState, Expr tree) At this stage, we do not know if the target prover is typed or not.
void	generateDeclarations(java.io.Writer s, java.util.HashMap variableNames) This methods generates the declarations for a specified prover.
void	getProof(java.io.Writer out, java.lang.String proofName, TNode term) Here we ensure that the resulting XML term is suitable for writing to an output file.
java.lang.String	getTypeInfo(TypeInfo caller) Since our XML mapping of type names is the identity one, we may simply return the old type name here.
java.lang.String	getVariableInfo(VariableInfo caller) Since our XML mapping of variable names is the identity one, we may simply return the old variable name here.
void	init() Initialization simply defines an identity map on the known types and names.
java.lang.String	labelRename(java.lang.String label) Our DTD specifies that term names are of type CDATA.
TNode	rewrite(TNode tree) All rewriting is handled by the prover based stylesheet, so we do nothing here.
void	setStyleSheet(java.lang.String stylesheet) This method only allows the field stylesheet to be set once.
TVisitor	visitor(java.io.Writer out) The visitor pattern is used to map an ESC/Java VC term to a prover term.

Methods inherited from class escjava.vcGeneration.ProverType

generateDeclarations, generateTerm

Methods inherited from class java.lang.Object

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

Field Detail

stylesheet

private java.lang.String stylesheet

This field defines the prover based stylesheet that will be used to translate our generated XML VC terms with calls to getProof(java.io.Writer, java.lang.String, escjava.vcGeneration.TNode)

visitor

private TXmlVisitor visitor

dom

private org.w3c.dom.Document dom

node

private org.w3c.dom.Element node

Constructor Detail

XmlProver

public XmlProver()

Method Detail

setStyleSheet

public void setStyleSheet(java.lang.String stylesheet)

This method only allows the field stylesheet to be set once.

Parameters:

stylesheet - target prover's stylesheet

labelRename

public java.lang.String labelRename(java.lang.String label)

Our DTD specifies that term names are of type CDATA. Hence this method is an identity renaming. The prover based stylesheet may perform a renaming of these term names.

Specified by:

labelRename in class ProverType

Parameters:

label - The method based label that needs to be renamed.

Returns:

The renamed method label.

visitor

public TVisitor visitor(java.io.Writer out)
                 throws java.io.IOException

Description copied from class: ProverType

The visitor pattern is used to map an ESC/Java VC term to a prover term.

vcGenerator uses this method to perform the mapping.

A typical implementation of this method will also need to extend the TVisitor class.

Specified by:

visitor in class ProverType

Parameters:

out - The stream to which we should write our visitor trail

Throws:

java.io.IOException

getProof

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

Here we ensure that the resulting XML term is suitable for writing to an output file.

After generating our raw XML term conforming to escjava/vcGeneration/xml/xmlprover.dtd (this can not be checked with JDK 1.4!!), we convert it to a prover VC term using the stylesheet specified by stylesheet.

The search rules for the stylesheet to be used are as follows (here we assume that <stylesheet> is the value of the field stylesheet):

• we first look in escjava/vcGeneration/xml for a file named <stylesheet>.xslt
• next we search a :-separated list of directories specified in the system property XMLPROVERPATH for a file named <stylesheet>.xslt. XMLPROVERPATH has a default value of '.'

Specified by:

getProof in class ProverType

Parameters:

proofName - name to be given to the proof assertion (eg. lemma or theorem)

Throws:

java.io.IOException

getVariableInfo

public java.lang.String getVariableInfo(VariableInfo caller)

Since our XML mapping of variable names is the identity one, we may simply return the old variable name here.

Specified by:

getVariableInfo in class ProverType

Parameters:

caller - The specific variable name translation/mapplet we are to use.

Returns:

getTypeInfo

public java.lang.String getTypeInfo(TypeInfo caller)

Since our XML mapping of type names is the identity one, we may simply return the old type name here.

Specified by:

getTypeInfo in class ProverType

Parameters:

caller - The specific type name translation/mapplet we are to use.

Returns:

init

public void init()

Initialization simply defines an identity map on the known types and names.

Specified by:

init in class ProverType

addTypeInfo

public Expr addTypeInfo(InitialState initState,
                        Expr tree)

At this stage, we do not know if the target prover is typed or not. Hence, we add the typing predicate to the VC term. The prover based stylesheet may eliminate this typing predicate.

Specified by:

addTypeInfo in class ProverType

Parameters:

tree - the VC term to which typing predicates may need to be added.

Returns:

rewrite

public TNode rewrite(TNode tree)

All rewriting is handled by the prover based stylesheet, so we do nothing here.

Specified by:

rewrite in class ProverType

Parameters:

tree - a VC term to be simplified

generateDeclarations

public void generateDeclarations(java.io.Writer s,
                                 java.util.HashMap variableNames)
                          throws java.io.IOException

Description copied from class: ProverType

This methods generates the declarations for a specified prover.

Specified by:

generateDeclarations in class ProverType

Parameters:

s - The buffer to which we want to generate the declarations to.

variableNames - The hashmap containing all the variables, usually TNode.variablesName.

Throws:

java.io.IOException