de.uka.ilkd.key.speclang

Interfaces

• AuxiliaryContract
• BlockContract
• ClassInvariant
• Contract
• DependencyContract
• FunctionalOperationContract
• InformationFlowContract
• InitiallyClause
• LoopContract
• LoopSpecification
• MergeContract
• OperationContract
• SpecExtractor
• SpecificationElement

Classes

• AbstractAuxiliaryContractImpl
• AbstractAuxiliaryContractImpl.Combinator
• AbstractAuxiliaryContractImpl.Creator
• AbstractAuxiliaryContractImpl.ReplacementMap
• AbstractAuxiliaryContractImpl.TermReplacementMap
• AbstractAuxiliaryContractImpl.VariableReplacementMap
• AuxiliaryContract.Terms
• AuxiliaryContract.Variables
• AuxiliaryContract.VariablesCreator
• BlockContractImpl
• BlockContractImpl.Combinator
• BlockContractImpl.Creator
• BlockWellDefinedness
• ClassAxiom
• ClassAxiomImpl
• ClassInvariantImpl
• ClassWellDefinedness
• Contract.OriginalVariables
• ContractAxiom
• ContractFactory
• DependencyContractImpl
• FunctionalAuxiliaryContract
• FunctionalBlockContract
• FunctionalLoopContract
• FunctionalOperationContractImpl
• HeapContext
• InformationFlowContractImpl
• InitiallyClauseImpl
• LoopContractImpl
• LoopContractImpl.Combinator
• LoopContractImpl.Creator
• LoopSpecImpl
• LoopWellDefinedness
• MethodWellDefinedness
• ModelMethodExecution
• PartialInvAxiom
• PositionedLabeledString
• PositionedString
• PredicateAbstractionMergeContract
• QueryAxiom
• RepresentsAxiom
• SLEnvInput
• StatementWellDefinedness
• UnparameterizedMergeContract
• WellDefinednessCheck
• WellDefinednessCheck.Condition
• WellDefinednessCheck.POTerms
• WellDefinednessCheck.TermAndFunc
• WellDefinednessCheck.TermListAndFunc

Enums

• LoopContractImpl.ReplaceTypes
• WellDefinednessCheck.Type