[Program Logic] Expectation Logic (eHoare)

What is it for?

eHoare is a program logic to bound the expectation of

How to use it?

The tactics work almost exactly as standard (possibilistic) Hoare tactics, except ...

blah    blih
------------
    bloh

Examples

See examples/ehoare.ec