Package | Description |
---|---|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml.translation |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<ClassAxiom> |
WellDefinednessPO.selectClassAxioms(KeYJavaType kjt) |
protected ImmutableSet<ClassAxiom> |
AbstractPO.selectClassAxioms(KeYJavaType selfKJT) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<ClassAxiom> |
SpecificationRepository.getClassAxioms(KeYJavaType selfKjt)
Returns all class axioms visible in the passed class, including the
axioms induced by invariant declarations.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addClassAxiom(ClassAxiom ax)
Registers the passed class axiom.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addClassAxioms(ImmutableSet<ClassAxiom> toAdd)
Registers the passed class axioms.
|
Modifier and Type | Class and Description |
---|---|
class |
ClassAxiomImpl
Represents an axiom specified in a class.
|
class |
ContractAxiom |
class |
ModelMethodExecution |
class |
PartialInvAxiom
A class axiom which is essentially of the form "o.
|
class |
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.
|
class |
RepresentsAxiom
A class axiom corresponding to a JML* represents clause.
|
Modifier and Type | Method and Description |
---|---|
ClassAxiom |
JMLSpecFactory.createJMLClassAxiom(KeYJavaType kjt,
TextualJMLClassAxiom textual)
Creates a class axiom from a textual JML representation.
|
ClassAxiom |
JMLSpecFactory.createJMLRepresents(KeYJavaType kjt,
TextualJMLRepresents textualRep) |
ClassAxiom |
JMLSpecFactory.createJMLRepresents(KeYJavaType kjt,
VisibilityModifier visibility,
LabeledParserRuleContext originalRep,
boolean isStatic) |
Copyright © 2003-2019 The KeY-Project.