Counterexample Failure

[DavePearce]

The following illustrates some kind of failure in counter-example generation:

type nat is (int x) where x >= 0

function f() -> (int r)
ensures r < -1:
    //
    nat i = 0
    //
    return 0

The problem is that, when counter example generation is activated, it fails to report a compile-time error. Running from the command-line is helpful:

./test.whiley:8: postcondition not satisfied
    return 0
    ^^^^^^^^
Exception in thread "main" java.lang.NullPointerException
        at wyal.util.WyalFileResolver.getWyalFile(Unknown Source)
        at wyal.util.WyalFileResolver.nonLocalNameLookup(Unknown Source)
        at wyal.util.WyalFileResolver.resolve(Unknown Source)
        ...
        at wyal.util.Interpreter.evaluateInvoke(Unknown Source)
        ...
        at wyc.command.Compile.findCounterexamples(Compile.java:445)

An exception is arising and this is likely the culprit. But, it's not clear why!

[DavePearce]

UPDATE: one interesting thing is that changing nat i = 0 to int i = 0 and it works out fine. Based on that, here's another example which is failing in the same way:

function f() -> (int r)
ensures r < -1:
    //
    int i = 0
    //
    return f()+1

It seems like any kind of resolution from within the interpreter during counterexample generation is doomed.

[DavePearce]

The minimal WyAL which causes the problem is this:

type nat is (int x)
where:
    x >= 0

assert:
    forall(nat i):
        if:
            i == 0
        then:
            i < -1

[DavePearce]

Have fixed case for constrained types, but not function invocations. The latter is more complex because we need to examine the return type. Furthermore, we ideally need to record what decision we made here.

[DavePearce]

This test case is also failing for reasons unknown:

type nat is (int x) where x >= 0

function f(int x) -> (int r)
ensures r <= 2:
    //
    return x+1

Looks like the problem is another exception raised here:

Exception in thread "main" java.lang.NullPointerException
        at wybs.util.AbstractSyntacticHeap.internalAllocate(Unknown Source)
        at wybs.util.AbstractSyntacticHeap.allocate(Unknown Source)

[DavePearce]

Am closing this now, as remaining issues are "features" to be implemented.