Next: , Previous: Running Daikon, Up: Top   [Contents][Index]

5 Daikon output

Daikon outputs the invariants that it discovers in textual form to your terminal. This chapter describes how to interpret those invariants — in other words, what do they mean?

Daikon also creates a .inv file that contains the invariants in serialized (binary) form. You can use the .inv file to print the invariants (see Printing invariants) in a variety of formats, to insert the invariants in your source code (see Annotate), to perform run-time checking of the invariants (see Runtime-check instrumenter, and InvariantChecker), and to do various other operations. See Tools, for descriptions of such tools.

If you wish to write your own tools for processing invariants, you have two general options. You can parse Daikon’s textual output, or you can write Java code that processes the .inv file. The .inv file is simply a serialized PptMap object. In addition to reading the Javadoc, you can examine how the other tools use this data structure.


Next: , Up: Daikon output   [Contents][Index]

5.1 Invariant syntax

Daikon can produce output in a variety of formats. Each of the format names can be specified as an argument to the --format argument of Daikon (see Options to control Daikon output), PrintInvariants (see Printing invariants), and Annotate (see Annotate). When passed on the command line, the format names are case-insensitive: --format JML and --format jml have the same effect.

You can enhance Daikon to produce output in other formats. See New formatting for invariants in Daikon Developer Manual.

Daikon format

Daikon’s default format is a mix of Java, mathematical logic, and some additional extensions. It is intended to concisely convey meaning to programmers.

DBC format

