Conversation
830f925 to
0a42fd7
Compare
|
what's an example use case for having the mode as a conclusion? |
Ghost-only functions would require ghost mode. |
so |
|
It seems that closures need something a bit more sophisticated than what I've written so far: the mode of a closure may be independent of the function it's passed to. |
| On built-in integer types, arithmetic operations are also safe: they may either panic | ||
| (in debug profiles) or perform wrapping operations (in release profiles). | ||
| Thus, in safety mode the precondition of these operations is `true` and | ||
| their postconditions are those of the wrapping operations. |
There was a problem hiding this comment.
A simpler solution is to keep the "won't overflow" precondition, because overflow of built-ins is undesirable basically always.
|
If we do that, we need to adapt the specifications of closures to take the mode as parameter. |
|
We need to discuss that directly. I think there is a direct way to encode all that (including safety) using first-class Booleans and without disabling preconditions in the safety mode. |
Yes, and that is why the logical functions |
| Hence, we follow different rules to determine verification conditions for proving | ||
| safety than for proving adherence to a contract. In safety mode: | ||
|
|
||
| 1. We ignore the contract of the function to verify: we don't assume preconditions, and we don't assert postconditions. |
There was a problem hiding this comment.
We already prove them in normal (non-safety) mode.
There was a problem hiding this comment.
So the same function would be proven in both modes?
cbea10a to
785419d
Compare
4 participants
Starting with a proposal for what they should look like, before implementing it.
Fixes #1532 (safety mode)
Fixes #1957 (termination mode)
Fixes #1940 (ghost mode)