de.uka.ilkd.key.speclang

Interface DependencyContract

All Superinterfaces:

Contract, SpecificationElement

All Known Implementing Classes:

DependencyContractImpl

public interface DependencyContract
extends Contract

A contract about the dependencies of an observer symbol, consisting of a precondition, a depends clause, and a measured-by clause.

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.speclang.Contract

Contract.OriginalVariables

Field Summary

Fields inherited from interface de.uka.ilkd.key.speclang.Contract

INVALID_ID

Method Summary

Methods inherited from interface de.uka.ilkd.key.speclang.Contract

createProofObl, createProofObl, createProofObl, getAccessible, getAssignable, getDep, getDep, getGlobalDefs, getGlobalDefs, getHTMLText, getMby, getMby, getMby, getOrigVars, getPlainText, getPre, getPre, getPre, getPre, getProofObl, getRequires, getTarget, getTypeName, hasMby, hasSelfVar, id, isAuxiliary, proofToString, setID, setTarget, toBeSaved, transactionApplicableContract

Methods inherited from interface de.uka.ilkd.key.speclang.SpecificationElement

getDisplayName, getKJT, getName, getVisibility