This format produces output in the design-by-contract (DBC) format expected by Parasoft’s Jtest tool (http://www.parasoft.com).

ESC/Java format
ESC format

The Extended Static Checker for Java (ESC/Java) is a programming tool for finding errors in Java programs by checking annotations that are inserted in source code; for more details, see http://www.hpl.hp.com/downloads/crl/jtk/. Daikon’s ESC/Java format (which can also be specified as ESC format) is intended for use with the original ESC/Java tool. Use Daikon’s JML format for use with the ESC/Java2 tool.

Java format

Write output as Java expressions. This means that each invariant would be a valid Java expression, if inserted at the correct program point: right after method entry, for method entry invariants; right before method exit, for method exit invariants;, or anywhere in the code, for object invariants.

There are two exceptions. Method exit invariants that refer to pre-state, such as ‘x == old(x) + 1’, are output with the tag ‘\old’ surrounding the pre-state expression (e.g. ‘x == \old(x) + 1’. Method exit invariants that refer to the return value of the method, such as ‘return == x + y’, are output with the tag ‘\result’ in place of the return value (e.g. ‘\result == x + y’). These expression are obviously not valid Java code.

JML format

Produces output in JML (Java Modeling Language, http://www.jmlspecs.org); for details, see the JML Manual. JML format lets you use the various JML tools on Daikon invariants, including runtime assertion checking and the ESC/Java2 tool.

Simplify format

Produces output in the format expected by the Simplify automated theorem prover; for details, see the Simplify distribution.


Next: , Previous: Invariant syntax, Up: Daikon output   [Contents][Index]

5.2 Program points

A program point is a specific place in the source code, such as immediately before a particular line of code. Daikon’s output is organized by program points.

For example, foo():::ENTER is the point at the entry to procedure foo(); the invariants at that point are the preconditions for the foo() method, properties that are always true when the procedure is invoked.

Likewise, foo():::EXIT is the program point at the procedure exit, and invariants there are postconditions. When there are multiple exit points from a procedure (for instance, because of multiple return statements), the different exits are differentiated by suffixing them with their line numbers; for instance, StackAr.top():::EXIT79. The exit point lacking a line number (in this example, StackAr.top():::EXIT) collects the postconditions that are true at every numbered exit point. This is an example of a program point that represents a collection of locations in the program source rather than a single location. This concept is represented in Daikon by the dataflow hierarchy, see Dataflow hierarchy in Daikon Developer Manual.

Two other program point tags that have special meaning to Daikon’s hierarchy organization are :::OBJECT and :::CLASS. The :::OBJECT tag indicates object invariants (sometimes called representation invariants or class invariants) over all the instance (member) fields and static fields of the class. These properties always hold for any object of the given class, from the point of view of a client or user. These properties hold at entry to and exit from every public method of the class (except not the entry to constructors, when fields are not yet initialized).

The :::CLASS tag is just like :::OBJECT, but only for static variables, which have only one value for all objects. Static fields and instance fields are often used for different purposes. Daikon’s separation of the two types of fields permits programmers to see the properties over the static fields without knowing which are the static fields and pick them out of the :::OBJECT program point.

(By contrast, ESC/Java and JML make class invariants hold even at the entry and exit of private methods. Their designers believe that most private methods preserve the class invariant and are called only when the class invariant holds. ESC/Java and JML require an explicit “helper” annotation to indicate a private method for which the class invariant does not hold.)

The Java instrumenter Chicory selects names for program points that include an indication of the argument and return types for each method. These signatures are presented in the JVML format: one character for each primitive type (‘B’ for byte, ‘C’ for character, ‘Z’ for boolean (so as not to clash with byte), etc.); ‘Lclassname;’ for object types; and a ‘[’ prefix for each level of array nesting.


Next: , Previous: Program points, Up: Daikon output   [Contents][Index]

5.3 Variable names

A front end produces a trace file that associates trace variable names with values. Trace variable names need not be exactly the same as the variables in the program. The trace may contain values that are not held in any program variables; in this case, the front end must make up a name to express that value (see below for examples).

Daikon ignores variable names when inferring invariants; it uses the names only when performing output. (Thus, the only practical restriction on trace names is that the VarInfoName parse method must be able to parse the name.)

By convention, trace variables are similar to program variables and field accesses. For example, w and x.y.z are legal trace variables. (So are ‘a[i]’, and ‘a[0].next’, but these are usually handled as derived variables instead; see below.) As in languages such as Java and C, a period character represents field access and square brackets represent selecting an element of a sequence.

In addition to variables that appear in the trace file, Daikon creates additional variables, called “derived variables”, by combining trace variables. For example, for any array a and integer i, Daikon creates a derived variable a[i]. This is not a variable in the program (and this expression might not even appear in the source code), but it may still be useful to compute invariants over this expression. For a list of derived variables and how to control Daikon’s use of them, see Options to enable/disable derived variables.

Some trace variables and derived variables may represent meaningless expressions; in such a circumstance, the value is said to be nonsensical (see Nonsensical values in Daikon Developer Manual).

The remainder of this section describes conventions for naming expressions. Those that cannot be named by simple C/Java expressions are primarily related to arrays and sequences. (In part, these special expressions are necessary because Daikon can only handle variables of scalar (integer, floating-point, boolean, String) and array-of-scalar types. Daikon cannot handle structs, classes, or multi-dimensional arrays or structures, but such data structures can be represented as scalars and arrays by choosing variable names that indicate their relationship.)

Daikon’s current front ends do not produce output for local variables, only for variables visible from outside a procedure. (Also see the --std-visibility option to Chicory, Chicory options.) More generally, Daikon’s front ends produce output at procedure exit and entry, not within the procedure. Thus, Daikon’s output forms a specification from the view of a client of a procedure. If you wish to compute invariants over local variables, you can extend one of Daikon’s front ends (or request us to do so). An alternative that permits computing invariants at arbitrary locations is to call a dummy procedure, passing all the variables of interest. The dummy procedure’s pre- and postconditions will be identical and will represent the invariants at the point of call.

The array introduction operator [] can made Daikon variables look slightly odd, but it is intended to assist in interpreting the variables and to provide an indication that the variable name cannot be substituted directly in a program as an expression.

Each array introduction operator [] increases the dimensionality of the variable, and each array indexing operation [i] decreases it. Since all Daikon variables are scalars or one-dimensional arrays, these operators must be matched up, or have at most one more [] than [i]. (There is one exception: according to a strict interpretation of the rules, the C/Java expression a[i] would turn into the Daikon variable a[][i], since it does not change the dimensionality of any expression it appears in. However, that would be even more confusing, and the point is to avoid confusion, so by convention Daikon front ends use just a[i], not a[][i]. Strictly speaking, none of the [] operators is necessary, since a user with a perfect knowledge of the type of each program variable and field could use that to infer the type of any Daikon expression.)


Up: Variable names   [Contents][Index]

5.3.1 orig() variable example

This section gives an example of use of orig() and post() variables and arrays.

Suppose you have initially that (in Java syntax)

int i = 0;
int[] a = new int[] { 22, 23 };
int[] b = new int[] { 46, 47 };

and then you run the following:

// pre-state values at this point
a[0] = 24;
a[1] = 25
a = b;
a[0] = 48;
a[1] = 49;
i = 1;
// post-state values at this point

The values of various variables are as follows:

orig(a[i]) = 22

The value of a[i] in the pre-state: {22, 23}[0]

orig(a[])[orig(i)] = 22

This is the same as orig(a[i]): {22, 23}[0].

orig(a[])[i] = 23

The value of a[] in the pre-state (which is an array object, not a reference), indexed by the post-state value of i: {22, 23}[1]

orig(a)[orig(i)] = 24

orig(a) is the original value of the reference a, not a’s original elements: {24, 25}[0]

orig(a)[i] = 25

The original pointer value of a, indexed by the post-state value of i: {24, 25}[1]

a[orig(i)] = 48

In the post-state, a indexed by the original value of i: {48, 49}[0]

a[i] = 49

The value of a[i] in the post-state.

b = orig(b) = some hashcode

The identity of the array b has not changed.

b[] = [48, 49]
orig(b[]) = [46, 47]

For an array b, ‘b=orig(b)’ does not imply ‘b[]=orig(b[])’.

orig(a[post(i)]) = 23

The pre-state value of a[1] (because the post-state value of i is 1): {22, 23}[1]


Next: , Previous: Variable names, Up: Daikon output   [Contents][Index]

5.4 Interpreting Daikon output

If nothing gets printed before the ‘Exiting’ line, then Daikon found no invariants. You can get a little bit more information by using the --output_num_samples flag to Daikon (see Options to control Daikon output).

Daikon’s output is predicated on the assumption that all expressions that get evaluated are sensible. For instance, if Daikon prints ‘a.b == 0’, then that means that ifa.b’ is sensible (that is, ‘a’ is non-null), then its value is zero. When ‘a’ is ‘null’, then ‘a.b’ is called “nonsensical”. Daikon’s output ignores all nonsensical values. If you would like the assumptions to be printed explicitly, then set the daikon.Daikon.guardNulls configuration option (see General configuration options).


Next: , Up: Interpreting output   [Contents][Index]

5.4.1 Redundant invariants

By default, Daikon does not display redundant invariants — those that are implied by other invariants in the output — because such results would merely clutter the output without adding any valuable information. For instance, if Daikon reports ‘x==y’, then it never also reports ‘x-1==y-1’. You can control this behavior to some extent by disabling invariant filters; see Invariant filters. (You can also print all invariants, even redundant ones, by saving the invariants to a .inv file and then using the PrintInvariants (see Printing invariants) or Diff (see Invariant Diff) programs to print the results.)


Next: , Previous: Redundant invariants, Up: Interpreting output   [Contents][Index]

5.4.2 Equal variables

If two variables x and y are equal, then any invariant about x is also true about y. Daikon chooses one variable (the leader) from the set of equal variables, and only prints invariants over the leader.

Suppose that a = b = c. Then Daikon will print a = b and a = c, but not b = c. Furthermore, Daikon might print a > d, but would not print b > d or c > d.

You can control which variables are in an equality set; see Variable comparability in Daikon Developer Manual.


Previous: Equal variables, Up: Interpreting output   [Contents][Index]

5.4.3 Has only one value variables

The output ‘var has only one value’ in Daikon’s output means that every time that variable var was encountered, it had the same value. Daikon ordinarily reports the actual value, as in ‘var == 22’. Typically this means that the variable is a hashcode or address — that is, its declared type is ‘hashcode’ (see Variable declarations in Daikon Developer Manual). For example, ‘var == 0x38E8A’ is not very illuminating, but it is still interesting that var was never rebound to a different object.

Note that ‘var has only one value’ is different from saying that var is unmodified.

A variable might have only one value but not be reported as unmodified because the variable is not a parameter to a procedure — for instance, if a routine always returns the same object, or in a class invariant. A variable can be reported as unmodified but not have only one value because the variable is never modified during any execution of the procedure, but has different values on different invocations of the procedure.


Next: , Previous: Interpreting output, Up: Daikon output   [Contents][Index]

5.5 Invariant list

The following is a list of all of the invariants that Daikon detects. Each invariant has a configuration enable switch. By default most invariants are enabled. Any that are not enabled by default are indicated below. Some invariants also have additional configuration switches that control their behavior. These are indicated below as well. See Options to enable/disable specific invariants.

AndJoiner

This is a special invariant used internally by Daikon to represent an antecedent invariant in an implication where that antecedent consists of two invariants anded together.

CommonFloatSequence

Represents sequences of double values that contain a common subset. Prints as ‘{e1, e2, e3, ...} subset of x[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.CommonFloatSequence.enabled’.

See also the following configuration option:

CommonSequence

Represents sequences of long values that contain a common subset. Prints as ‘{e1, e2, e3, ...} subset of x[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.CommonSequence.enabled’.

See also the following configuration option:

CommonStringSequence

Represents string sequences that contain a common subset. Prints as "{s1, s2, s3, ...} subset of x[]".

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.stringsequence.CommonStringSequence.enabled’.

CompleteOneOfScalar

Tracks every unique value and how many times it occurs.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.scalar.CompleteOneOfScalar.enabled’.

CompleteOneOfString

Tracks every unique value and how many times it occurs.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.string.CompleteOneOfString.enabled’.

DummyInvariant

This is a special invariant used internally by Daikon to represent invariants whose meaning Daikon doesn’t understand. The only operation that can be performed on a DummyInvariant is to print it.

The main use for a dummy invariant is to represent a splitting condition that appears in a .spinfo file. The .spinfo file can indicate an arbitrary Java expression, which might not be equivalent to any invariant in Daikon’s grammar.

Ordinarily, Daikon uses splitting conditions to split data, then seeks to use that split data to form conditional invariants out of its standard built-in invariants. If you wish the expression in the .spinfo file to be printed as an invariant, then the configuration option ‘daikon.split.PptSplitter.dummy_invariant_level’ must be set, and formatting information must be supplied in the splitter info file.

EltLowerBound

Represents the invariant that each element of a sequence of long values is greater than or equal to a constant. Prints as ‘x[] elements >= c’.

See also the following configuration options:

EltLowerBoundFloat

Represents the invariant that each element of a sequence of double values is greater than or equal to a constant. Prints as ‘x[] elements >= c’.

See also the following configuration options:

EltNonZero

Represents the invariant "x != 0" where x represents all of the elements of a sequence of long. Prints as ‘x[] elements != 0’.

EltNonZeroFloat

Represents the invariant "x != 0" where x represents all of the elements of a sequence of double. Prints as ‘x[] elements != 0’.

EltOneOf

Represents sequences of long values where the elements of the sequence take on only a few distinct values. Prints as either ‘x[] == c’ (when there is only one value), or as ‘x[] one of {c1, c2, c3}’ (when there are multiple values).

See also the following configuration options:

EltOneOfFloat

Represents sequences of double values where the elements of the sequence take on only a few distinct values. Prints as either ‘x[] == c’ (when there is only one value), or as ‘x[] one of {c1, c2, c3}’ (when there are multiple values).

See also the following configuration option:

EltOneOfString

Represents sequences of String values where the elements of the sequence take on only a few distinct values. Prints as either ‘x[] == c’ (when there is only one value), or as ‘x[] one of {c1, c2, c3}’ (when there are multiple values).

See also the following configuration option:

EltRangeFloat.EqualMinusOne

Internal invariant representing double scalars that are equal to minus one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing

EltRangeFloat.EqualOne

Internal invariant representing double scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing

EltRangeFloat.EqualZero

Internal invariant representing double scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeFloat.GreaterEqual64

Internal invariant representing double scalars that are greater than or equal to 64. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing

EltRangeFloat.GreaterEqualZero

Internal invariant representing double scalars that are greater than or equal to 0. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing

EltRangeInt.BooleanVal

Internal invariant representing longs whose values are always 0 or 1. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeInt.Bound0_63

Internal invariant representing longs whose values are between 0 and 63. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

EltRangeInt.EqualMinusOne

Internal invariant representing long scalars that are equal to minus one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing

EltRangeInt.EqualOne

Internal invariant representing long scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing

EltRangeInt.EqualZero

Internal invariant representing long scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

EltRangeInt.Even

Invariant representing longs whose values are always even. Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf invariants it is printed.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.EltRangeInt.Even.enabled’.

EltRangeInt.GreaterEqual64

Internal invariant representing long scalars that are greater than or equal to 64. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing

EltRangeInt.GreaterEqualZero

Internal invariant representing long scalars that are greater than or equal to 0. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing

EltRangeInt.PowerOfTwo

Invariant representing longs whose values are always a power of 2 (exactly one bit is set). Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf invariants it is printed.

EltUpperBound

Represents the invariant that each element of a sequence of long values is less than or equal to a constant. Prints as ‘x[] elements <= c’.

See also the following configuration options:

EltUpperBoundFloat

Represents the invariant that each element of a sequence of double values is less than or equal to a constant. Prints as ‘x[] elements <= c’.

See also the following configuration options:

EltwiseFloatEqual

Represents equality between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] elements are equal’.

EltwiseFloatGreaterEqual

Represents the invariant ">=" between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] sorted by ">="’.

EltwiseFloatGreaterThan

Represents the invariant ">" between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] sorted by ">"’.

EltwiseFloatLessEqual

Represents the invariant "<=" between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] sorted by "<="’.

EltwiseFloatLessThan

Represents the invariant "<" between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as ‘x[] sorted by "<"’.

EltwiseIntEqual

Represents equality between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] elements are equal’.

EltwiseIntGreaterEqual

Represents the invariant ">=" between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] sorted by ">="’.

