Inconsistency with eq_T and ord_T signatures

[nickbattle]

When you define an "eq" or "ord" clause for a type, it creates eq_T, ord_T, max_T and min_T functions. The LRM says that these functions have the signature "T T +> bool" or "T T +> T", which is as you might expect. But actually both VDMJ and Overture create functions of this form:

types
    R ::
        a : nat
        b : nat
    eq r1 = r2 == r1 = r2
    ord r1 < r2 == r1.a < r2.a;

    T = nat
    eq t1 = t2 == t1 = t2
    ord t1 < t2 == t1 < t2;

> env
ord_R = (R * R +> bool)
max_R = (R * R +> R)
min_R = (R * R +> R)
ord_T = (nat * nat +> bool)     <--- NOTE
max_T = (T * T +> T)
min_T = (T * T +> T)
eq_T = (nat * nat +> bool)      <--- NOTE
eq_R = (R * R +> bool)
> 

Note that all of the functions use the type as a parameter apart from eq/ord of the named type T. The reason for this is that the eq and ord clauses shown simply compare their arguments, and if they were of type T that would recurse (stack overflow). So they are created using the RHS of the named type, "nat" in this case.

So firstly we have an inconsistency, since eq_R is defined in terms of Rs, and that stack overflows in the example above(!). You cannot directly compare records, so the ord_R function is OK, but again it is inconsistent with ordT's signature. The min/max_ functions are fine, as they are created internally rather than using a user clause.

Lastly, the LRM says that the signatures of these functions are all R R +> ... or T T +> ....

We need to be consistent, decide how to solve the "eq a = b == a = b" and "ord a < b == a < b" cases, and then maybe update the LRM (and possibly the tools!)

[tomooda]

The syntax is defined as

type definition = identifier, ‘=’, type, [ invariant ], [ eq clause ], [ ord clause ]
                  | identifier, ‘::’, field list, [ invariant ], [ eq clause ], [ ord clause ] ;

and I think ord_T must be typed as T * T +> bool because the ord clause is on the LHS of the type synonym.

For the infinite recursion, I think one good way is to pre-define eq_ that does the primitive equality comparision and use it in the body of the eq clause, just like the super call in Java. I'd also add you can process all those overloading resolutions before the execution by applying macro expansions (each instantiation of generic functions needs the macro expansions, too, in this case!).

[nickbattle]

At the moment, T = nat ord a < b == a < b would get turned into an explicit function definition like this:

ord_T: T * T +> bool
ord_T(a, b) == a < b;   <-- This recurses

I suppose we could include an implicit "let" before the body expression to re-define the types:

ord_T: T * T +> bool
ord_T(a', b') ==
    let a:nat = a', b:nat = b' in
        a < b;   <-- This is now ok

It's a bit more difficult with records because the rhs type would have to be composed:

eq_R: R * R +> bool
eq_R(a', b') ==
    let a:compose R' of x:nat y:nat end = a', b:compose R' of x:nat y:nat end = b' in
        a = b;   <-- This is now ok

[paulch42]

On a related point, the LRM (section 3.5) states the order relation must be a strict partial order. In that case, the type of the order relation must be T * T -> bool, not T * T +> bool. Similarly, the min and max functions can't be total.

This would then raise the question, should the equality function be total or partial. Again it is stated in the LRM (section 3.4) the defined equality must be total. However, note the default equality relation for a basic or compound type (sections 3.1 and 3.2) is always specified with the partial function type.

[nickbattle]

Incidentally, if we add an invariant clause to the types, we get these extra signatures:

inv_T(nat) = (nat +> bool)
inv_R(R) = (R +> bool)

Note that the one for T has arguments that match the RHS not T. But R is not the same(!), which has been a long standing problem. You can't test an R value using inv_R because in order to create the argument you have to have met the invariant anyway.

[tomooda]

not a solution but just an idea memo. how about

types
    R ::
        a : nat
        b : nat
    inv mk_R(a, b) == something;

deriving inv_R(R) = (nat*nat +> bool) I know this is infeasible because this would break backward compatibility.

[nickbattle]

We did consider something like that years ago when we first came across the problem. It doesn't really break compatibility in the sense that no one could really be using record invariants anyway!

