Class and Description |
---|
Contract
A contractual agreement about an ObserverFunction.
|
Class and Description |
---|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
AuxiliaryContract
Super-interface for
BlockContract and LoopContract . |
BlockContract
A block contract.
|
Contract
A contractual agreement about an ObserverFunction.
|
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.
|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
BlockContract
A block contract.
|
InformationFlowContract
A contract about the dependencies of an observer symbol, consisting of
a precondition, a depends clause, and a measured-by clause.
|
LoopSpecification
A loop invariant, consisting of an invariant formula, a set of loop
predicates, a modifies clause, and a variant term.
|
Class and Description |
---|
BlockContract
A block contract.
|
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.
|
LoopSpecification
A loop invariant, consisting of an invariant formula, a set of loop
predicates, a modifies clause, and a variant term.
|
Class and Description |
---|
BlockContract
A block contract.
|
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.
|
LoopSpecification
A loop invariant, consisting of an invariant formula, a set of loop
predicates, a modifies clause, and a variant term.
|
Class and Description |
---|
SpecificationElement
Common superinterface of all constructs created by the specification
language front ends and managed by SpecificationRepository.
|
Class and Description |
---|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
BlockContract
A block contract.
|
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 . |
Class and Description |
---|
ClassInvariant
A class invariant.
|
Contract
A contractual agreement about an ObserverFunction.
|
Class and Description |
---|
ClassAxiom
An axiom originating from a (JML) specification, belonging to a particular
class, and constraining a particular observer symbol.
|
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.
|
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 . |
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.
|
PositionedString
A string with associated position information (file and line number).
|
WellDefinednessCheck
A contract for checking the well-definedness of a jml specification element
(i.e.
|
Class and Description |
---|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
BlockContract
A block contract.
|
ClassAxiom
An axiom originating from a (JML) specification, belonging to a particular
class, and constraining a particular observer symbol.
|
ClassInvariant
A class invariant.
|
Contract
A contractual agreement about an ObserverFunction.
|
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.
|
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 . |
SpecificationElement
Common superinterface of all constructs created by the specification
language front ends and managed by SpecificationRepository.
|
StatementWellDefinedness
A contract for checking the well-definedness of a jml statement.
|
WellDefinednessCheck
A contract for checking the well-definedness of a jml specification element
(i.e.
|
Class and Description |
---|
AuxiliaryContract
Super-interface for
BlockContract and LoopContract . |
AuxiliaryContract.Terms |
AuxiliaryContract.Variables
This class contains all new variables that are introduced during a
AuxiliaryContract 's instantiation. |
BlockContract
A block contract.
|
Contract
A contractual agreement about an ObserverFunction.
|
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.
|
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.
|
Class and Description |
---|
AbstractAuxiliaryContractImpl
Abstract base class for all default implementations of the sub-interfaces of
AuxiliaryContract . |
AbstractAuxiliaryContractImpl.Combinator
This class is used to to combine multiple contracts for the same block and apply them
simultaneously.
|
AbstractAuxiliaryContractImpl.Creator
This class contains a builder method for
AbstractAuxiliaryContractImpl s
(AbstractAuxiliaryContractImpl.Creator.create() ). |
AuxiliaryContract
Super-interface for
BlockContract and LoopContract . |
AuxiliaryContract.Terms |
AuxiliaryContract.Variables
This class contains all new variables that are introduced during a
AuxiliaryContract 's instantiation. |
BlockContract
A block contract.
|
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.
|
ClassInvariant
A class invariant.
|
ClassWellDefinedness
A contract for checking the well-definedness of a specification for a class invariant.
|
Contract
A contractual agreement about an ObserverFunction.
|
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 |
DependencyContract
A contract about the dependencies of an observer symbol, consisting of
a precondition, a depends clause, and a measured-by clause.
|
FunctionalAuxiliaryContract
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 . |
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.
|
LoopWellDefinedness
A contract for checking the well-definedness of a jml loop invariant.
|
MergeContract
Specification of a
MergePointStatement . |
MethodWellDefinedness
A contract for checking the well-definedness of a specification for a method or model field.
|
ModelMethodExecution |
OperationContract |
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.
|
SpecificationElement
Common superinterface of all constructs created by the specification
language front ends and managed by SpecificationRepository.
|
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.
|
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.
|
Class and Description |
---|
ClassInvariant
A class invariant.
|
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.
|
Class and Description |
---|
BlockContract
A block contract.
|
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 . |
PositionedString
A string with associated position information (file and line number).
|
SpecExtractor
Extracts specifications from comments.
|
SpecificationElement
Common superinterface of all constructs created by the specification
language front ends and managed by SpecificationRepository.
|
Class and Description |
---|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
BlockContract
A block contract.
|
ClassAxiom
An axiom originating from a (JML) specification, belonging to a particular
class, and constraining a particular observer symbol.
|
ClassInvariant
A class invariant.
|
Contract
A contractual agreement about an ObserverFunction.
|
ContractFactory
Contracts should only be created through methods of this class
|
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.
|
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 . |
Class and Description |
---|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
BlockContract
A block contract.
|
Contract
A contractual agreement about an ObserverFunction.
|
LoopSpecification
A loop invariant, consisting of an invariant formula, a set of loop
predicates, a modifies clause, and a variant term.
|
Class and Description |
---|
AuxiliaryContract
Super-interface for
BlockContract and LoopContract . |
Contract
A contractual agreement about an ObserverFunction.
|
LoopSpecification
A loop invariant, consisting of an invariant formula, a set of loop
predicates, a modifies clause, and a variant term.
|
Class and Description |
---|
AuxiliaryContract
Super-interface for
BlockContract and LoopContract . |
Contract
A contractual agreement about an ObserverFunction.
|
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.
|
LoopSpecification
A loop invariant, consisting of an invariant formula, a set of loop
predicates, a modifies clause, and a variant term.
|
Class and Description |
---|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
Contract
A contractual agreement about an ObserverFunction.
|
Class and Description |
---|
Contract
A contractual agreement about an ObserverFunction.
|
PositionedString
A string with associated position information (file and line number).
|
Class and Description |
---|
LoopSpecification
A loop invariant, consisting of an invariant formula, a set of loop
predicates, a modifies clause, and a variant term.
|
Copyright © 2003-2019 The KeY-Project.