EltwiseIntGreaterThan

Represents the invariant ">" between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] sorted by ">"’.

EltwiseIntLessEqual

Represents the invariant "<=" between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] sorted by "<="’.

EltwiseIntLessThan

Represents the invariant "<" between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as ‘x[] sorted by "<"’.

Equality

Keeps track of sets of variables that are equal. Other invariants are instantiated for only one member of the Equality set, the leader. If variables ‘x’, ‘y’, and ‘z’ are members of the Equality set and ‘x’ is chosen as the leader, then the Equality will internally convert into binary comparison invariants that print as ‘x == y’ and ‘x == z’.

FloatEqual

Represents an invariant of "==" between two double scalars.

FloatGreaterEqual

Represents an invariant of ">=" between two double scalars.

FloatGreaterThan

Represents an invariant of ">" between two double scalars.

FloatLessEqual

Represents an invariant of "<=" between two double scalars.

FloatLessThan

Represents an invariant of "<" between two double scalars.

FloatNonEqual

Represents an invariant of "!=" between two double scalars.

FunctionBinary.BitwiseAndLong_{xyz, yxz, zxy}

Represents the invariant ‘x = BitwiseAnd (y, z)’ over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.BitwiseOrLong_{xyz, yxz, zxy}

Represents the invariant ‘x = BitwiseOr (y, z)’ over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.BitwiseXorLong_{xyz, yxz, zxy}

