public final class DLSpecFactory
extends java.lang.Object
Constructor and Description |
---|
DLSpecFactory(Services services) |
private final Services services
public DLSpecFactory(Services services)
private Term extractPre(Term fma) throws ProofInputException
ProofInputException
private LocationVariable extractHeapAtPre(Term fma) throws ProofInputException
ProofInputException
private ProgramVariable extractExcVar(Term fma)
private UseOperationContractRule.Instantiation extractInst(Term fma) throws ProofInputException
ProofInputException
private IProgramMethod extractProgramMethod(UseOperationContractRule.Instantiation inst) throws ProofInputException
ProofInputException
private Modality extractModality(UseOperationContractRule.Instantiation inst) throws ProofInputException
ProofInputException
private ProgramVariable extractSelfVar(UseOperationContractRule.Instantiation inst) throws ProofInputException
ProofInputException
private ImmutableList<ProgramVariable> extractParamVars(UseOperationContractRule.Instantiation inst) throws ProofInputException
ProofInputException
private ProgramVariable extractResultVar(UseOperationContractRule.Instantiation inst) throws ProofInputException
ProofInputException
public ClassInvariant createDLClassInvariant(java.lang.String name, java.lang.String displayName, ParsableVariable selfVar, Term inv) throws ProofInputException
ProofInputException
public FunctionalOperationContract createDLOperationContract(java.lang.String name, Term fma, Term modifies) throws ProofInputException
ProofInputException