escjava.vcGeneration
Class ProverType

java.lang.Object
  escjava.vcGeneration.ProverType

Direct Known Subclasses:

CoqProver, PvsProver, SammyProver, SimplifyProver, XmlProver

public abstract class ProverType

extends java.lang.Object

The interface to be implemented when adding a new prover to ESC/Java.

Any implementing class should be placed in an appropriately named subpackage of the escjava.vcGeneration package. In addition, the implementing classes name should be be a capitilized version of the subpackages name with all dots removed:

For example, for subpackage pvs.unsorted, the implementing classes name should be PvsUnsortedProver. This restriction exists so that new provers may be generically loaded and created at runtime within the escjava.Main class and different provers may be easily identified within an editing environment.

With this interface, even Simplify is treated as just another prover.

The following terminology is used consistently throughout the vcGenerator package:

• by prover we shall mean a logic and an underlying proof engine
• by proof we shall mean an ESC/Java VC term (targeted to some prover).

Constructor Summary

ProverType()

Method Summary

abstract Expr	addTypeInfo(InitialState initState, Expr tree) This method is used by untyped prover logics to add typing predicates to the supplied VC term.
protected abstract void	generateDeclarations(java.io.Writer out, java.util.HashMap variablesName) This methods generates the declarations for a specified prover.
void	generateDeclarations(java.io.Writer out, TNode term) This convenience method generates the declarations for a given term.
void	generateTerm(java.io.Writer out, TNode term) This convenience method uses the visitor pattern to generate a prover specific term.
abstract void	getProof(java.io.Writer out, java.lang.String name, TNode term) This method allows a VC term (generated by using the visitor pattern), for example, to: be wrapped up as a prover assertion (eg. a lemma or theorem for the prover) universally quantify all free variables in the VC term
abstract java.lang.String	getTypeInfo(TypeInfo caller) TypeInfo represents a single translation/mapping between an old type name and the targeted prover type name.
abstract java.lang.String	getVariableInfo(VariableInfo caller) VariableInfo represents a single translation/mapping between an old variable name and the targeted prover variable name.
abstract void	init() Used to initialise the variable and type maps.
abstract java.lang.String	labelRename(java.lang.String label) This method is used to provide prover based renaming of the VC file name.
abstract TNode	rewrite(TNode tree) This method allows an ESC/Java VC term to be simplified before it is translated to the target prover.
protected abstract 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 java.lang.Object

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

Constructor Detail

ProverType

public ProverType()

Method Detail

labelRename

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

This method is used to provide prover based renaming of the VC file name.

Parameters:

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

Returns:

The renamed method label.

visitor

protected abstract TVisitor visitor(java.io.Writer out)
                             throws java.io.IOException

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.

Parameters:

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

Throws:

java.io.IOException

getProof

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

This method allows a VC term (generated by using the visitor pattern), for example, to:

• be wrapped up as a prover assertion (eg. a lemma or theorem for the prover)
• universally quantify all free variables in the VC term

Parameters:

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

Throws:

java.io.IOException

getVariableInfo

public abstract java.lang.String getVariableInfo(VariableInfo caller)

VariableInfo represents a single translation/mapping between an old variable name and the targeted prover variable name.

This method returns the target prover's variable name given one of these translations/mapplets.

Parameters:

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

Returns:

getTypeInfo

public abstract java.lang.String getTypeInfo(TypeInfo caller)

TypeInfo represents a single translation/mapping between an old type name and the targeted prover type name.

This method returns the target prover's type name given one of these translations/mapplets.

Parameters:

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

Returns:

init

public abstract void init()

Used to initialise the variable and type maps.

addTypeInfo

public abstract Expr addTypeInfo(InitialState initState,
                                 Expr tree)

This method is used by untyped prover logics to add typing predicates to the supplied VC term.

Typed prover logics do not need to do anything here.

Parameters:

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

Returns:

rewrite

public abstract TNode rewrite(TNode tree)

This method allows an ESC/Java VC term to be simplified before it is translated to the target prover.

Parameters:

tree - a VC term to be simplified

generateDeclarations

protected abstract void generateDeclarations(java.io.Writer out,
                                             java.util.HashMap variablesName)
                                      throws java.io.IOException

This methods generates the declarations for a specified prover.

Parameters:

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

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

Throws:

java.io.IOException

generateDeclarations

public final void generateDeclarations(java.io.Writer out,
                                       TNode term)
                                throws java.io.IOException

This convenience method generates the declarations for a given term. These declarations are written to the specified stream.

Parameters:

out - the stream to which the generated declarations are written

term - the term from which the declarations are to be obtained

Throws:

java.io.IOException

generateTerm

public final void generateTerm(java.io.Writer out,
                               TNode term)
                        throws java.io.IOException

This convenience method uses the visitor pattern to generate a prover specific term. Used by VcGenerator.getProof(Writer, String).

Parameters:

out - the stream to which the generated term is to be written

term - the term we wish to convert

Throws:

java.io.IOException