Represents the invariant ‘x = BitwiseXor (y, z)’ over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.DivisionLong_{xyz, xzy, yxz, yzx, zxy, zyx}

Represents the invariant ‘x = Division (y, z)’ over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.GcdLong_{xyz, yxz, zxy}

Represents the invariant ‘x = Gcd (y, z)’ over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.LogicalAndLong_{xyz, yxz, zxy}

Represents the invariant ‘x = LogicalAnd (y, z)’ over three long scalars. For logical operations, Daikon treats 0 as false and all other values as true. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.LogicalOrLong_{xyz, yxz, zxy}

Represents the invariant ‘x = LogicalOr (y, z)’ over three long scalars. For logical operations, Daikon treats 0 as false and all other values as true. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.LogicalXorLong_{xyz, yxz, zxy}

Represents the invariant ‘x = LogicalXor (y, z)’ over three long scalars. For logical operations, Daikon treats 0 as false and all other values as true. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.LshiftLong_{xyz, xzy, yxz, yzx, zxy, zyx}

Represents the invariant ‘x = Lshift (y, z)’ over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.MaximumLong_{xyz, yxz, zxy}

Represents the invariant ‘x = Maximum (y, z)’ over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.MinimumLong_{xyz, yxz, zxy}

Represents the invariant ‘x = Minimum (y, z)’ over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.ModLong_{xyz, xzy, yxz, yzx, zxy, zyx}

Represents the invariant ‘x = Mod (y, z)’ over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.MultiplyLong_{xyz, yxz, zxy}

Represents the invariant ‘x = Multiply (y, z)’ over three long scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinary.PowerLong_{xyz, xzy, yxz, yzx, zxy, zyx}

Represents the invariant ‘x = Power (y, z)’ over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.RshiftSignedLong_{xyz, xzy, yxz, yzx, zxy, zyx}

Represents the invariant ‘x = RshiftSigned (y, z)’ over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinary.RshiftUnsignedLong_{xyz, xzy, yxz, yzx, zxy, zyx}

Represents the invariant ‘x = RshiftUnsigned (y, z)’ over three long scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinaryFloat.DivisionDouble_{xyz, xzy, yxz, yzx, zxy, zyx}

Represents the invariant ‘x = Division (y, z)’ over three double scalars. Since the function is non-symmetric, all six permutations of the variables are checked.

FunctionBinaryFloat.MaximumDouble_{xyz, yxz, zxy}