[tomooda]

another idea is a postfix that tears down the inv, eq, ord clauses. I.e.

types
    R ::
        a : nat
        b : nat
    inv mk_R(a, b) == something;

is equivalent to

types
    R! ::
        a : nat
        b : nat;
    R = R! inv mk_R(a, b) == something;

deriving inv_R(R) = (R! +> bool) where ! is a postfix to tear down the inv, eq and ord clauses.

[pglvdm]

My recommendation would be that we everywhere would use the name of the type (also with records) for all these extra functions BUT with a semantics which states it does not recurse for all these generated functions (inv_T, eq_T and ord_T).

[nickbattle]

"With a semantics which states it does not recurse" sounds like a special evaluation mode that applies to (what?) specific typed expressions within a function body (perhaps carried into functions that it calls?), so that a = b or a < b has different semantics in different places. That sounds like trouble, since the same typed expression has different meanings depending on (what?) the call stack.

I think we have two distinct cases. First, the eq/ord case, where you could require the user to say let x':nat = x, y':nat = y in ... if they want to refer to RHS values, like eq a = b == a = b, though it isn't as easy with records. Second, the inv_T argument case, which is about how to apply the function, not so much what it does.

If we say that inv_T parameters are special and don't have the invariant applied, you still can never call the function explicitly except for legal values, since you have to create a T value to pass, which isn't in a special context. So I'm not sure how this helps? You could pass a nat value and say that wasn't converted to T, but that's effectively the same as saying it's inv_T: nat +> bool. And again it isn't as easy with record invariants.

Can you give some examples of how your idea would work?

[pglvdm]

If we take the original examples: types R :: a : nat b : nat eq r1 = r2 == r1 = r2 ord r1 < r2 == r1.a < r2.a;

T = nat
eq t1 = t2 == t1 = t2
ord t1 < t2 == t1 < t2;

env ord_R = (R R +> bool) max_R = (R R +> R) min_R = (R R +> R) ord_T = (nat nat +> bool) <--- NOTE max_T = (T T +> T) min_T = (T T +> T) eq_T = (nat nat +> bool) <--- NOTE eq_R = (R R +> bool)

I suggest to change ord_T = (nat nat +> bool) <--- NOTE to ord_T = (T T +> bool)
and eq_T = (nat nat +> bool) <--- NOTE to eq_T = (T T +> bool)
and then with the understanding for all implicitly generated functions the types of the generated functions are NOT checked... So e.g. for inv_R(a_r_record) does not check the argument type including its invariant (which would yield an infinite recursion).

[nickbattle]

To try to make progress with this, I've tried to implement a blend of Tomo's R! idea, together with Leo's observation at the LB meeting that other formalisms do this with "maximal" types and Peter's suggestion, which is similar. The development is in a branch called "maximal", so we can try it before committing(!).

So now, the implicit functions that require "maximal type" behaviour have T! parameter types. These are the same as T but do not include any invariant, equality or ordering clauses. The functions that don't care about this still have T parameters. If I add an invariant to each of the types in the original example, the signatures are now:

> env
ord_R = (R! * R! +> bool)
max_R = (R * R +> R)
min_R = (R * R +> R)
ord_T = (T! * T! +> bool)
max_T = (T * T +> T)
min_T = (T * T +> T)
eq_T = (T! * T! +> bool)
inv_T = (T! +> bool)
eq_R = (R! * R! +> bool)
inv_R = (R! +> bool)
>

In real use (ie. explicit calls to these) we are unlikely to pass R! values (how would you create one?), but to enable this I've extended the mk_R syntax to allow mk_R!, which creates an R! value. We may not need this though.

So now things behave as you would want, I think. You can call inv_T(123) even if T values are limited to <10 etc. You can also write equality and ordering clauses that refer to the same variables (without the eq/ord), like eq a = b == a = b and that won't blow the stack. The min/max functions behave as before.

I'm still testing some of the POG (subtyping is more complex), but it's looking reasonable too.

[nickbattle]

One problem here is that the eq_T and ord_T functions, with their T! parameters, will allow you to compare values that are not actually values of the type T. That makes sense for inv_T, because you deliberately want to be able to test non-T values. But for equality and ordering, I think it only makes sense to compare genuine T values. But we still want to suppress the eq/ord within the bodies of these functions, so that we avoid recursive problems. For example:

