Open ePaul opened 8 years ago
Hey Paulo,
Yes, verification is optional (at least at the moment).
Also, it does say this in the glossary:
It doesn't mention runtime or verification time though. It's not clear what should be said here. It might be too specific given the nature of modern compilers (e.g. incremental compilation, etc).
In the language specification it is not clearly mentioned that there are three phases, and how they depend on each other.
This is what I gathered (e.g. from the description of the
assert
andassume
andfail
statements):I first assumed those phased happen always in this order, and only verified code is actually run. But the description of
fail
tells me that it throws a fault at runtime, while the verifier makes sure it is not reachable. How can it then throw a fault? Same forassert
(which is basicallyif (! condition): fail
).Does this mean verification is optional?