Model checking R/G programs in Alloy

When you run a program on your lap-top you "rely" on the operating system not letting any other program to interfere with your state space. But programs could be designed in a collaborative-style, with sub-programs helping each other over a shared state. (Example: on-the-fly garbage collection.)

Thus "no-interference" programming is just a special case of "allow-interference" programming. In the early 1980s, Cliff Jones proposed a dynamic extension to (static) Hoare logic: further to pre / post conditions, one could also specify interference of the environment via rely / guarantee conditions. Interest on R/G programming is growing a lot due to its potential for concurrency. But it has become clear that "allow-interference" programming has its subtleties, e.g. concerning non-termination.