Represents the invariant ‘x = Maximum (y, z)’ over three double scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinaryFloat.MinimumDouble_{xyz, yxz, zxy}

Represents the invariant ‘x = Minimum (y, z)’ over three double scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

FunctionBinaryFloat.MultiplyDouble_{xyz, yxz, zxy}

Represents the invariant ‘x = Multiply (y, z)’ over three double scalars. Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

GuardingImplication

This is a special implication invariant that guards any invariants that are over variables that are sometimes missing. For example, if the invariant ‘a.x = 0’ is true, the guarded implication is ‘a != null => a.x = 0’.

Implication

The Implication invariant class is used internally within Daikon to handle invariants that are only true when certain other conditions are also true (splitting).

IntEqual

Represents an invariant of "==" between two long scalars.

IntGreaterEqual

Represents an invariant of ">=" between two long scalars.

IntGreaterThan

Represents an invariant of ">" between two long scalars.

IntLessEqual

Represents an invariant of "<=" between two long scalars.

IntLessThan

Represents an invariant of "<" between two long scalars.

IntNonEqual

Represents an invariant of "!=" between two long scalars.

See also the following configuration option:

IsPointer

IsPointer is an invariant that heuristically determines whether an integer represents a pointer (a 32-bit memory address). Since both a 32-bit integer and an address have the same representation, sometimes a a pointer can be mistaken for an integer. When this happens, several scalar invariants are computed for integer variables. Most of them would not make any sense for pointers. Determining whether a 32-bit variable is a pointer can thus spare the computation of many irrelevant invariants.

The basic approach is to discard the invariant if any values that are not valid pointers are encountered. By default values between -100,000 and 100,00 (except 0) are considered to be invalid pointers. This approach has been experimentally confirmed on Windows x86 executables.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.scalar.IsPointer.enabled’.

LinearBinary

Represents a Linear invariant between two long scalars ‘x’ and ‘y’, of the form ‘ax + by + c = 0’. The constants ‘a’, ‘b’ and ‘c’ are mutually relatively prime, and the constant ‘a’ is always positive.

LinearBinaryFloat

Represents a Linear invariant between two double scalars ‘x’ and ‘y’, of the form ‘ax + by + c = 0’. The constants ‘a’, ‘b’ and ‘c’ are mutually relatively prime, and the constant ‘a’ is always positive.

LinearTernary

Represents a Linear invariant over three long scalars ‘x’, ‘y’, and ‘z’, of the form ‘ax + by + cz + d = 0’. The constants ‘a’, ‘b’, ‘c’, and ‘d’ are mutually relatively prime, and the constant ‘a’ is always positive.

LinearTernaryFloat

Represents a Linear invariant over three double scalars ‘x’, ‘y’, and ‘z’, of the form ‘ax + by + cz + d = 0’. The constants ‘a’, ‘b’, ‘c’, and ‘d’ are mutually relatively prime, and the constant ‘a’ is always positive.

LowerBound

Represents the invariant ‘x >= c’, where ‘c’ is a constant and ‘x’ is a long scalar.

See also the following configuration options:

LowerBoundFloat

Represents the invariant ‘x >= c’, where ‘c’ is a constant and ‘x’ is a double scalar.

See also the following configuration options:

Member

Represents long scalars that are always members of a sequence of long values. Prints as ‘x in y[]’ where ‘x’ is a long scalar and ‘y[]’ is a sequence of long.

MemberFloat

Represents double scalars that are always members of a sequence of double values. Prints as ‘x in y[]’ where ‘x’ is a double scalar and ‘y[]’ is a sequence of double.

MemberString

Represents String scalars that are always members of a sequence of String values. Prints as ‘x in y[]’ where ‘x’ is a String scalar and ‘y[]’ is a sequence of String.

Modulus

Represents the invariant ‘x == r (mod m)’ where ‘x’ is a long scalar variable, ‘r’ is the (constant) remainder, and ‘m’ is the (constant) modulus.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.scalar.Modulus.enabled’.

NoDuplicates

Represents sequences of long that contain no duplicate elements. Prints as ‘x[] contains no duplicates’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.NoDuplicates.enabled’.

NoDuplicatesFloat

Represents sequences of double that contain no duplicate elements. Prints as ‘x[] contains no duplicates’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.NoDuplicatesFloat.enabled’.

NonModulus

Represents long scalars that are never equal to r (mod m) where all other numbers in the same range (i.e., all the values that x doesn’t take from min(x) to max(x)) are equal to r (mod m). Prints as ‘x != r (mod m)’, where ‘r’ is the remainder and ‘m’ is the modulus.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.scalar.NonModulus.enabled’.

NonZero

Represents long scalars that are non-zero. Prints as ‘x != 0’, or as ‘x != null’ for pointer types.

NonZeroFloat

Represents double scalars that are non-zero. Prints as ‘x != 0’.

NumericFloat.Divides

Represents the divides without remainder invariant between two double scalars. Prints as ‘x % y == 0’.

NumericFloat.Square

Represents the square invariant between two double scalars. Prints as ‘x = y**2’.

NumericFloat.ZeroTrack

Represents the zero tracks invariant between two double scalars; that is, when ‘x’ is zero, ‘y’ is also zero. Prints as ‘x = 0 ==> y = 0’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoScalar.NumericFloat.ZeroTrack.enabled’.

NumericInt.BitwiseAndZero

Represents the BitwiseAnd == 0 invariant between two long scalars; that is, ‘x’ and ‘y’ have no bits in common. Prints as ‘x & y == 0’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoScalar.NumericInt.BitwiseAndZero.enabled’.

