search

UoY-RoboStar / robochart-textual

This repository contains the plugins for the RoboChart textual editor
Eclipse Public License 2.0
0 stars 1 forks source link

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

Open MattWindsor91 opened 1 year ago

MattWindsor91 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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

MattWindsor91 commented 1 year ago

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 commented 1 year ago

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.