Package de.uka.ilkd.key.speclang

This package contains the specification language frontends of KeY.

See: Description

Interface Summary

Interface	Description
AuxiliaryContract	Super-interface for BlockContract and LoopContract.
BlockContract	A block contract.
ClassInvariant	A class invariant.
Contract	A contractual agreement about an ObserverFunction.
DependencyContract	A contract about the dependencies of an observer symbol, consisting of a precondition, a depends clause, and a measured-by clause.
FunctionalOperationContract	A contract about an operation (i.e., a method or a constructor), consisting of a precondition, a postcondition, a modifies clause, a measured-by clause, and a modality.
InformationFlowContract	A contract about the dependencies of an observer symbol, consisting of a precondition, a depends clause, and a measured-by clause.
InitiallyClause
LoopContract	A contract for a block that begins with a loop.
LoopSpecification	A loop invariant, consisting of an invariant formula, a set of loop predicates, a modifies clause, and a variant term.
MergeContract	Specification of a MergePointStatement.
OperationContract
SpecExtractor	Extracts specifications from comments.
SpecificationElement	Common superinterface of all constructs created by the specification language front ends and managed by SpecificationRepository.

Class Summary

Class	Description
AbstractAuxiliaryContractImpl	Abstract base class for all default implementations of the sub-interfaces of AuxiliaryContract.
AbstractAuxiliaryContractImpl.Combinator<T extends AuxiliaryContract>	This class is used to to combine multiple contracts for the same block and apply them simultaneously.
AbstractAuxiliaryContractImpl.Creator<T extends AuxiliaryContract>	This class contains a builder method for AbstractAuxiliaryContractImpls (AbstractAuxiliaryContractImpl.Creator.create()).
AbstractAuxiliaryContractImpl.ReplacementMap<S extends Sorted>	A map from some type to the same type.
AbstractAuxiliaryContractImpl.TermReplacementMap	A replacement map for terms.
AbstractAuxiliaryContractImpl.VariableReplacementMap	A replacement map for variables.
AuxiliaryContract.Terms
AuxiliaryContract.Variables	This class contains all new variables that are introduced during a AuxiliaryContract's instantiation.
AuxiliaryContract.VariablesCreator
BlockContractImpl	Default implementation of BlockContract.
BlockContractImpl.Combinator	This class is used to to combine multiple contracts for the same block and apply them simultaneously.
BlockContractImpl.Creator	This class is used to build BlockContractImpls.
BlockWellDefinedness	A contract for checking the well-definedness of a jml block contract.
ClassAxiom	An axiom originating from a (JML) specification, belonging to a particular class, and constraining a particular observer symbol.
ClassAxiomImpl	Represents an axiom specified in a class.
ClassInvariantImpl	Standard implementation of the ClassInvariant interface.
ClassWellDefinedness	A contract for checking the well-definedness of a specification for a class invariant.
Contract.OriginalVariables	Class for storing the original variables without always distinguishing several different cases depending on which variables are present/needed in order to provide a general interface.
ContractAxiom
ContractFactory	Contracts should only be created through methods of this class
DependencyContractImpl	Standard implementation of the DependencyContract interface.
FunctionalAuxiliaryContract<T extends AuxiliaryContract>	This class is only used to generate a proof obligation for an AuxiliaryContract.
FunctionalBlockContract	This class is only used to generate a proof obligation for a block (see FunctionalBlockContractPO.
FunctionalLoopContract	This class is only used to generate a proof obligation for a block that starts with a loop (see FunctionalLoopContractPO.
FunctionalOperationContractImpl	Standard implementation of the OperationContract interface.
HeapContext	Heap contexts are various scenarios of what happens to heap variables during PO generation and built-in rule applications, like saving atPre heaps, anonymisation, etc.
InformationFlowContractImpl	Standard implementation of the DependencyContract interface.
InitiallyClauseImpl	Standard implementation of the InitiallyClause interface.
LoopContractImpl	Default implementation for LoopContract.
LoopContractImpl.Combinator	This class is used to to combine multiple contracts for the same block and apply them simultaneously.
LoopContractImpl.Creator	This class is used to build LoopContractImpls.
LoopSpecImpl	Standard implementation of the LoopInvariant interface.
LoopWellDefinedness	A contract for checking the well-definedness of a jml loop invariant.
MethodWellDefinedness	A contract for checking the well-definedness of a specification for a method or model field.
ModelMethodExecution
PartialInvAxiom	A class axiom which is essentially of the form "o.
PositionedLabeledString	A positionedString with labels, which can then be passed over to the translated term.
PositionedString	A string with associated position information (file and line number).
PredicateAbstractionMergeContract	A MergeContract for the MergeWithPredicateAbstraction MergeProcedure.
QueryAxiom	A class axiom that connects an observer symbol representing a Java method (i.e., an object of type IProgramMethod), with the corresponding method body.
RepresentsAxiom	A class axiom corresponding to a JML* represents clause.
SLEnvInput	EnvInput for standalone specification language front ends.
StatementWellDefinedness	A contract for checking the well-definedness of a jml statement.
UnparameterizedMergeContract	A MergeContract for UnparametricMergeProcedures like MergeByIfThenElse.
WellDefinednessCheck	A contract for checking the well-definedness of a jml specification element (i.e. a class invariant, a method contract, a model field or any jml statement), consisting of precondition, assignable-clause, postcondition, accessible-clause, measured-by-clause and represents-clause.
WellDefinednessCheck.Condition	A static data structure for storing and passing two terms, denoting the implicit and the explicit part of a pre- or post-condition.
WellDefinednessCheck.POTerms	A data structure for storing and passing all specifications of a specification element includinf pre- and post-condition, an assignable-clause and a list of all other clauses specified.
WellDefinednessCheck.TermAndFunc	A static data structure for passing a term with a function.
WellDefinednessCheck.TermListAndFunc	A static data structure for passing a term list with a function.

Enum Summary

Enum	Description
LoopContractImpl.ReplaceTypes
WellDefinednessCheck.Type

Package de.uka.ilkd.key.speclang Description

This package contains the specification language frontends of KeY. The task of the individual frontends (locates in subpackages such as "jml"), is to create objects of the types declared in this package. Core types are Contract, OperationContract, and DependencyContract. These are used as input by the proof obligations declared in package proof.init.