NumericInt.BitwiseComplement

Represents the bitwise complement invariant between two long scalars. Prints as ‘x = ~y’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoScalar.NumericInt.BitwiseComplement.enabled’.

NumericInt.BitwiseSubset

Represents the bitwise subset invariant between two long scalars; that is, the bits of ‘y’ are a subset of the bits of ‘x’. Prints as ‘x = y | x’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoScalar.NumericInt.BitwiseSubset.enabled’.

NumericInt.Divides

Represents the divides without remainder invariant between two long scalars. Prints as ‘x % y == 0’.

NumericInt.ShiftZero

Represents the ShiftZero invariant between two long scalars; that is, ‘x’ right-shifted by ‘y’ is always zero. Prints as ‘x >> y = 0’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoScalar.NumericInt.ShiftZero.enabled’.

NumericInt.Square

Represents the square invariant between two long scalars. Prints as ‘x = y**2’.

NumericInt.ZeroTrack

Represents the zero tracks invariant between two long scalars; that is, when ‘x’ is zero, ‘y’ is also zero. Prints as ‘x = 0 ==> y = 0’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoScalar.NumericInt.ZeroTrack.enabled’.

OneOfFloat

Represents double variables that take on only a few distinct values. Prints as either ‘x == c’ (when there is only one value) or as ‘x one of {c1, c2, c3}’ (when there are multiple values).

See also the following configuration option:

OneOfFloatSequence

Represents double[] variables that take on only a few distinct values. Prints as either ‘x == c’ (when there is only one value) or as ‘x one of {c1, c2, c3}’ (when there are multiple values).

See also the following configuration option:

OneOfScalar

Represents long scalars that take on only a few distinct values. Prints as either ‘x == c’ (when there is only one value), ‘x one of {c1, c2, c3}’ (when there are multiple values), or ‘x has only one value’ (when ‘x’ is a hashcode (pointer) - this is because the numerical value of the hashcode (pointer) is uninteresting).

See also the following configuration options:

OneOfSequence

Represents long[] variables that take on only a few distinct values. Prints as either ‘x == c’ (when there is only one value) or as ‘x one of {c1, c2, c3}’ (when there are multiple values).

See also the following configuration options:

OneOfString

Represents String variables that take on only a few distinct values. Prints as either ‘x == c’ (when there is only one value) or as ‘x one of {c1, c2, c3}’ (when there are multiple values).

See also the following configuration option:

OneOfStringSequence

Represents String[] variables that take on only a few distinct values. Prints as either ‘x == c’ (when there is only one value) or as ‘x one of {c1, c2, c3}’ (when there are multiple values).

See also the following configuration option:

PairwiseFloatEqual

Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] == y[]’.

PairwiseFloatGreaterEqual

Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] >= y[]’.

PairwiseFloatGreaterThan

Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] > y[]’.

PairwiseFloatLessEqual

Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] <= y[]’.

PairwiseFloatLessThan

Represents an invariant between corresponding elements of two sequences of double values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] < y[]’.

PairwiseIntEqual

Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] == y[]’.

PairwiseIntGreaterEqual

Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] >= y[]’.

PairwiseIntGreaterThan

Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] > y[]’.

PairwiseIntLessEqual

Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] <= y[]’.

PairwiseIntLessThan

Represents an invariant between corresponding elements of two sequences of long values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] < y[]’.

PairwiseLinearBinary

Represents a linear invariant (i.e., ‘y = ax + b’) between the corresponding elements of two sequences of long values. Each ‘(x[i], y[i])’ pair is examined. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’ and so forth. Prints as ‘y[] = a * x[] + b’.

PairwiseLinearBinaryFloat

Represents a linear invariant (i.e., ‘y = ax + b’) between the corresponding elements of two sequences of double values. Each ‘(x[i], y[i])’ pair is examined. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’ and so forth. Prints as ‘y[] = a * x[] + b’.

PairwiseNumericFloat.Divides

Represents the divides without remainder invariant between corresponding elements of two sequences of double. Prints as ‘x[] % y[] == 0’.

PairwiseNumericFloat.Square

Represents the square invariant between corresponding elements of two sequences of double. Prints as ‘x[] = y[]**2’.

PairwiseNumericFloat.ZeroTrack

Represents the zero tracks invariant between corresponding elements of two sequences of double; that is, when ‘x[]’ is zero, ‘y[]’ is also zero. Prints as ‘x[] = 0 ==> y[] = 0’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.PairwiseNumericFloat.ZeroTrack.enabled’.

PairwiseNumericInt.BitwiseAndZero

Represents the BitwiseAnd == 0 invariant between corresponding elements of two sequences of long; that is, ‘x[]’ and ‘y[]’ have no bits in common. Prints as ‘x[] & y[] == 0’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseAndZero.enabled’.

PairwiseNumericInt.BitwiseComplement

Represents the bitwise complement invariant between corresponding elements of two sequences of long. Prints as ‘x[] = ~y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseComplement.enabled’.

PairwiseNumericInt.BitwiseSubset