types
    T = nat
    inv t == t < 10
    ord a < b == a < b;

> p ord_T(1,2)
= true
Executed in 0.066 secs. 
> p ord_T(2,1)
= false
Executed in 0.004 secs. 
> p ord_T(100,200)       -- This ought to be an error?
= true
Executed in 0.002 secs. 
> p ord_T(200,100)      -- This ought to be an error?
= false
Executed in 0.003 secs. 
> 

So perhaps eq/ord functions ought to include pre inv_T(a) and inv_T(b) - that is, although the parameters are T! and so have no eq/ord behaviour, they are also valid T values.

[tomooda]

How about ord_T is typed T * T +> bool and therefore a and b are typed as T, but the interpreter upcasts a and b to T! in the right-hand side of the ord clause.

[nickbattle]

Yes, that might work Tomo. It's proving quite hard to generate the correct T! values to pass to inv_T in a precondition, given the parameter patterns for the ord clause can include ignore patterns. With an upcast, that would be easier, though it would need to be a special case in the type checker too, I think, which is a bit ugly.

I'll try it later :-)

[nickbattle]

Yes, that was much easier Tomo! :-) I've pushed the new version to "maximal". So now, the signatures are:

> env
ord_R = (R * R +> bool)
max_R = (R * R +> R)
min_R = (R * R +> R)
ord_T = (T * T +> bool)
max_T = (T * T +> T)
min_T = (T * T +> T)
eq_T = (T * T +> bool)
inv_T = (T! +> bool)
eq_R = (R * R +> bool)
inv_R = (R! +> bool)

So the only strangeness is with the inv_T, which makes more sense. Internally, the eq/ord functions do this:

let <pattern1> : T! = p1, <pattern2> : T! = p2 in <expression>

Where the p1/p2 are the normal "T" parameters to the function. That then binds the right variables, with maximal types if needed, for the evaluation of the body expression.

This is starting to look quite neat :-)

[nickbattle]

I think the only part of the LRM affected would be Section 3.3, "Invariants". Though we have to decide whether we want the T! type operator to be generally available - so specifiers can use it themselves. The "maximal" branch does have this enabled. It means the type parser allows T! for named types and records, and the mk_R! syntax is enabled to create maximal record values. That would need to be mentioned in the LRM too.

If we disable the parsing (or make it contingent on a property setting*), the inv/eq/ord functionality will still work transparently, though T! will always appear in the invariant signature.

* Which reminds me, the T! parsing ought to be limited to "vdm10"... will fix :-)

[nickbattle]

While we're here, we should also try to clear up Paul's earlier point: https://github.com/overturetool/language/issues/50#issuecomment-722249234

@leouk, does this sound right - regarding the partial ordering?

[nickbattle]

With Paul's correction for partiality on ordering, we get the following - note that eq is still total(?)

    T = nat
    inv t == t < 10
    eq a = b == a = b
    ord a < b == a < b;

> env
ord_T = (T * T -> bool)
max_T = (T * T -> T)
min_T = (T * T -> T)
eq_T = (T * T +> bool)
inv_T = (T! +> bool)
> 

Does that look right?

[nickbattle]

We may also need to review the POs in light of partiality?

> pog
Generated 6 proof obligations:

Proof Obligation 1: (Unproved)
T: total function obligation in 'DEFAULT' (test.vdm) at line 3:16
(forall t:T! &
  is_(inv_T(t), bool))

Proof Obligation 2: (Unproved)
T: invariant satisfiability obligation in 'DEFAULT' (test.vdm) at line 2:5
exists t : nat & (t < 10)

Proof Obligation 3: (Unproved)
T: total function obligation in 'DEFAULT' (test.vdm) at line 4:8
(forall p1:T, p2:T &
  is_(eq_T(p1, p2), bool))

Proof Obligation 4: (Unproved)
T: equivalence relation obligation in 'DEFAULT' (test.vdm) at line 4:8
(forall x:T & eq_T(x, x))
    and (forall x:T, y:T & eq_T(x, y) => eq_T(y, x))
    and (forall x:T, y:T, z:T & eq_T(x, y) and eq_T(y, z) => eq_T(x, z))

