Commit 8b41483f authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: TODO

parent ce0e29d8
......@@ -19,6 +19,9 @@ generic
integration of the library? This would require a special [raise] call:
why_raise e = raise (Why.Error e)
- the drivers cannot deal with theories defined in the .mlw files.
Otherwise why3 would report an error. Is it acceptable?
......@@ -40,6 +43,15 @@ WhyML
- we check the context type invariants around Eany, but not around
Eabstr, which is rather strange. Should Eabstr have preconditions?
If not, why should it post-ensure the invariants that didn't
necessarily hold before its execution? Probably, we shouldn't
add the context invariants to the outer spec of Eany.
- and what about return/raise invariants, should Eany and Eabstr
ensure them? (at the moment, they do)
- currently every unhandled exception has postcondition "true".
Markdown is supported
0% or
Finish editing this message first!
Please register or to comment