escjava.vcGeneration.sammy
Class SammyProver

java.lang.Object
  escjava.vcGeneration.ProverType
      escjava.vcGeneration.sammy.SammyProver

public class SammyProver

extends ProverType

Constructor Summary

SammyProver()

Method Summary

Expr	addTypeInfo(InitialState initState, Expr tree) This method is used by untyped prover logics to add typing predicates to the supplied VC term.
void	generateDeclarations(java.io.Writer s, java.util.HashMap variablesName) This methods generates the declarations for a specified prover.
void	getProof(java.io.Writer out, java.lang.String proofName, 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
java.lang.String	getTypeInfo(TypeInfo caller) TypeInfo represents a single translation/mapping between an old type name and the targeted prover type name.
java.lang.String	getVariableInfo(VariableInfo caller) VariableInfo represents a single translation/mapping between an old variable name and the targeted prover variable name.
void	init() Used to initialise the variable and type maps.
java.lang.String	labelRename(java.lang.String label) This method is used to provide prover based renaming of the VC file name.
TNode	rewrite(TNode tree) This method allows an ESC/Java VC term to be simplified before it is translated to the target prover.
private void	sammyRename(TypeInfo caller)
private void	sammyRename(VariableInfo caller)
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

Constructor Detail

SammyProver

public SammyProver()

Method Detail

labelRename

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

Description copied from class: ProverType

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

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

Description copied from class: ProverType

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

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)

Description copied from class: ProverType

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.

Specified by:

getVariableInfo in class ProverType

Parameters:

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

Returns:

sammyRename

private void sammyRename(VariableInfo caller)

getTypeInfo

public java.lang.String getTypeInfo(TypeInfo caller)

Description copied from class: ProverType

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.

Specified by:

getTypeInfo in class ProverType

Parameters:

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

Returns:

sammyRename

private void sammyRename(TypeInfo caller)

init

public void init()

Description copied from class: ProverType

Used to initialise the variable and type maps.

Specified by:

init in class ProverType

addTypeInfo

public Expr addTypeInfo(InitialState initState,
                        Expr tree)

Description copied from class: ProverType

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.

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)

Description copied from class: ProverType

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

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 variablesName)
                          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.

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

Throws:

java.io.IOException