UoY-RoboStar / robocert-textual

Textual plugin and CSP generator for RoboCert
Eclipse Public License 2.0
2 stars 0 forks source link

Add breakable loops #13

Open MattWindsor91 opened 3 years ago

MattWindsor91 commented 3 years ago

Per #12, we have at least one property where we want loops that we can break out of when some condition is met. The exact nature of the break isn't clear, but perhaps the best way to start would be manual breaking and then adding in more high-level control flow later?

Obviously, #11 blocks this.

MattWindsor91 commented 3 years ago

Lima's construct - introducing a break communication and using [| break |> on the outer level of the loop - should work here.

MattWindsor91 commented 3 years ago

Something that might be nice: loop ... until X, where X can be an arrow. This would effectively have the semantics of making the loop a sort-of loose gap.

Getting the semantics right for that might be tricky, though. We could always require that X is something that can be interrupted on, at which point it becomes a generalisation of how we would encode break. (Indeed, one could imagine loop until break to be a special case, though this seems a little awkwardly verbose).

MattWindsor91 commented 2 years ago

The current candidate break syntax is:

breaking from NAME:
    subsequence

I also propose syntactic sugar break from NAME as shorthand for

breaking from NAME:
    nothing