Proof Obligation 5: (Unproved)
T: strict order obligation in 'DEFAULT' (test.vdm) at line 5:9
(forall x:T & not ord_T(x, x))
    and (forall x:T, y:T, z:T & ord_T(x, y) and ord_T(y, z) => ord_T(x, z))

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

[leouk]

If we take the original examples: types R :: a : nat b : nat eq r1 = r2 == r1 = r2 ord r1 < r2 == r1.a < r2.a;

T = nat
eq t1 = t2 == t1 = t2
ord t1 < t2 == t1 < t2;

env ord_R = (R R +> bool) max_R = (R R +> R) min_R = (R R +> R) ord_T = (nat nat +> bool) <--- NOTE max_T = (T T +> T) min_T = (T T +> T) eq_T = (nat nat +> bool) <--- NOTE eq_R = (R R +> bool)

I suggest to change ord_T = (nat nat +> bool) <--- NOTE to ord_T = (T T +> bool) and eq_T = (nat nat +> bool) <--- NOTE to eq_T = (T T +> bool) and then with the understanding for all implicitly generated functions the types of the generated functions are NOT checked... So e.g. for inv_R(a_r_record) does not check the argument type including its invariant (which would yield an infinite recursion).

This is similar to what I do in the Isabelle translations

[leouk]

To try to make progress with this, I've tried to implement a blend of Tomo's R! idea, together with Leo's observation at the LB meeting that other formalisms do this with "maximal" types and Peter's suggestion, which is similar. The development is in a branch called "maximal", so we can try it before committing(!).

So now, the implicit functions that require "maximal type" behaviour have T! parameter types. These are the same as T but do not include any invariant, equality or ordering clauses. The functions that don't care about this still have T parameters. If I add an invariant to each of the types in the original example, the signatures are now:

> env
ord_R = (R! * R! +> bool)
max_R = (R * R +> R)
min_R = (R * R +> R)
ord_T = (T! * T! +> bool)
max_T = (T * T +> T)
min_T = (T * T +> T)
eq_T = (T! * T! +> bool)
inv_T = (T! +> bool)
eq_R = (R! * R! +> bool)
inv_R = (R! +> bool)
>

In real use (ie. explicit calls to these) we are unlikely to pass R! values (how would you create one?), but to enable this I've extended the mk_R syntax to allow mk_R!, which creates an R! value. We may not need this though.

So now things behave as you would want, I think. You can call inv_T(123) even if T values are limited to <10 etc. You can also write equality and ordering clauses that refer to the same variables (without the eq/ord), like eq a = b == a = b and that won't blow the stack. The min/max functions behave as before.

I'm still testing some of the POG (subtyping is more complex), but it's looking reasonable too.

I like the T! Mark, which is a clear capturing of the maximal aspect of the type. It’s use should be limited I would say.

One reason that comes to mind is that some operators over maximal type behaviour that creates problems in Z is negation. Oky, VDM doesn’t have something like the schema calculus but I can see things getting tricky.

The example is that in Z “not S” for a schema S, leads to the negation going all the way to the maximal type.

S == [ c: nat | c < 10 ]

Not S == [ c: Arithmos | c >= 10 or c < 0 ]

where artihmos is the largest/maximal numeric (super) type of all (nat, int, real, etc) types.

Hope this makes sense in terms of the cautionary tale on using T! Unchecked.

[leouk]

Yes, that was much easier Tomo! :-) I've pushed the new version to "maximal". So now, the signatures are:

> env
ord_R = (R * R +> bool)
max_R = (R * R +> R)
min_R = (R * R +> R)
ord_T = (T * T +> bool)
max_T = (T * T +> T)
min_T = (T * T +> T)
eq_T = (T * T +> bool)
inv_T = (T! +> bool)
eq_R = (R * R +> bool)
inv_R = (R! +> bool)

So the only strangeness is with the inv_T, which makes more sense. Internally, the eq/ord functions do this:

let <pattern1> : T! = p1, <pattern2> : T! = p2 in <expression>

Where the p1/p2 are the normal "T" parameters to the function. That then binds the right variables, with maximal types if needed, for the evaluation of the body expression.

