public class OriginTermLabel extends java.lang.Object implements TermLabel
An OriginTermLabel
saves a term's origin in the JML specification
(getOrigin()
) as well as the origins of all of its subterms and former
subterms (getSubtermOrigins()
).
For this to work correctly, you must call
#collectSubtermOrigins(Term, TermBuilder)
for every top-level formula in your
original proof obligation.
Before doing this, you can call TermBuilder.addLabelToAllSubs(Term, TermLabel)
for every term you have added to the original contract in your PO to add an
OriginTermLabel
of your choosing. Terms for which you do not do this get a label of the form
new OriginTermLabel(SpecType.NONE, null, -1)
.
Modifier and Type | Class and Description |
---|---|
static class |
OriginTermLabel.FileOrigin
Origin for terms that originate from a file.
|
static class |
OriginTermLabel.NodeOrigin
Origin for terms that originate from a proof node.
|
static class |
OriginTermLabel.Origin
An origin encapsulates some information about where a term originates from.
|
static class |
OriginTermLabel.SpecType
A
SpecType is any type of JML specification which gets translated into JavaDL. |
Modifier and Type | Field and Description |
---|---|
static int |
CHILD_COUNT |
static Name |
NAME
Display name for
OriginTermLabel s. |
Constructor and Description |
---|
OriginTermLabel(OriginTermLabel.Origin origin)
Creates a new
OriginTermLabel . |
OriginTermLabel(OriginTermLabel.Origin origin,
java.util.Set<OriginTermLabel.Origin> subtermOrigins)
Creates a new
OriginTermLabel . |
OriginTermLabel(java.util.Set<OriginTermLabel.Origin> subtermOrigins)
Creates a new
OriginTermLabel . |
Modifier and Type | Method and Description |
---|---|
static boolean |
canAddLabel(Operator op,
Services services)
Determines whether an
OriginTermLabel can be added to a term with the specified
operator. |
static boolean |
canAddLabel(Term term,
Services services)
Determines whether an
OriginTermLabel can be added to the specified term. |
static Term |
collectSubtermOrigins(Term term,
Services services)
This method transforms a term in such a way that
every
OriginTermLabel contains all of the correct
getSubtermOrigins() . |
static OriginTermLabel.Origin |
computeCommonFileOrigin(java.util.Set<OriginTermLabel.FileOrigin> origins)
Compute the common origin from all origins in the passed origins set.
|
static OriginTermLabel.Origin |
computeCommonNodeOrigin(java.util.Set<OriginTermLabel.NodeOrigin> origins)
Compute the common origin from all origins in the passed origins set.
|
static OriginTermLabel.Origin |
computeCommonOrigin(java.util.Set<? extends OriginTermLabel.Origin> origins)
Compute the common origin from all origins in the passed origins set.
|
boolean |
equals(java.lang.Object obj) |
java.lang.Object |
getChild(int i)
Retrieves the i-th parameter object of this term label.
|
int |
getChildCount()
Gets the number of parameters of this term label.
|
OriginTermLabel.Origin |
getOrigin() |
static OriginTermLabel.Origin |
getOrigin(PosInOccurrence pio)
Find a term's origin.
|
static OriginTermLabel.Origin |
getOrigin(PosInSequent pis)
Find a term's origin.
|
java.util.Set<OriginTermLabel.Origin> |
getSubtermOrigins()
Returns the origins of the term's sub-terms and former sub-terms.
|
int |
hashCode() |
boolean |
isProofRelevant()
Returns
true iff this label is used in any way during the proof. |
Name |
name()
returns the name of this element
|
static SequentChangeInfo |
removeOriginLabels(Sequent seq,
Services services)
Removes all
OriginTermLabel from the specified sequent. |
static Term |
removeOriginLabels(Term term,
Services services)
Removes all
OriginTermLabel from the specified term and its sub-terms. |
java.lang.String |
toString() |
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
removeIrrelevantLabels, removeIrrelevantLabels
public static final Name NAME
OriginTermLabel
s.public static final int CHILD_COUNT
getChildCount()
,
Constant Field Valuespublic OriginTermLabel(OriginTermLabel.Origin origin)
OriginTermLabel
.origin
- the term's origin.public OriginTermLabel(OriginTermLabel.Origin origin, java.util.Set<OriginTermLabel.Origin> subtermOrigins)
OriginTermLabel
.origin
- the term's origin.subtermOrigins
- the origins of the term's (former) subterms.public OriginTermLabel(java.util.Set<OriginTermLabel.Origin> subtermOrigins)
OriginTermLabel
.subtermOrigins
- the origins of the term's (former) subterms.public static OriginTermLabel.Origin getOrigin(PosInSequent pis)
pis
- the position of the term whose origin to find.public static OriginTermLabel.Origin getOrigin(PosInOccurrence pio)
pio
- the position of the term whose origin to find.public int hashCode()
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public static boolean canAddLabel(Term term, Services services)
Determines whether an OriginTermLabel
can be added to the specified term.
E.g., no labels should be added to terms whose operator is a heap variable as this leads to various problems during proof search.
term
- a termservices
- services.true
iff an OriginTermLabel
can be added to the specified term.public static boolean canAddLabel(Operator op, Services services)
Determines whether an OriginTermLabel
can be added to a term with the specified
operator.
E.g., no labels should be added to terms whose operator is a heap variable as this leads to various problems during proof search.
op
- the specified operator.services
- services.true
iff an OriginTermLabel
can be added to a term
with the specified operator.public static SequentChangeInfo removeOriginLabels(Sequent seq, Services services)
OriginTermLabel
from the specified sequent.seq
- the sequent to transform.services
- services.public static Term removeOriginLabels(Term term, Services services)
OriginTermLabel
from the specified term and its sub-terms.term
- the term to transform.services
- services.public static OriginTermLabel.Origin computeCommonFileOrigin(java.util.Set<OriginTermLabel.FileOrigin> origins)
origins
- the passed origins setpublic static OriginTermLabel.Origin computeCommonNodeOrigin(java.util.Set<OriginTermLabel.NodeOrigin> origins)
origins
- the passed origins setpublic static OriginTermLabel.Origin computeCommonOrigin(java.util.Set<? extends OriginTermLabel.Origin> origins)
origins
- the passed origins setpublic static Term collectSubtermOrigins(Term term, Services services)
OriginTermLabel
contains all of the correct
getSubtermOrigins()
.term
- the term to transform.services
- services.public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.Object getChild(int i)
TermLabel
A term label may have structure, i.e. can be parameterized.
public int getChildCount()
TermLabel
getChildCount
in interface TermLabel
public boolean isProofRelevant()
TermLabel
true
iff this label is used in any way during the proof.
E.g., OriginTermLabel
s are not used during the proof;
they only provide a convenience for the user.isProofRelevant
in interface TermLabel
true
iff this label is used in any way during the proof.public OriginTermLabel.Origin getOrigin()
public java.util.Set<OriginTermLabel.Origin> getSubtermOrigins()
Returns the origins of the term's sub-terms and former sub-terms.
Note that you need to have called #collectSubtermOrigins(Term, TermBuilder)
for this method to work correctly.
OriginTermLabelRefactoring
Copyright © 2003-2019 The KeY-Project.