escjava.vcGeneration.coq
Class CoqProver

java.lang.Object
  escjava.vcGeneration.ProverType
      escjava.vcGeneration.coq.CoqProver

public class CoqProver

extends ProverType

This class is an implementations of the interface ProverType. In order to handle the Coq theorem prover.

Version:

14/11/2005

Author:

J. Charles, based on the work of C. Hurlin and C.Pulley

Constructor Summary

CoqProver()

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.
private void	coqRename(TypeInfo t) Rename the type, ie. the name TypeInfo.old to a proper Coq name in the variable TypeInfo.def
private void	coqRename(VariableInfo vi) Rename the variable, ie. the name VariableInfo.old to a proper Coq name in the variable VariableInfo.def.
void	generateDeclarations(java.io.Writer s, java.util.HashMap variablesNames) Generates the declarations for the forall construct in the Coq Fashion, i.e.
private void	generatePureMethodsDeclarations(java.io.Writer s) Generates the pure methods declarations
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 vi) Returns a valid Coq name corresponding to the given VariableInfo.
void	init() Defines predefined Coq types, and some predefined variables (ecReturn, ecThrow and XRES).
java.lang.String	labelRename(java.lang.String label) This method is used to provide prover based renaming of the VC file name.
java.lang.String	removeInvalidChar(java.lang.String name) Removes the invalid characters in Coq for a given String.
TNode	rewrite(TNode tree) Tries to simplify the given tree using the class TProofTyperVisitor.
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

CoqProver

public CoqProver()

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

Returns:

an instance of the class TCoqVisitor.

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)

Returns:

the Coq vernacular file representing the proof.

Throws:

java.io.IOException

generatePureMethodsDeclarations

private void generatePureMethodsDeclarations(java.io.Writer s)
                                      throws java.io.IOException

Generates the pure methods declarations

Parameters:

s - The output for the declarations.

Throws:

java.io.IOException

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 type to translate to Coq.

Returns:

a valid type name.

init

public void init()

Defines predefined Coq types, and some predefined variables (ecReturn, ecThrow and XRES). For now there is no String types should be extended in the future.

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)

Tries to simplify the given tree using the class TProofTyperVisitor.

Specified by:

rewrite in class ProverType

Parameters:

tree - the tree to simplify.

coqRename

private void coqRename(TypeInfo t)

Rename the type, ie. the name TypeInfo.old to a proper Coq name in the variable TypeInfo.def

Parameters:

t - the type name to rename.

getVariableInfo

public java.lang.String getVariableInfo(VariableInfo vi)

Returns a valid Coq name corresponding to the given VariableInfo.

Specified by:

getVariableInfo in class ProverType

Parameters:

vi - the variable info to analyse.

Returns:

coqRename

private void coqRename(VariableInfo vi)

Rename the variable, ie. the name VariableInfo.old to a proper Coq name in the variable VariableInfo.def. Stolen from the PVS plugin...

Parameters:

vi - the variable to rename.

removeInvalidChar

public java.lang.String removeInvalidChar(java.lang.String name)

Removes the invalid characters in Coq for a given String.

Parameters:

name - The name where some invalid characters appear.

Returns:

The name without the invalid characters.

generateDeclarations

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

Generates the declarations for the forall construct in the Coq Fashion, i.e. (var1: Type1) (var2 : Type2)...

Specified by:

generateDeclarations in class ProverType

Parameters:

s - The output

variablesNames - the variables' names.

Throws:

java.io.IOException