See: Description
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 | 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
AbstractAuxiliaryContractImpl s
(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
BlockContractImpl s. |
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
LoopContractImpl s. |
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 | |
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 | |
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 | Description |
---|---|
LoopContractImpl.ReplaceTypes | |
WellDefinednessCheck.Type |