This is starting to look quite neat :-)

Nick, the intention here is to deliberately not check the invariant for T on eq/ord right? This is important given some invariants can be quite costly and double checking them in this would be wasteful.

[leouk]

While we're here, we should also try to clear up Paul's earlier point: #50 (comment)

@leouk, does this sound right - regarding the partial ordering?

The VDM syntax (with eq and ord) defines a total order always, by definition (Ie you couldn’t avoid the order totality at all). So the PO for totality must always be there.

The point about partial x total function type on the ord/etc I would say they are partial (functions). If anything the values might fail the invariant say, for a valid check?

[leouk]

With Paul's correction for partiality on ordering, we get the following - note that eq is still total(?)

  T = nat
  inv t == t < 10
  eq a = b == a = b
  ord a < b == a < b;

> env
ord_T = (T * T -> bool)
max_T = (T * T -> T)
min_T = (T * T -> T)
eq_T = (T * T +> bool)
inv_T = (T! +> bool)
> 

Does that look right?

Does that mean invT gets checked at the entry of min/max/eq/ord? Earlier you mentioned p1/p2 let bound to T!, but here it shows as T?

Perhaps T is right, yet wasteful/slow given inv Will be checked anyway?

[leouk]

We may also need to review the POs in light of partiality?

> pog
Generated 6 proof obligations:

Proof Obligation 1: (Unproved)
T: total function obligation in 'DEFAULT' (test.vdm) at line 3:16
(forall t:T! &
  is_(inv_T(t), bool))

Proof Obligation 2: (Unproved)
T: invariant satisfiability obligation in 'DEFAULT' (test.vdm) at line 2:5
exists t : nat & (t < 10)

Proof Obligation 3: (Unproved)
T: total function obligation in 'DEFAULT' (test.vdm) at line 4:8
(forall p1:T, p2:T &
  is_(eq_T(p1, p2), bool))

Proof Obligation 4: (Unproved)
T: equivalence relation obligation in 'DEFAULT' (test.vdm) at line 4:8
(forall x:T & eq_T(x, x))
    and (forall x:T, y:T & eq_T(x, y) => eq_T(y, x))
    and (forall x:T, y:T, z:T & eq_T(x, y) and eq_T(y, z) => eq_T(x, z))

Proof Obligation 5: (Unproved)
T: strict order obligation in 'DEFAULT' (test.vdm) at line 5:9
(forall x:T & not ord_T(x, x))
    and (forall x:T, y:T, z:T & ord_T(x, y) and ord_T(y, z) => ord_T(x, z))

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

The total function bit does add an extra PO that might be overbearing (Ie I’d say +> for definitions isn’t necessary).

The total order is the one that’s inevitable, for catering for things like “not x <= y” being defined.

[nickbattle]

Thanks for those, Leo (it's sometimes easier to reply directly on the GitHub issue page, rather than replying to the email notifications? :-)

So you've raised a few points:

We should be careful about allowing a T! for users specifications, because it can lead to complications, such as the Z schema case you gave? Offering T! isn't essential, I think, but can you see a comparable situation where we get into trouble with VDM-SL?

Yes, the intention of the "implicit let" is to suppress the checks in the body of the test. That would have the effect of only evaluating invariants on the function parameters, and not again within the body. It's not for efficiency though: it's so that we can say ord a < b == a < b without recursing (because the RHS variables are T!).

The LRM says that ord must define a strict partial order, not a total order (Section 3.5). So if you've seen a reason why this can't be done, we'll have to update the LRM and the POs - currently, I think the POs are for a strict partial order. I think I read somewhere that the equality check that comes with that has to be total(?), but I would welcome a lot more clarity on this area! It's not difficult to get it right, but it's easy to get it wrong :-)

[leouk]

At first I can't think of an example; yet I can't think of a valid use outside the given need either?

Perhaps the percolation of checked for and unchecked for (invariant) types of Will if nothing else cause confusion to beginners?

On the strict partial and partial, you are right it's easy to get it wrong! Isabelle pushes towards partial order, so would have to encode the strict partial to see po consequences. My key concern is with things like "not x < y". Strict partial seems to prefer irreflexive and assimétric relations which are fine but more involved to prove. Will have a go in Isabelle and come back to you :-).

[nickbattle]

I'm sorry I won't be able to make the LB meeting at the weekend, but I would really like to try to progress this issue - the changes are available for experimentation in the "maximal" branch of VDMJ. We're so close, and this clear up some very long standing issues in VDM.

I think we need to decide whether the T! semantics is available for normal users or just implicit in certain generated functions, and we need to decide exactly the type of ordering (and hence POs) that the ord clause requires.

[nickbattle]

We placed an action of @leouk at the LB meeting today, to progress the type of sort we should enforce and hence the POs required.

[nickbattle]

So as suggested at today's LB meeting, I've pushed a change to the maximal branch that includes a new vdmj.parser.maximal_types property, that defaults to false. By default you cannot write T! or mk_R!, though these pling types may appear in the signatures of generated invariant functions. If the flag is set, you can enter these types and use them as expected.

I will draft an Appendix for the LRM when I get a minute :-)

