| java.lang.Object de.uka.ilkd.key.proof.init.AbstractPO de.uka.ilkd.key.proof.init.ComputeSpecificationPONew
ComputeSpecificationPONew | public class ComputeSpecificationPONew extends AbstractPO (Code) | | |
Methods inherited from de.uka.ilkd.key.proof.init.AbstractPO | public boolean askUserForEnvironment()(Code)(Java Doc) public static Term buildAtPreDefinitions(Map atPreFunctions)(Code)(Java Doc) protected ProgramVariable buildExcVar()(Code)(Java Doc) protected ListOfProgramVariable buildParamVars(ModelMethod modelMethod)(Code)(Java Doc) protected ProgramVariable buildResultVar(ModelMethod modelMethod)(Code)(Java Doc) protected LogicVariable buildSelfVarAsLogicVar()(Code)(Java Doc) protected ProgramVariable buildSelfVarAsProgVar()(Code)(Java Doc) public static void createAtPreFunctionsForTerm(Term term, Map atPreFunctions)(Code)(Java Doc) public ProofAggregate getPO()(Code)(Java Doc) public String name()(Code)(Java Doc) public void readActivatedChoices() throws ProofInputException(Code)(Java Doc) public void readSpecs()(Code)(Java Doc) protected void registerInNamespaces(ProgramVariable pv)(Code)(Java Doc) protected void registerInNamespaces(ListOfProgramVariable pvs)(Code)(Java Doc) protected void registerInNamespaces(Map atPreFunctions)(Code)(Java Doc) protected Term replaceOps(Map map, Term term)(Code)(Java Doc) public void setInitConfig(InitConfig initConfig)(Code)(Java Doc) protected ListOfParsableVariable toPV(ListOfProgramVariable vars)(Code)(Java Doc) protected Term translateInv(ClassInvariant inv) throws SLTranslationError(Code)(Java Doc) protected Term translateInvOpen(ClassInvariant inv, ParsableVariable selfVar) throws SLTranslationError(Code)(Java Doc) protected Term translateInvs(ListOfClassInvariant invs) throws SLTranslationError(Code)(Java Doc) protected Term translateInvsOpen(ListOfClassInvariant invs, ParsableVariable selfVar) throws SLTranslationError(Code)(Java Doc) protected Term translateModifies(OperationContract contract, Term targetTerm, ParsableVariable selfVar, ListOfParsableVariable paramVars) throws SLTranslationError(Code)(Java Doc) protected Term translatePost(OperationContract contract, ParsableVariable selfVar, ListOfParsableVariable paramVars, ParsableVariable resultVar, ParsableVariable excVar) throws SLTranslationError(Code)(Java Doc) protected Term translatePre(OperationContract contract, ParsableVariable selfVar, ListOfParsableVariable paramVars) throws SLTranslationError(Code)(Java Doc)
|
|
|