Missing PO on ordering predicates

[leouk]

There is a missing PO for ord/eq predicates. It should say "x <= y or y <= x", to ensure that the definition of eq+ord is total. Otherwise, things like "not <" will possibly fail in proofs.

[nickbattle]

I would like to see your example for this, but I'm guessing that it would be something like this:

types
    T = nat * nat
    eq a = b == a.#1 = b.#1;

Proof Obligation 3: (Unproved)
T: total order obligation in 'DEFAULT' (test.vdm) at line 2:5
(forall x:T, y:T & x <= y or y <= x)

This is now produced when a type definition includes either an eq clause or a ord clause (or both). It could perhaps have a better name ("total order" mean something else). Is that what is needed here?

The change is pushed to "development" if you want to try it.

There may be GUI work required to include this, not sure.

[leouk]

Yes, the missing PO is correct. The example that I have is like this

R :: 
        x: nat
        y: nat 
    eq mk_R(x1, -) = mk_R(x2, -) == **x1 <> x2**
    ord mk_R(x1, y1) < mk_R(x2, y2) == (x1 < x2) or (x1 = x2 and y1 < y2);  

This is "silly", but the point is that, given VDM's definition of total orders (e.g. eq + less), then the concern is what happens when you negate stuff that might be ill defined. (e.g. not r1 <= r2, is the same as r1 > r2, iff we've got a total order defined). For the example above, you get the silly counter example discovered by quick check as

Quickcheck found a counterexample:
  r1 = ⦇x = 0, y = 0⦈
  r2 = ⦇x = 0, y = 0⦈

By the way, would this be discoverable with our quickcheck?

[nickbattle]

OK, thanks for that example. I ran the same definition through our own quickcheck, and you get this:

> qc -c
Created 7 default ranges in ranges.qc. Check them! Then run 'qc'
> qc
Expanding 7 ranges:
.......
Ranges expanded in 0.153s
PO# 1, PASSED in 0.012s
PO# 2, FAILED in 0.0s: Counterexample: x = mk_R(0, 0)
R: equivalence relation obligation in 'DEFAULT' (test.vdm) at line 5:8
(forall x:R & eq_R(x, x))
    and (forall x:R, y:R & eq_R(x, y) => eq_R(y, x))
    and (forall x:R, y:R, z:R & eq_R(x, y) and eq_R(y, z) => eq_R(x, z))

PO# 3, PASSED in 0.013s
PO# 4, PASSED in 0.112s
PO# 5, FAILED in 0.0s: Counterexample: y = mk_R(0, 0), x = mk_R(0, 0)
R: total order obligation in 'DEFAULT' (test.vdm) at line 2:5
(forall x:R, y:R & x <= y or y <= x)

> 

So yes, I think that caught the same counterexample, as well as tripping up on the equivalence relation PO.

[leouk]

Yep. Nice.I tried running qc but command wasn’t registered. Anything specific to do here to play with it?

[nickbattle]

Quickcheck is a plugin, so you have to have the jar on your classpath. But that should be all.

I think the latest vdmsl.sh includes it?

[kgpierce]

This has been added and checked.