Daikon output (The Daikon Invariant Detector User Manual)

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.

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 (https://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 https://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 is 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, https://www.cs.ucf.edu/~leavens/JML/); for details, see the JML Manual. JML format lets you use the various JVM tools on Daikon invariants, including run-time 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.

CSharpContract format

Produces C# output for use with Microsoft’s Code Contracts https://www.microsoft.com/en-us/research/project/code-contracts/. The format employs some extension/utility methods to improve contract readability; the library containing these methods can be found at https://github.com/twschiller/daikon-code-contract-extensions.

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.

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 Class.getName format: one character for each primitive type (‘B’ for byte, ‘C’ for character, ‘Z’ for boolean, etc.); ‘Lclassname;’ for object types; and a ‘[’ prefix for each level of array nesting.

5.2.1 OBJECT and CLASS program points

Two 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.)

A trace file does not contain samples for the :::OBJECT and :::CLASS program points. Variable values for these artificial program points are constructed from samples that do appear in a trace file. For example, an object invariant is a property that holds at entry to and exit from every public method of the class, so the :::OBJECT program point is constructed from samples at those points.

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 multidimensional arrays or structures, but such data structures can be represented as scalars and arrays by choosing variable names that indicate their relationship.)

a[i] array access. a and i are themselves arbitrary variable names, of array and integral type, respectively.
a[-1] from-end array access. a[-1] denotes the last element of array a; it is syntactic sugar for a[a.length-1].
a[] array contents. For array-valued expression a, all of its elements, as a sequence. Simply using the expression a means the identity (address or hashcode) of the array, not a list of its elements. For two arrays a and b, ‘a=b’ implies ‘a[]=b[]’, but ‘a[]=b[]’ does not imply ‘a=b’.
x.y, x->y field access. When field access is applied to a structure/class, it has the usual meaning of selecting one field from the structure/class.
When field access is applied to an array, it means to map the field access across the elements of the array. For example, if a is an array, then a[].foo is the sequence consisting of the foo fields of each of the elements of a. Likewise, a[].foo.bar contains the bar fields of a[].foo. By contrast, a.foo does not make sense, because one cannot ask for the foo field of an address, and a[].foo[] would be a two-dimensional array.
As in Java, x.getClass() is the run-time type of x, which may differ from its declared type.
a.length is the length (number of elements) of array a; this is not necessarily the number of initialized or used elements.
s.toString is the string value of String s, namely a sequence of characters.
Classname.varname static class variable. Static variables of a class have names of the form ‘classname.varname’
orig(x) refers to the value of variable x upon entry to a procedure (because the procedure body might modify the value of x). These variables appear only at :::EXIT program points. Typically, orig() variables do not appear in the trace, but are automatically created by Daikon when it matches up :::ENTER and :::EXITnn program points. See orig variable example.
This variable prints as orig when using Daikon output format (see Invariant syntax), but may print differently in other formats (such as \old).
post(x) refers to the value of variable x upon exit from a procedure. Such a value is usually written simply x; the post prefix is needed only within an orig expression, when the post-state value needs to be referenced. Just as orig may be used only in a post-state context and specifies an expression to be evaluated in the ‘pre-state’, post may be used only in a ‘pre-state’ context and specifies an expression to be evaluated in the post-state. See orig variable example.
/globalVar C global variable. In C output, global variables with external linkage are prefixed with a slash. For instance, global /x is distinct from procedure parameter /x. (In Java programs, variables can be distinguished by prefixing them with this. or, for class-static variables, a class name.)
myfile_c/staticVar C static variable. In C output, file-static variables have names of the form ‘filename/varname’, where periods (‘.’) in the filename are converted into underscores (‘_’). For example, ‘Global_c/x’ is the name for a file-static variable x declared in the file Global.c).
myfile_c@funcname/funcStaticVar C function-scoped static variable. In C output, for static variables which are declared within functions, an at-sign ‘@’ separates the filename and the function name and then a slash separates the function name and variable name (e.g., ‘Global_c@main/funcStaticVar’ for a static variable funcStaticVar declared within the function main in the file Global.c).

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.)

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]

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 if ‘a.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).

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.)

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.

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, the “has only one value” output 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.

5.4.4 Object inequality

Daikon may report ‘x < y’ where the operator ‘<’ is not applicable to the type of ‘x’ and ‘y’, as in ‘myString < otherString’.

In this case, the invariant means that the first expression is always less than the second, according to the ‘Comparable.compareTo’ method.

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:

