Skip to content

[Program Logic] Expectation Logic (eHoare)

Francois Dupressoir edited this page Sep 21, 2023 · 3 revisions

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

Clone this wiki locally