Connect Floyd–Hoare (aka axiomatic) to game-theoretic semantics

[shingarov]

In refinement calculus 1, Floyd–Hoare "function-boundary" pre/postconditions are equivalent to intermittent assert/assume invariants. One generalization of this view is "assigning blame", or "who loses the game", if invariant is broken.

As one illustration, let's say Kasparov calls Karpov with argument x, and somewhere in Karpov's definitional code there is an intermittent assumption:

Karpov(x):
    ...
    assume(x>0)
    ...

Then if Kasparov calls Karpov(-1), Kasparov loses the game.

In the current codebase, only the assert side is implemented (and only in the "core OCaml" toy-language). This Issue calls to extend the implementation to the assume side.