001 package escjava.vcGeneration;
002
003 import java.util.HashMap;
004 import java.io.*;
005
006 import escjava.translate.InitialState;
007 import javafe.ast.Expr;
008
009 /**
010 * The interface to be implemented when adding a new prover to ESC/Java.
011 *
012 * <p><b>Any</b> implementing class <i>should</i> be placed in an appropriately named
013 * <i>subpackage</i> of the <i>escjava.vcGeneration</i>
014 * package. In addition, the implementing classes name should be be a capitilized
015 * version of the subpackages name with all dots removed:
016 * <center>
017 * For example, for subpackage <i>pvs.unsorted</i>, the implementing classes name
018 * should be <i>PvsUnsortedProver</i>.
019 * </center>
020 * This restriction exists so that new provers may be generically loaded and
021 * created at runtime within the <i>escjava.Main</i> class and different provers may
022 * be easily identified within an editing environment.
023 *
024 * <p>With this interface, even Simplify is treated as just another prover.
025 *
026 * <p>The following terminology is used consistently throughout the vcGenerator
027 * package:
028 * <ul>
029 * <li>by <i>prover</i> we shall mean a <i>logic</i> and
030 * an underlying proof <i>engine</i></li>
031 * <li>by <i>proof</i> we shall mean an ESC/Java
032 * VC term (targeted to some prover).</li>
033 * </ul>
034 */
035
036 abstract public class ProverType {
037
038 /**
039 * This method is used to provide prover based renaming of the VC file name.
040 *
041 * @param label The method based label that needs to be renamed.
042 * @return The renamed method label.
043 */
044 abstract public String labelRename(String label);
045
046 /**
047 * The visitor pattern is used to map an ESC/Java VC term to a prover term.
048 *
049 * <p>vcGenerator uses this method to perform the mapping.
050 *
051 * <p>A typical implementation of this method will also need to extend the
052 * TVisitor class.
053 *
054 * @param out The stream to which we should write our visitor trail
055 */
056 abstract protected TVisitor visitor(Writer out) throws IOException;
057
058 /**
059 * This method allows a VC term (generated by using the visitor pattern), for
060 * example, to:
061 * <ul>
062 * <li>be wrapped up as a prover assertion (eg. a lemma or theorem for the prover)</li>
063 * <li>universally quantify all free variables in the VC term</li>
064 * </ul>
065 *
066 * @param name name to be given to the proof assertion (eg. lemma or theorem)
067 * @param declns free variables of the VC term
068 * @param vc VC term generated by the visitor pattern
069 */
070 abstract public void getProof(Writer out, String name, TNode term) throws IOException;
071
072 /**
073 * {@link VariableInfo} represents a <b>single</b> translation/mapping between an <i>old</i>
074 * variable name and the <i>targeted</i> prover variable name.
075 *
076 * <p>This method returns the target prover's variable name given one of these
077 * translations/mapplets.
078 *
079 * @param caller The specific variable name translation/mapplet we are to use.
080 * @return
081 */
082 abstract public String getVariableInfo(VariableInfo caller);
083
084 /**
085 * {@link TypeInfo} represents a <b>single</b> translation/mapping between an <i>old</i>
086 * type name and the <i>targeted</i> prover type name.
087 *
088 * <p>This method returns the target prover's type name given one of these
089 * translations/mapplets.
090 *
091 * @param caller The specific type name translation/mapplet we are to use.
092 * @return
093 */
094 abstract public String getTypeInfo(TypeInfo caller);
095
096 /**
097 * Used to initialise the variable and type maps.
098 */
099 abstract public void init();
100
101 /**
102 * This method is used by untyped prover logics to add typing predicates to
103 * the supplied VC term.
104 * <p>Typed prover logics do not need to do anything here.
105 *
106 * @param tree the VC term to which typing predicates <i>may</i> need to be added.
107 * @return
108 */
109 abstract public Expr addTypeInfo(InitialState initState, Expr tree);
110
111 /**
112 * This method allows an ESC/Java VC term to be simplified <i>before</i>
113 * it is translated to the target prover.
114 *
115 * @param tree a VC term to be simplified
116 */
117 //FIXME To what extent is this really necessary?
118 abstract public TNode rewrite(TNode tree);
119
120 /**
121 * This methods generates the declarations for a specified prover.
122 * @param out The buffer to which we want to generate the declarations to.
123 * @param variablesName The hashmap containing all the variables, usually {@link TNode#variablesName}.
124 */
125 abstract protected void generateDeclarations(/*@ non_null @*/Writer out, HashMap variablesName) throws IOException;
126
127 /**
128 * This convenience method generates the declarations for a given term. These declarations
129 * are written to the specified stream.
130 *
131 * @param out the stream to which the generated declarations are written
132 * @param term the term from which the declarations are to be obtained
133 */
134 final public void generateDeclarations(Writer out, TNode term) throws IOException {
135 term.generateDeclarations(out, this);
136 }
137
138 /**
139 * This convenience method uses the visitor pattern to generate a prover specific term.
140 * Used by {@link VcGenerator#getProof(Writer, String)}.
141 *
142 * @param out the stream to which the generated term is to be written
143 * @param term the term we wish to convert
144 */
145 final public void generateTerm(Writer out, TNode term) throws IOException {
146 term.accept(visitor(out));
147 }
148
149 }