v0.8.arrays.alpha2

Experimental support for contracts and arrays.

Kind 2 0.8 with experimental support for arrays

The basis of the extension of Lustre that we have implemented is to allow recursive (and implicitly quantified) array definitions in equations as such:

A[i] = if i = 0 then 2 else B[i - 1] ;

If n is the size of the array, this is semantically equivalent to the following formula:

∀ i ∈ [0; n]. ( i = 0 ⇒ A[i] = 2 ) ⋀ ( i ≠ 0 ⇒ A[i] = B[i-1] ).

The definition of A in the previous equation can also make use of A itself (as opposed to only pre A for variables which are not arrays) at the condition that the recursive definition is well formed. For instance,

A[i] = A[i];

will be rejected, whereas

A[i] = if i = 0 then 0 else A[i-1];

will not.

Specifications (properties, assertions, contracts) allow one to use quantifiers at the propositional level (not inside terms). For example, a property that specifies that the matrix M is symmetric can be written as

--%PROPERTY "M symmetric" forall (i, j: int) 0 <= i and i < n and 0 <= j and j < n => M[i][j] = M[j][i];

Finally the language allows to write parameterized (in the size of the arrays) problems by declaring the types of arrays as an unspecified constant (e.g., an input variable A : int ^ n;). Support for this feature is still preliminary. Kind 2 might diverge or stall because the underlying solvers do not terminate or fail.

We use several possible encodings for the arrays, the default one being to internally represent equations by quantified constraints. Some options allow to change this behavior:

• --smt_arrays to use the builtin theory of arrays in solvers
• --inline_arrays to eagerly instantiate quantifiers over array bounds when they are statically known
• --arrays_rec to use an encoding with recursive functions for arrays (this only works with option --smtsolver CVC4 before)

A more extensive description is available at https://github.com/kind2-mc/kind2/blob/develop/doc/usr/content/2_input/2_arrays.md .