diff options
Diffstat (limited to 'kvx/abstractbb/Impure/README.md')
| -rw-r--r-- | kvx/abstractbb/Impure/README.md | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/kvx/abstractbb/Impure/README.md b/kvx/abstractbb/Impure/README.md new file mode 100644 index 00000000..2b19d14a --- /dev/null +++ b/kvx/abstractbb/Impure/README.md @@ -0,0 +1,31 @@ +# `Impure`: importing OCaml functions as non-deterministic ones. + +The principle of this library is to encode the type `A -> B` of an +OCaml function as a type `A -> ?? B` in Coq, where `?? B` is the type +of an axiomatized monad that can be interpreted as `B -> Prop`. In +other word, this encoding abstracts an OCaml function as a function +returning a postcondition on its possible results (ie a relation between its +parameter and its result). Side-effects are simply ignored. And +reasoning on such a function is only possible in partial correctness. + +See further explanations and examples on [ImpureDemo](https://github.com/boulme/ImpureDemo). + +## Credits + +[Sylvain Boulmé](mailto:Sylvain.Boulme@univ-grenoble-alpes.fr). + +## Code Overview + +- [ImpMonads](ImpMonads.v) axioms of "impure computations" and some Coq models of these axioms. + +- [ImpConfig](ImpConfig.v) declares the `Impure` monad and defines its extraction. + +- [ImpCore](ImpCore.v) defines notations for the `Impure` monad and a `wlp_simplify` tactic (to reason about `Impure` functions in a Hoare-logic style). + +- [ImpPrelude](ImpPrelude.v) declares the data types exchanged with `Impure` oracles. + +- [ImpIO](ImpIO.v), [ImpLoops](ImpLoops.v), [ImpHCons](ImpHCons.v) declare `Impure` oracles and define operators from these oracles. + [ImpExtern](ImpExtern.v) exports all these impure operators. + +- [ocaml/](ocaml/) subdirectory containing the OCaml implementations of `Impure` oracles. + |