Cyclic Type Invariants

[DavePearce]

(see also Whiley/WhileyCompiler#425)

There is an inherent problem with recursively defined types and properties. The following illustrates the smallest example I can come up with:

property valid(natarray arr)
// All elements are naturals
where all { i in 0..|arr| | arr[i] >= 0 }

type natarray is (int[] xs) where valid(xs)

The problem is that, on entry to valid() the interpreter currently checks that arr has type natarray and this causes it to recursively call itself infinitely. The fix is actually very easy. Just restate the property as follows:

property valid(int[] arr)
// All elements are naturals
where all { i in 0..|arr| | arr[i] >= 0 }

Now there is no loop!

[DavePearce]

As Whiley/WhileyCompiler#445 shows, this can arise for both property and function declarations. How do we check for this? Is this a sufficient characterisation:

• A type whose invariant indirectly accesses itself.

Therefore, to check for it, we start from types and their invariants and look for cycles. This must include indirect type invariant as well. Examples:

type X is (T y) where f(y)

property f(X x) where e

type Y is (T y) where f(y)
type X is (Y y)

property f(X x) where e

type X is (T y) where y is X

[DavePearce]

Next step: write up RFC