de.uka.ilkd.key.speclang.dl.translation

Class DLSpecFactory

java.lang.Object

de.uka.ilkd.key.speclang.dl.translation.DLSpecFactory

public final class DLSpecFactory
extends java.lang.Object

A factory for creating class invariants and operation contracts from DL specifications. For an example, see java_dl/DLContractChooser.

Field Summary

Fields

Modifier and Type	Field and Description
private Services	services

Constructor Summary

Constructors

Constructor and Description
DLSpecFactory(Services services)

Method Summary

Modifier and Type	Method and Description
ClassInvariant	createDLClassInvariant(java.lang.String name, java.lang.String displayName, ParsableVariable selfVar, Term inv) Creates a class invariant from a formula and a designated "self".
FunctionalOperationContract	createDLOperationContract(java.lang.String name, Term fma, Term modifies) Creates an operation contract from an implication formula of the form "pre -> {heapAtPre := heap} [#catchAll(java.lang.Throwable exc){m();}]post", (where the update and/or the #catchAll may be omitted) and a modifies clause.
private ProgramVariable	extractExcVar(Term fma)
private LocationVariable	extractHeapAtPre(Term fma)
private UseOperationContractRule.Instantiation	extractInst(Term fma)
private Modality	extractModality(UseOperationContractRule.Instantiation inst)
private ImmutableList<ProgramVariable>	extractParamVars(UseOperationContractRule.Instantiation inst)
private Term	extractPost(Term fma)
private Term	extractPre(Term fma)
private IProgramMethod	extractProgramMethod(UseOperationContractRule.Instantiation inst)
private ProgramVariable	extractResultVar(UseOperationContractRule.Instantiation inst)
private ProgramVariable	extractSelfVar(UseOperationContractRule.Instantiation inst)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

services

private final Services services

Constructor Detail

DLSpecFactory

public DLSpecFactory(Services services)

Method Detail

extractPre

private Term extractPre(Term fma)
                 throws ProofInputException

Throws:

ProofInputException

extractHeapAtPre

private LocationVariable extractHeapAtPre(Term fma)
                                   throws ProofInputException

Throws:

ProofInputException

extractExcVar

private ProgramVariable extractExcVar(Term fma)

extractInst

private UseOperationContractRule.Instantiation extractInst(Term fma)
                                                    throws ProofInputException

Throws:

ProofInputException

extractProgramMethod

private IProgramMethod extractProgramMethod(UseOperationContractRule.Instantiation inst)
                                     throws ProofInputException

Throws:

ProofInputException

extractModality

private Modality extractModality(UseOperationContractRule.Instantiation inst)
                          throws ProofInputException

Throws:

ProofInputException

extractSelfVar

private ProgramVariable extractSelfVar(UseOperationContractRule.Instantiation inst)
                                throws ProofInputException

Throws:

ProofInputException

extractParamVars

private ImmutableList<ProgramVariable> extractParamVars(UseOperationContractRule.Instantiation inst)
                                                 throws ProofInputException

Throws:

ProofInputException

extractResultVar

private ProgramVariable extractResultVar(UseOperationContractRule.Instantiation inst)
                                  throws ProofInputException

Throws:

ProofInputException

extractPost

private Term extractPost(Term fma)

createDLClassInvariant

public ClassInvariant createDLClassInvariant(java.lang.String name,
                                             java.lang.String displayName,
                                             ParsableVariable selfVar,
                                             Term inv)
                                      throws ProofInputException

Creates a class invariant from a formula and a designated "self".

Throws:

ProofInputException

createDLOperationContract

public FunctionalOperationContract createDLOperationContract(java.lang.String name,
                                                             Term fma,
                                                             Term modifies)
                                                      throws ProofInputException

Creates an operation contract from an implication formula of the form "pre -> {heapAtPre := heap} [#catchAll(java.lang.Throwable exc){m();}]post", (where the update and/or the #catchAll may be omitted) and a modifies clause.

Throws:

ProofInputException