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?
WhyML
-----
......@@ -40,6 +43,15 @@ WhyML
The type cast can then play the role of the "close" instruction.
Do we need it? What's the good syntax for open types?
- 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".
"false" would be a poor choice, as it could introduce inconsistency
in the WPs of the caller. Should we allow unhandled exceptions at all?
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment