|
|||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||
ObjectInvariant
UnaryInvariant
SingleStringSequence
CommonStringSequence
public class CommonStringSequence
Represents string sequences that contain a common subset. Prints as "{s1, s2, s3, ...} subset of x[]".
| 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. |
| Constructor Summary | |
|---|---|
protected |
CommonStringSequence(PptSlice ppt)
|
| Method Summary | |
|---|---|
InvariantStatus |
add_modified(String[] a,
int count)
This method need not check for falsified; that is done by the caller. |
InvariantStatus |
check_modified(String[] a,
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 |
String |
format_daikon()
|
String |
format_using(OutputFormat format)
|
static CommonStringSequence |
get_proto()
Returns the prototype invariant for CommonStringSequence |
protected CommonStringSequence |
instantiate_dyn(PptSlice slice)
instantiate an invariant on the specified slice |
DiscardInfo |
isObviousImplied()
|
boolean |
isSameFormula(Invariant other)
|
String |
repr()
For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output. |
| Methods inherited from class SingleStringSequence |
|---|
add_unmodified, add, check_unmodified, check, valid_types, var |
| Methods inherited from class UnaryInvariant |
|---|
resurrect_done |
| Methods inherited from class Object |
|---|
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
| Field Detail |
|---|
public static boolean dkconfig_enabled
| Constructor Detail |
|---|
protected CommonStringSequence(PptSlice ppt)
| Method Detail |
|---|
public static CommonStringSequence get_proto()
public boolean enabled()
enabled in class Invariantprotected CommonStringSequence instantiate_dyn(PptSlice slice)
instantiate_dyn in class Invariantpublic String repr()
Invariant
repr in class Invariantpublic String format_using(OutputFormat format)
format_using in class Invariantpublic String format_daikon()
public InvariantStatus check_modified(String[] a,
int count)
check_modified in class SingleStringSequence
public InvariantStatus add_modified(String[] a,
int count)
SingleStringSequence
add_modified in class SingleStringSequenceprotected double computeConfidence()
Invariant
computeConfidence in class InvariantInvariant.getConfidence()public DiscardInfo isObviousImplied()
public boolean isSameFormula(Invariant other)
isSameFormula in class Invariant
|
|||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||