[nickbattle]

Incidentally, we absolutely do need the ability to parse T! because when POs are generated for invariants that use them, they have to be parsed internally. The same happens when we generate the bodies of eq/ord functions. So all the new property does is make that parser feature available to normal users. I can explain this in the Appendix, which may help people understand what it's for.

[nickbattle]

Here is a suggestion for the LRM appendix text. Comments welcome...

Appendix A: Maximal Types

As described in section ??, type definitions that include inv, eq or ord clauses generate implicit functions, which can be used elsewhere in a specification. For example, the following type definition generates the implicit functions shown:

types
    T = nat
    inv t == t < 10
    eq t1 = t2 == t1 = t2
    ord t1 < t2 == t1 < t2;

ord_T = (T * T -> bool)
max_T = (T * T -> T)
min_T = (T * T -> T)
eq_T = (T * T +> bool)
inv_T = (T! +> bool)

However, the example above causes problems. Note that the equality and ordering clauses try to reflect the implicit rules for the underlying nat value (e.g. the eq comparison for two numbers t1 and t2 is just t1 = t2). When this is turned into the eq_T or ord_T functions, they would naively be defined as follows:

    eq_T: T * T +> bool
    eq_T(a, b) == a = b;

    ord_T: T * T -> bool
    ord_T(a, b) == a < b;

But an evaluation of these functions would produce an infinite recursion, because the body of both functions involves an eq/ord comparison of two T variables, which invokes the eq_T/ord_T function, and so on...

A similar situation occurs with the inv_T function, which is passed a value of type T. But in order to create a T value, the inv_T function must have been called (successfully), so calling inv_T(123) would try to call inv_T(123) to convert the 123 literal to a T value, which also produces an infinite recursion.

The solution to this problem is the use of "maximal types". For a type T, there is a maximal type T! which is the same, but without any invariant, equality or ordering constraints. If you look closely, the signature of inv_T shows that it actually takes a T! parameter. This type can accept any natural number, so the recursion is avoided.

The solution for equality and ordering also uses maximal types, but slightly differently. The two functions are actually generated as follows:

    eq_T: T * T +> bool
    eq_T(p1, p2) ==
        let a : T! = p1, b : T! = p2 in
            a = b;

    ord_T: T * T -> bool
    ord_T(p1, p2) ==
        let a : T! = p1, b : T! = p2 in
            a < b;

Notice that the "let" clauses convert the parameters to maximal types, which are then used to perform the check as the user specified without recursion.

Normally, maximal types are only used internally in this way, and it is illegal to use T! in a specification. However, it may be possible to enable the use of T! types in specification, depending on tool support.

[nickbattle]

@leouk we just need to agree the type of ordering that VDM's ord clause must implement, and hence what the POs are. Currently, we produce these:

types
    T = nat
    ord a < b == a < b;

Proof Obligation 1: (Unproved)
T: total function obligation in 'DEFAULT' (test.vdm) at line 3:9
(forall a:nat, b:nat &
  is_(ord_T(a, b), bool))

Proof Obligation 2: (Unproved)
T: strict order obligation in 'DEFAULT' (test.vdm) at line 3:9
(forall x:T & not ord_T(x, x)) and (forall x:T, y:T, z:T & ord_T(x, y) and ord_T(y, z) => ord_T(x, z))

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)