Represents the bitwise subset invariant between corresponding elements of two sequences of long; that is, the bits of ‘y[]’ are a subset of the bits of ‘x[]’. Prints as ‘x[] = y[] | x[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseSubset.enabled’.

PairwiseNumericInt.Divides

Represents the divides without remainder invariant between corresponding elements of two sequences of long. Prints as ‘x[] % y[] == 0’.

PairwiseNumericInt.ShiftZero

Represents the ShiftZero invariant between corresponding elements of two sequences of long; that is, ‘x[]’ right-shifted by ‘y[]’ is always zero. Prints as ‘x[] >> y[] = 0’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.PairwiseNumericInt.ShiftZero.enabled’.

PairwiseNumericInt.Square

Represents the square invariant between corresponding elements of two sequences of long. Prints as ‘x[] = y[]**2’.

PairwiseNumericInt.ZeroTrack

Represents the zero tracks invariant between corresponding elements of two sequences of long; that is, when ‘x[]’ is zero, ‘y[]’ is also zero. Prints as ‘x[] = 0 ==> y[] = 0’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.PairwiseNumericInt.ZeroTrack.enabled’.

PairwiseString.SubString

Represents the substring invariant between corresponding elements of two sequences of String. Prints as ‘x[] is a substring of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.PairwiseString.SubString.enabled’.

PairwiseStringEqual

Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] == y[]’.

PairwiseStringGreaterEqual

Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] >= y[]’.

PairwiseStringGreaterThan

Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] > y[]’.

PairwiseStringLessEqual

Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] <= y[]’.

PairwiseStringLessThan

Represents an invariant between corresponding elements of two sequences of String values. The length of the sequences must match for the invariant to hold. A comparison is made over each ‘(x[i], y[i])’ pair. Thus, ‘x[0]’ is compared to ‘y[0]’, ‘x[1]’ to ‘y[1]’, and so forth. Prints as ‘x[] < y[]’.

Positive

Represents the invariant ‘x &gt; 0’ where ‘x’ is a long scalar. This exists only as an example for the purposes of the manual. It isn’t actually used (it is replaced by the more general invariant LowerBound).

PrintableString

