Comparison operations can be chained, but lead to generator problems later

[MattWindsor91]

In one of my models, I have expressions of the form 0 <= x <= 180 where x is a nat. This validates ok, which led me to believe that the semantics would be equivalent to 0 <= x /\ x <= 180. csp-gen, however, generates the direct CSP translation ((0 <= x) <= 180), which is ill-formed CSP as it is comparing a Bool with an Int.

A read of the draft Z specification tells me that <= et al. are strictly mathematical toolkit relations with the type P(A × A), which would lead me to believe that if RoboChart's expression language is generally faithful to Z's then the validator or grammar should not be allowing this sort of expression. It might be that this chaining is intentional, in which case the CSP generator is at fault (and therefore I'd be happy to reopen the bug there).

[pefribeiro]

Hi @MattWindsor91, in what context is your expression being used? I just tried this in a condition and I get a type-checker error, as it should be?

[MattWindsor91]

Ah, apologies -- it's preconditions and postconditions in functions. I can see the type checker is, rightly, unable to determine a type in other positions.

[pefribeiro]

Ok, I think that's because there is no type-checking implemented for those.

[MattWindsor91]

That would make sense! Is type checking the pre/postconditions difficult, or something I could trivially PRQ in at some point? Presumably the former.

[pefribeiro]

I think that would be for @alvarohm to comment. I don't suppose it's difficult, but I think it may just have been that there was not sufficient coverage in the implementation, and so it could have precluded writing of more complex pre/postconditions.