|
|||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||
ObjectInvariant
BinaryInvariant
TwoSequenceString
SeqSeqStringEqual
public class SeqSeqStringEqual
Represents invariants between two sequences of String values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as x[] == y[] lexically. If order doesn't matter for each variable, then the sequences are compared to see if they are set equivalent. Prints as x[] == y[]. If the auxiliary information (e.g., order matters) doesn't match between two variables, then this invariant cannot apply to those variables.
| Nested Class Summary |
|---|
| Nested classes/interfaces inherited from class Invariant |
|---|
Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match |
| Field Summary | |
|---|---|
static boolean |
dkconfig_enabled
Boolean. |
| Fields inherited from class TwoSequenceString |
|---|
swap |
| Constructor Summary | |
|---|---|
protected |
SeqSeqStringEqual(boolean order)
|
protected |
SeqSeqStringEqual(PptSlice ppt,
boolean order)
|
| Method Summary | |
|---|---|
InvariantStatus |
add_modified(String[] v1,
String[] v2,
int count)
Default implementation simply calls check. |
InvariantStatus |
check_modified(String[] v1,
String[] v2,
int count)
|
protected double |
computeConfidence()
This method computes the confidence that this invariant occurred by chance. |
boolean |
enabled()
Returns whether or not this invariant is enabled |
double |
eq_confidence()
If the invariant is a equality invariant, then its confidence. |
static SeqSeqStringEqual |
find(PptSlice ppt)
|
String |
format_simplify()
|
String |
format_using(OutputFormat format)
|
NISuppressionSet |
get_ni_suppressions()
Returns a list of non-instantiating suppressions for this invariant. |
static SeqSeqStringEqual |
get_proto()
Returns the prototype invariant for SeqSeqStringEqual |
protected SeqSeqStringEqual |
instantiate_dyn(PptSlice slice)
Instantiates the invariant on the specified slice |
boolean |
instantiate_ok(VarInfo[] vis)
Non-Equal SeqComparison is only valid on integral types |
boolean |
isEqual()
|
boolean |
isExclusiveFormula(Invariant o)
|
DiscardInfo |
isObviousDynamically_SomeInEquality()
Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations. |
DiscardInfo |
isObviousDynamically(VarInfo[] vis)
Return non-null if this invariant is necessarily true from a fact that can be determined dynamically (after checking data) -- for the given varInfos rather than the varInfos of this. |
DiscardInfo |
isObviousStatically_SomeInEquality()
Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations. |
DiscardInfo |
isObviousStatically(VarInfo[] vis)
Return true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this. |
boolean |
isSameFormula(Invariant o)
Return true if both invariants are the same class and the order of the variables (swap) is the same. |
void |
repCheck()
Check the rep invariants of this. |
String |
repr()
Returns a representation of the class. |
protected Invariant |
resurrect_done_swapped()
Swaps the variables by inverting the state of swap. |
| Methods inherited from class TwoSequenceString |
|---|
add_unmodified, add, check_unmodified, check, get_swap, resurrect_done_unswapped, resurrect_done, valid_types, var1, var1, var2, var2 |
| Methods inherited from class BinaryInvariant |
|---|
add_unordered, check_unordered, find, is_symmetric |
| Methods inherited from class Object |
|---|
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
| Methods inherited from interface Comparison |
|---|
var1, var2 |
| Field Detail |
|---|
public static boolean dkconfig_enabled
| Constructor Detail |
|---|
protected SeqSeqStringEqual(PptSlice ppt,
boolean order)
protected SeqSeqStringEqual(boolean order)
| Method Detail |
|---|
public static SeqSeqStringEqual get_proto()
public boolean enabled()
enabled in class Invariantpublic boolean instantiate_ok(VarInfo[] vis)
instantiate_ok in class InvariantInvariant.valid_types(VarInfo[])protected SeqSeqStringEqual instantiate_dyn(PptSlice slice)
instantiate_dyn in class Invariantprotected Invariant resurrect_done_swapped()
TwoSequenceString
resurrect_done_swapped in class TwoSequenceStringpublic String repr()
TwoSequenceString
repr in class TwoSequenceStringpublic String format_using(OutputFormat format)
format_using in class Invariantpublic String format_simplify()
public InvariantStatus check_modified(String[] v1,
String[] v2,
int count)
check_modified in class TwoSequenceString
public InvariantStatus add_modified(String[] v1,
String[] v2,
int count)
TwoSequenceString
add_modified in class TwoSequenceStringprotected double computeConfidence()
Invariant
computeConfidence in class TwoSequenceStringInvariant.getConfidence()public double eq_confidence()
Comparison
eq_confidence in interface Comparisonpublic boolean isSameFormula(Invariant o)
TwoSequenceString
isSameFormula in class TwoSequenceStringpublic boolean isExclusiveFormula(Invariant o)
isExclusiveFormula in class Invariantpublic DiscardInfo isObviousStatically_SomeInEquality()
isObviousStatically_SomeInEquality in class Invariantpublic DiscardInfo isObviousDynamically_SomeInEquality()
isObviousDynamically_SomeInEquality in class Invariantpublic DiscardInfo isObviousStatically(VarInfo[] vis)
Invariant
isObviousStatically in class Invariantvis - The VarInfos this invariant is obvious over. The
position and data type of the variables is the *same* as that of
this.ppt.var_infos.public DiscardInfo isObviousDynamically(VarInfo[] vis)
Invariant
isObviousDynamically in class Invariantpublic void repCheck()
Invariant
repCheck in class Invariantpublic boolean isEqual()
public static SeqSeqStringEqual find(PptSlice ppt)
public NISuppressionSet get_ni_suppressions()
get_ni_suppressions in class Invariant
|
|||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||