public final class DLSpecFactory
extends java.lang.Object
Constructor and Description |
---|
DLSpecFactory(Services services) |
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.
|
public DLSpecFactory(Services services)
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
Copyright © 2003-2019 The KeY-Project.