Package | Description |
---|---|
de.uka.ilkd.key.nparser.builder | |
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.dl.translation | |
de.uka.ilkd.key.speclang.jml.translation |
Modifier and Type | Method and Description |
---|---|
java.util.List<ClassInvariant> |
ContractsAndInvariantsFinder.getInvariants() |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<ClassInvariant> |
SpecificationRepository.getClassInvariants(KeYJavaType kjt)
Returns all known class invariants for the passed type.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addClassInvariant(ClassInvariant inv)
Registers the passed class invariant, and inherits it to all subclasses
if it is public or protected.
|
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addClassInvariants(ImmutableSet<ClassInvariant> toAdd)
Registers the passed class invariants.
|
Modifier and Type | Class and Description |
---|---|
class |
ClassInvariantImpl
Standard implementation of the ClassInvariant interface.
|
Modifier and Type | Method and Description |
---|---|
ClassInvariant |
PartialInvAxiom.getInv() |
ClassInvariant |
ClassWellDefinedness.getInvariant() |
ClassInvariant |
ClassInvariantImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
ClassInvariant |
ClassInvariant.map(java.util.function.UnaryOperator<Term> op,
Services services) |
ClassInvariant |
ClassInvariantImpl.setKJT(KeYJavaType newKjt) |
ClassInvariant |
ClassInvariant.setKJT(KeYJavaType kjt)
Returns another class invariant like this one, except that it refers to the
passed KeYJavaType.
|
Constructor and Description |
---|
ClassWellDefinedness(ClassInvariant inv,
IObserverFunction target,
Term accessible,
Term mby,
Services services) |
PartialInvAxiom(ClassInvariant inv,
boolean isStatic,
Services services)
Creates a new class axiom.
|
PartialInvAxiom(ClassInvariant inv,
java.lang.String displayName,
Services services) |
Modifier and Type | Method and Description |
---|---|
ClassInvariant |
DLSpecFactory.createDLClassInvariant(java.lang.String name,
java.lang.String displayName,
ParsableVariable selfVar,
Term inv)
Creates a class invariant from a formula and a designated "self".
|
Modifier and Type | Method and Description |
---|---|
ClassInvariant |
JMLSpecFactory.createJMLClassInvariant(KeYJavaType kjt,
TextualJMLClassInv textualInv) |
ClassInvariant |
JMLSpecFactory.createJMLClassInvariant(KeYJavaType kjt,
VisibilityModifier visibility,
boolean isStatic,
LabeledParserRuleContext originalInv) |
Copyright © 2003-2019 The KeY-Project.