ethereum
Describe the function preconditions in comments/docstrings
Issue
Pointed out by @franck44 and @protolambda, it would be more readable if we can more it clear of what are the preconditions of each function.
How to solve it
Add more detailed comments about the pre-conditions.
/cc @protolambda feel free to update this issue content. :)
It might be helpful to use Nagini to specify pre- and post-conditions (as well as other useful annotations).
It enriches statically-typed Python3 subset (PEP-484, mypy) with constructs to specify pre-conditions (Requires) and post-conditions (Ensures), exceptional post-conditions (Exsures), as well as invariants, function purity (@Pure), assertions, predicates, etc.
It uses Boogie and Z3 as Dafny, though it's underlying logic is different. However, the idea is to use its extensions to annotate the py-spec with pre-/post-conditions and other useful annotations (like @Pure).
One option can be to design a contract library based on the ideas of the Nagini contract library (e.g. one can express Dafny annotations instead of Viper ones).
Took a look Viper and Nagini today. Some quick notes:
- The verification system is great!
- Nagini requires input programs to comply to the static, nominal type system defined in PEP 484 as implemented in the Mypy, which means it requires remerkleable complies Mypy rules + #1707
- I'm worried that Nagini is not actively maintained. Since remerkleable has some complicated typing tricks, we may have some edge cases. (Sometimes, the issue is in
mypy)