You had some views on this here: https://github.com/overturetool/language/issues/50#issuecomment-1501595576

[leouk]

@leouk we just need to agree the type of ordering that VDM's ord clause must implement, and hence what the POs are. Currently, we produce these:

types
  T = nat
  ord a < b == a < b;

Proof Obligation 1: (Unproved)
T: total function obligation in 'DEFAULT' (test.vdm) at line 3:9
(forall a:nat, b:nat &
  is_(ord_T(a, b), bool))

Proof Obligation 2: (Unproved)
T: strict order obligation in 'DEFAULT' (test.vdm) at line 3:9
(forall x:T & not ord_T(x, x)) and (forall x:T, y:T, z:T & ord_T(x, y) and ord_T(y, z) => ord_T(x, z))

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)

You had some views on this here: #50 (comment)

I see. With PO 3, which wasn't there before, the issue would go away, yes. Note that this would influence the definition of the eq_T (as well as ord_T) (i.e. you might want to warn the user that you need both really).

Just emphasise why this is crucial, we need to remember negation of the relation (not x <= y). If. the order is not total, this is not defined! I guess given VDM's semanatics, we could consider whether this is "optional" or not.

The experiment I worked on (which is here) considered the same POs on the VDM manual that you show here.

The concrete (counter)example, which highlights the problem is this one:

types 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 would fail the total order PO with the counter example mk_R(0,0).

PS: I don't yet see the total order on my VDMJ build. Likely need to rebuild it.

[nickbattle]

Folks,

Is there anything stopping me from merging this with the 4.5.0-SNAPSHOT that's in the works? There's a lot of other QuickCheck related work going on elsewhere and it's becoming a pain to merge/maintain the extra branch, if I can avoid it. We can still "sign off" on the whole thing and approve/edit the LRM appendix suggestion at the next LB (late November).

[pglvdm]

seen from my side that would be great...

[nickbattle]

The maximal branch has now been merged into the 4.5.0-SNAPSHOT. It will therefore make it into the next release (VDMJ 4.5.0), unless we take steps to prevent it.

[tomooda]

I created a pull request to the LRM. @nickbattle please check the PDF along with the bugfix of the measure function.

[nickbattle]

This looks great Tomo. One small quibble: should m be total in the "last" function (eg. ... +> nat)? In VDMJ, you get this, with measure len l:

fmap = ((@elem +> @elem) +> (seq of (@elem) +> seq of (@elem)))
measure_fmap = ((@elem +> @elem) +> (seq of (@elem) +> nat))

[nickbattle]

One other thing. Would you be able to fix the examples/VDMSL/ISO8601/Seq.vdmsl spec? Three measure functions should now be curried. This is the only example spec that needs to be fixed.

Was...

  size6[@a]: (@a * @a +> bool) * @a * seq of @a +> nat
  size6(-,-,s) == len s;

  size7[@a]: (@a * @a +> bool) * seq of @a +> nat
  size7(-,s) == len s;

  size8[@a]: (@a * @a +> bool) * seq of @a * seq of @a +> nat
  size8(-,s,t) == len s + len t;

Become...

  size6[@a]: (@a * @a +> bool) +> @a * seq of @a +> nat
  size6(-)(-, s) == len s;

  size7[@a]: (@a * @a +> bool) +> seq of @a +> nat
  size7(-)(s) == len s;

  size8[@a]: (@a * @a +> bool) +> seq of @a * seq of @a +> nat
  size8(-)(s, t) == len s + len t;

[tomooda]

@nickbattle thanks for the check. I pushed a fix to the PR.

[nickbattle]

Thanks Tomo. I edited the post above, a minute or two after posting, because I had got the parameter grouping wrong. I just tested the PR version of the file, but it fails because you're using my original version. Sorry about that. I'll add a comment to the PR too.

[tomooda]

Thanks Nick. It was my mistake. I read your edited version but didn't notice the parameter groupings. Anyway, it's now fixed. :-)

[nickbattle]

Thanks! I can confirm that the new version works perfectly :)

[tomooda]

merged :-) we can close this issue?

[nickbattle]

I think so. @kgpierce ?