Towards refinement

[stevana]

Refinement is used by the Z/Event-B/TLA+ people as a way to not have to model the whole system in full detail at once. The father of Z/Event-B, Jean-Raymond Abrial, makes the analogy that if you think of a model as the blueprint (in the architecture/engineering sense), then refinement is a way to zoom in and get a more detailed view of the system.

A nice demo of how this plays out in Event-B is given by Abrial in the following video. I've started to port the example from the demo in the example/bank branch in order to better understand it.

I suspect that the necessary bits of the puzzle can be read off from the notion of morphism/(linear) simulation between indexed containers/interaction structures, but I don't see exactly how it all fits together yet.

I'll use this issue for notes. Any thoughts or comments are of course welcome!

[stevana]

Refinement of concurrent objects (via linearisability): www.cs.ox.ac.uk/people/hongseok.yang/paper/TCS10-concurrent-objects.pdf

[stevana]

On composing state machines a la Harel's state charts: https://gist.github.com/andymatuschak/d5f0a8730ad601bcccae97e8398e25b2

Also see:

• Typescript's state chart implementation: https://github.com/davidkpiano/xstate
• Python's state chart implementation: https://pypi.org/project/sismic/