‘daikon.inv.unary.sequence.CommonFloatSequence.hashcode_seqs’

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:

‘daikon.inv.unary.sequence.CommonSequence.hashcode_seqs’

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. Prints as x has values: v1 v2 v3 ....

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. Prints as either x has no values or as x has values: "v1" "v2" "v3" ....

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. In particular, the invariant cannot be tested against a sample: the invariant is always assumed to hold and is always considered to be statistically justified.

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, whether or not it is itself discovered by Daikon during invariant detection, 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:

‘daikon.inv.unary.sequence.EltLowerBound.minimal_interesting’
‘daikon.inv.unary.sequence.EltLowerBound.maximal_interesting’

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:

‘daikon.inv.unary.sequence.EltLowerBoundFloat.minimal_interesting’
‘daikon.inv.unary.sequence.EltLowerBoundFloat.maximal_interesting’

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[] elements == c (when there is only one value), or as x[] elements one of {c1, c2, c3} (when there are multiple values).

May print as x[] elements has only one value when x is an array of hashcodes (pointers) – this is because the numerical value of the hashcode (pointer) is uninteresting.

See also the following configuration options:

‘daikon.inv.unary.sequence.EltOneOf.size’
‘daikon.inv.unary.sequence.EltOneOf.omit_hashcode_values_Simplify’

EltOneOfFloat

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

See also the following configuration option:

‘daikon.inv.unary.sequence.EltOneOfFloat.size’

EltOneOfString

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

See also the following configuration option:

‘daikon.inv.unary.stringsequence.EltOneOfString.size’

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. Prints as x is even.

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. Prints as x is a power of 2.

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:

‘daikon.inv.unary.sequence.EltUpperBound.minimal_interesting’
‘daikon.inv.unary.sequence.EltUpperBound.maximal_interesting’

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:

‘daikon.inv.unary.sequence.EltUpperBoundFloat.minimal_interesting’
‘daikon.inv.unary.sequence.EltUpperBoundFloat.maximal_interesting’

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. Prints as x == y.

FloatGreaterEqual

Represents an invariant of >= between two double scalars. Prints as x >= y.

FloatGreaterThan

Represents an invariant of > between two double scalars. Prints as x > y.

FloatLessEqual

Represents an invariant of <= between two double scalars. Prints as x <= y.

FloatLessThan

Represents an invariant of < between two double scalars. Prints as x < y.

FloatNonEqual

Represents an invariant of != between two double scalars. Prints as x != y.

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. Prints as x == y.

IntGreaterEqual

Represents an invariant of >= between two long scalars. Prints as x >= y.

IntGreaterThan

Represents an invariant of > between two long scalars. Prints as x > y.

IntLessEqual

Represents an invariant of <= between two long scalars. Prints as x <= y.

IntLessThan

Represents an invariant of < between two long scalars. Prints as x < y.

IntNonEqual

Represents an invariant of != between two long scalars. Prints as x != y.

See also the following configuration option:

‘daikon.inv.binary.twoScalar.IntNonEqual.integral_only’

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,000 (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:

‘daikon.inv.unary.scalar.LowerBound.minimal_interesting’
‘daikon.inv.unary.scalar.LowerBound.maximal_interesting’

LowerBoundFloat

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

See also the following configuration options:

‘daikon.inv.unary.scalar.LowerBoundFloat.minimal_interesting’
‘daikon.inv.unary.scalar.LowerBoundFloat.maximal_interesting’

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:

‘daikon.inv.unary.scalar.OneOfFloat.size’

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:

‘daikon.inv.unary.sequence.OneOfFloatSequence.size’

OneOfScalar

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).

May print as 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:

‘daikon.inv.unary.scalar.OneOfScalar.size’
‘daikon.inv.unary.scalar.OneOfScalar.omit_hashcode_values_Simplify’

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:

‘daikon.inv.unary.sequence.OneOfSequence.size’
‘daikon.inv.unary.sequence.OneOfSequence.omit_hashcode_values_Simplify’

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:

‘daikon.inv.unary.string.OneOfString.size’

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:

‘daikon.inv.unary.stringsequence.OneOfStringSequence.size’

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

PairwiseFloatGreaterThan

PairwiseFloatLessEqual

PairwiseFloatLessThan

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

PairwiseIntGreaterThan

PairwiseIntLessEqual

PairwiseIntLessThan

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

PairwiseStringGreaterThan

PairwiseStringLessEqual

PairwiseStringLessThan

Positive

Represents the invariant x > 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. Prints as x is even.

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

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[].