Represents a string that contains only printable ascii characters (values 32 through 126 plus 9 (tab)

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.string.PrintableString.enabled’.

RangeFloat.EqualMinusOne

Internal invariant representing double scalars that are equal to minus one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing

RangeFloat.EqualOne

Internal invariant representing double scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing

RangeFloat.EqualZero

Internal invariant representing double scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeFloat.GreaterEqual64

Internal invariant representing double scalars that are greater than or equal to 64. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing

RangeFloat.GreaterEqualZero

Internal invariant representing double scalars that are greater than or equal to 0. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing

RangeInt.BooleanVal

Internal invariant representing longs whose values are always 0 or 1. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeInt.Bound0_63

Internal invariant representing longs whose values are between 0 and 63. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

RangeInt.EqualMinusOne

Internal invariant representing long scalars that are equal to minus one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing

RangeInt.EqualOne

Internal invariant representing long scalars that are equal to one. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing

RangeInt.EqualZero

Internal invariant representing long scalars that are equal to zero. Used for non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

RangeInt.Even

Invariant representing longs whose values are always even. Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf invariants it is printed.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.scalar.RangeInt.Even.enabled’.

RangeInt.GreaterEqual64

Internal invariant representing long scalars that are greater than or equal to 64. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing

RangeInt.GreaterEqualZero

Internal invariant representing long scalars that are greater than or equal to 0. Used for non-instantiating suppressions. Will never print since Bound accomplishes the same thing

RangeInt.PowerOfTwo

Invariant representing longs whose values are always a power of 2 (exactly one bit is set). Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf invariants it is printed.

Reverse

Represents two sequences of long where one is in the reverse order of the other. Prints as ‘x[] is the reverse of y[]’.

ReverseFloat

Represents two sequences of double where one is in the reverse order of the other. Prints as ‘x[] is the reverse of y[]’.

SeqFloatEqual

Represents an invariant between a double scalar and a a sequence of double values. Prints as ‘x[] elements == y’ where ‘x’ is a double sequence and ‘y’ is a double scalar.

SeqFloatGreaterEqual

Represents an invariant between a double scalar and a a sequence of double values. Prints as ‘x[] elements >= y’ where ‘x’ is a double sequence and ‘y’ is a double scalar.

SeqFloatGreaterThan

Represents an invariant between a double scalar and a a sequence of double values. Prints as ‘x[] elements > y’ where ‘x’ is a double sequence and ‘y’ is a double scalar.

SeqFloatLessEqual

Represents an invariant between a double scalar and a a sequence of double values. Prints as ‘x[] elements <= y’ where ‘x’ is a double sequence and ‘y’ is a double scalar.

SeqFloatLessThan

Represents an invariant between a double scalar and a a sequence of double values. Prints as ‘x[] elements < y’ where ‘x’ is a double sequence and ‘y’ is a double scalar.

SeqIndexFloatEqual

Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as ‘x[i] == i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexFloatEqual.enabled’.

SeqIndexFloatGreaterEqual

Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as ‘x[i] >= i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexFloatGreaterEqual.enabled’.

SeqIndexFloatGreaterThan

Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as ‘x[i] > i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexFloatGreaterThan.enabled’.

SeqIndexFloatLessEqual

Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as ‘x[i] <= i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexFloatLessEqual.enabled’.

SeqIndexFloatLessThan

Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as ‘x[i] < i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexFloatLessThan.enabled’.

SeqIndexFloatNonEqual

Represents an invariant over sequences of double values between the index of an element of the sequence and the element itself. Prints as ‘x[i] != i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexFloatNonEqual.enabled’.

SeqIndexIntEqual

Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as ‘x[i] == i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexIntEqual.enabled’.

SeqIndexIntGreaterEqual

Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as ‘x[i] >= i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexIntGreaterEqual.enabled’.

SeqIndexIntGreaterThan

Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as ‘x[i] > i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexIntGreaterThan.enabled’.

SeqIndexIntLessEqual

Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as ‘x[i] <= i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexIntLessEqual.enabled’.

SeqIndexIntLessThan

Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as ‘x[i] < i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexIntLessThan.enabled’.

SeqIndexIntNonEqual

Represents an invariant over sequences of long values between the index of an element of the sequence and the element itself. Prints as ‘x[i] != i’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.unary.sequence.SeqIndexIntNonEqual.enabled’.

SeqIntEqual

Represents an invariant between a long scalar and a a sequence of long values. Prints as ‘x[] elements == y’ where ‘x’ is a long sequence and ‘y’ is a long scalar.

SeqIntGreaterEqual

Represents an invariant between a long scalar and a a sequence of long values. Prints as ‘x[] elements >= y’ where ‘x’ is a long sequence and ‘y’ is a long scalar.

SeqIntGreaterThan

Represents an invariant between a long scalar and a a sequence of long values. Prints as ‘x[] elements > y’ where ‘x’ is a long sequence and ‘y’ is a long scalar.

SeqIntLessEqual

Represents an invariant between a long scalar and a a sequence of long values. Prints as ‘x[] elements <= y’ where ‘x’ is a long sequence and ‘y’ is a long scalar.

SeqIntLessThan

Represents an invariant between a long scalar and a a sequence of long values. Prints as ‘x[] elements < y’ where ‘x’ is a long sequence and ‘y’ is a long scalar.

SeqSeqFloatEqual

Represents invariants between two sequences of double 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.

SeqSeqFloatGreaterEqual

Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as ‘x[] >= y[] lexically’.

If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqFloatGreaterThan

Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as ‘x[] > y[] lexically’.

If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqFloatLessEqual

Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as ‘x[] <= y[] lexically’.

If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqFloatLessThan

Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as ‘x[] < y[] lexically’.

If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntEqual

Represents invariants between two sequences of long 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.

SeqSeqIntGreaterEqual

Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as ‘x[] >= y[] lexically’.

If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntGreaterThan

Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as ‘x[] > y[] lexically’.

If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntLessEqual

Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as ‘x[] <= y[] lexically’.

If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqIntLessThan

Represents invariants between two sequences of long values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as ‘x[] < y[] lexically’.

If the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

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.

SeqSeqStringGreaterEqual

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 the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqStringGreaterThan

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 the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqStringLessEqual

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 the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

SeqSeqStringLessThan

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 the auxiliary information (e.g., order matters) doesn’t match between two variables, then this invariant cannot apply to those variables.

StdString.SubString

Represents the substring invariant between two String scalars. Prints as ‘x is a substring of y’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoString.StdString.SubString.enabled’.

StringEqual

Represents an invariant of "==" between two String scalars.

StringGreaterEqual

Represents an invariant of ">=" between two String scalars.

StringGreaterThan

Represents an invariant of ">" between two String scalars.

StringLessEqual

Represents an invariant of "<=" between two String scalars.

StringLessThan

Represents an invariant of "<" between two String scalars.

StringNonEqual

Represents an invariant of "!=" between two String scalars.

SubSequence

Represents two sequences of long values where one sequence is a subsequence of the other. Prints as ‘x[] is a subsequence of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.SubSequence.enabled’.

SubSequenceFloat

Represents two sequences of double values where one sequence is a subsequence of the other. Prints as ‘x[] is a subsequence of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.SubSequenceFloat.enabled’.

SubSet

Represents two sequences of long values where one of the sequences is a subset of the other; that is each element of one sequence appears in the other. Prints as either ‘x[] is a subset of y[]’ or as ‘x[] is a superset of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.SubSet.enabled’.

SubSetFloat

Represents two sequences of double values where one of the sequences is a subset of the other; that is each element of one sequence appears in the other. Prints as either ‘x[] is a subset of y[]’ or as ‘x[] is a superset of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.SubSetFloat.enabled’.

SuperSequence

Represents two sequences of long values where one sequence is a subsequence of the other. Prints as ‘x[] is a subsequence of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.SuperSequence.enabled’.

SuperSequenceFloat

Represents two sequences of double values where one sequence is a subsequence of the other. Prints as ‘x[] is a subsequence of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.SuperSequenceFloat.enabled’.

SuperSet

Represents two sequences of long values where one of the sequences is a subset of the other; that is each element of one sequence appears in the other. Prints as either ‘x[] is a subset of y[]’ or as ‘x[] is a superset of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.SuperSet.enabled’.

SuperSetFloat

Represents two sequences of double values where one of the sequences is a subset of the other; that is each element of one sequence appears in the other. Prints as either ‘x[] is a subset of y[]’ or as ‘x[] is a superset of y[]’.

This invariant is not enabled by default. See the configuration option ‘daikon.inv.binary.twoSequence.SuperSetFloat.enabled’.

UpperBound

Represents the invariant ‘x <= c’, where ‘c’ is a constant and ‘x’ is a long scalar.

See also the following configuration options:

UpperBoundFloat

Represents the invariant ‘x <= c’, where ‘c’ is a constant and ‘x’ is a double scalar.

See also the following configuration options:


Previous: Invariant list, Up: Daikon output   [Contents][Index]

5.6 Invariant filters

Invariant filters are used to suppress the printing of invariants that are true, but not considered “interesting” — usually because the invariants are considered obvious or redundant in a given context.

The following is a list of the invariant filters that Daikon supports. Each of these filters has a corresponding configuration enable switch; by default, all filters are enabled. See Options to enable/disable filters, for details.


Previous: Invariant list, Up: Daikon output   [Contents][Index]