VDMJ POG misses mutual recursion

[joey-coleman]

The following bug was originally reported on Sourceforge by nick_battle, 2009-09-28 11:49:09:

VDMJ's PO generator does not correctly identify mutually recursive functions, and so does not generate the associated POs (simply recursive functions are fine).

[joey-coleman]

Comment by nick_battle, 2013-05-31 20:59:03.978000:

Still in 2.0.0b2

[joey-coleman]

Comment by nick_battle, 2013-08-09 07:33:07.523000:

• Release: v2.0.0beta2 --> v2.0.0beta4

[joey-coleman]

Comment by nick_battle, 2013-08-27 15:49:14.814000:

• Release: v2.0.0beta4 --> v2.0.0beta5

[joey-coleman]

Comment by nick_battle, 2013-09-02 11:07:59.540000:

• Release: v2.0.0beta5 --> v2.0.0beta6

[joey-coleman]

Comment by nick_battle, 2013-10-16 07:09:53.290000:

• Release: v2.0.0beta6 --> v2.0.0

[joey-coleman]

Comment by nick_battle, 2013-10-16 07:09:53.828000:

Still in 2.0

[lausdahl]

Please add test case!

[nickbattle]

Here you go...

functions
    f: nat -> nat
    f(a) == if a = 0 then 0 else g(a-1)
    measure id;

    g: nat -> nat
    g(a) == if a = 0 then 0 else f(a-1)
    measure id;

    id: nat -> nat
    id(a) == a;

That produces two subtype POs (for the a-1 on a nat), but no recursive POs. But we ought to prove that the mutually recurive f/g call sequence terminates by using their measures (via a PO).

[nickbattle]

This ought to be possible by creating a variation of the cyclic dependency searching that the type checker does - mutually recursive function calls look like cyclic dependencies (in fact they are unless they are protected by conditionals). So we probably need a slightly different visitor to search for function applications (regardless of conditionals), then find loops (possibly of n>2?) and produce the POs from that.

[nickbattle]

I think the POs we should produce relate to the measure for the "current" function compared to that for the next in a mutually recursive cycle. This is a generalisation of what Augusto proposed in his MSc thesis: that considers mutual recursion between two functions, and describes a single PO that has no caller context:

forall x:nat & not(x=0) => id_even(x) > id_odd(x-1)
and
forall x:nat & not(x=0) => id_odd(x) > id_even(x-1)

This is valid, but it seems more natural to generate one obligation for each recursive call in the context of each caller. So the example would generate two POs:

even: recursive function obligation in 'DEFAULT' (test.vdm) at line 15:5
(forall x:nat &
  (not (x = 0) =>
    measure_odd(x) > measure_even((x - 1))))

odd: recursive function obligation in 'DEFAULT' (test.vdm) at line 5:5
(forall x:nat &
  (not (x = 0) =>
    measure_even(x) > measure_odd((x - 1))))

This then extends in a natural way to recursive cycles with an arbitrary number of functions, though it also changes the definition of what constitutes a recursive function (something that requires a measure), so the type checker has to change as well as the POG.

[nickbattle]

This is now working in VDMJ (4.3.0 build 200101 and later). Recursion has been generalised to be a cycle of functions that can call each other in a loop, with the simple case of a function calling itself as a minimal case. In general, if a function can be part of a cycle like [f, g, h, f, g, h...] then all members of the cycle ought to have a measure defined (a warning if not). Note that a single function can be a member of multiple cycles, because it may call several other functions that call back to it. The warnings indicate the cycles concerned (since it can be hard to see!).

In general, the test is that the measure value of the current invocation, is greater than that of the measure of the next function in the cycle, at the point that the 2nd function is called. The POs generated reflect this.

Currently, the runtime test of measures only tests the decreasing measure value of the current function (like simple recursion). This is because the admin overhead of tracking multiple measures for different cycles each on possibly different threads could become prohibitive. Since a cycle, by definition, returns to itself at regular intervals, and since all measures must be monotonically decreasing, and since each function in the cycle is tested, this is a reasonable compromise. But it means a recursion that has "gone rogue" might make one more loop before the measure error is caught at runtime.

A new error has been introduced since you cannot meaningfully compare measures from two functions in a cycle unless they all either return "nat" or the same sized nat tuple. So all of the measures in a cycle must now have the same return type.

The extra type checking overhead for calculating and analysing recursive cycles does not seem to be too onerous, though it is naturally greater for larger specifications.

I will start to port the change over to Overture's visitors...

[nickbattle]

I've just pushed a fix for this to ncb/development. It is basically the same as the fixes for VDMJ, though there are a couple of problems still.

One is that the visitor processing in Overture is somewhat slower than VDMJ, so (the worst example) the NewspeakSL test, which is nearly 3000 lines and is highly recursive, takes about 45 seconds to typecheck. It identifies large numbers of mutually recursive cycles, none of which has a measure. VDMJ checks this in about 7 seconds. To help with this, I've added a "skip.recursion.check" property which just does "simple" recursive checks, if set (ie. previous functionality).

The second problem is with VDM++ where, in some cases, it does not know the fully qualified type of an apply expression (like "name(nat, real)"), when the arguments make forward reference to definitions that are not yet resolved. In these cases, it fails to spot the recursive call currently. I'm trying to find out how to get round this (in VDMJ it is easier because the LexNameToken used in the apply is the same as the one used in its definition, so when that is updated, so are all of the copies).

I'll do some more testing and try to fix the problem above.

[nickbattle]

So now the 2nd problem is much better. I'm now looking up the name of the apply to get the resolved name before returning it as part of a cycle. That seems to solve it for the examples in the tests.

Still testing.

[nickbattle]

So this seems OK. I'm going to mark it as mergable, though it really needs thorough testing before release.

[nickbattle]

The algorithm was still missing some complex loop cases (now fixed), but this means that it takes even longer to check all of the possible loops in complex specs. I've now put a depth limit on the search: it will only identify loops that are less than 8 calls long (plus the original), for example:

Warning 5013: Mutually recursive cycle has no measure in 'DEFAULT' (test.vdm) at line 29:5
Cycle: [h, f, h]
Cycle: [h, f, g1, g2, g3, g4, g5, g6, h]
Warning 5013: Mutually recursive cycle has no measure in 'DEFAULT' (test.vdm) at line 2:5
Cycle: [f, g1, g2, g3, g4, g5, g6, h, f]
Cycle: [f, h, f]
etc.

This now checks complex specs in a fraction of a second. If you have loops longer than this... you won't get a warning.