Docs - random thoughts
Ferinko opened this issue · 2 comments
General comments on the docs.
you will also need to use the -s flag to specify which SMT solvers you would like to use for the testing
UX wise, maybe this could be transparent? As in, we set a default to -s z3 or some such and then -s will be an 'advanced' setting?
The following flags are able to added with
Typo.
Specifies conditions that must be true if the function returns.
For future reference: what if the function does not return 🤔 (rollbacks?). Nevertheless, would probably sound better 'when the function returns' to both implicitly assume it returns and make it clearer that it's at the point when the function does return, not 'if it returns anything', which fails to refer to said specific point in time.... or maybe I'm overthinking this and it's fine! :)
Restricts the initial state, value of logical variables, or set of possible inputs for which the postcondition must hold.
Maybe this shouldn't mention postcondition at all 🤔 .
Allows the introduction of logical variables.
Worth explaining they're variables to conveniently refer to (sub)expressions?
Allows claims to be made about the state of a storage variable before and after the function. ...
The entire section on logical variables is rough, but I think this simply stems from the confusing nature of the machinery we have implemented... this might warrant a rethink as to how we express these updates 🤔.
UX wise, maybe this could be transparent? As in, we set a default to -s z3 or some such and then -s will be an 'advanced' setting?
Yes, I like this. I'll handle it within #79 since it is a tiny change.
The entire section on logical variables is rough, but I think this simply stems from the confusing nature of the machinery we have implemented... this might warrant a rethink as to how we express these updates thinking.
I assume you mean storage variables? Agreed. I've tweaked it slightly, but I'll think more about how to make that better. Perhaps an example would be more clarifying.
The rest of your comments are addressed in 51db583.