On Wednesday, 30 July 2014 at 13:14:11 UTC, Daniel Murphy wrote:
For instance, if assert(false) is proven reachable then it
means either:
1. the specification is inconsistent/contradictory (thus wrong)
2. the program has been proved incorrect
The compiler should then refuse to generate code. If it is not
proven reachable then emitting HALT might be ok.
You say this as if it's a law of physics. One of the great
things about working on D is that we get to assign the
semantics that we decide are most useful, and don't have to
follow what other people have done.
It follows the law of logic:
http://en.wikipedia.org/wiki/Hoare_logic
http://en.wikipedia.org/wiki/Propositional_calculus
Any verifier for D would have to understand the semantics of
D's assert.
If D gets this it will be a general verifier adapted to D. That
follows the rules of established sound logic developed over the
past 2300 years.
All asserts should be established as either true or unknown.
Assert(false) is weird. It is basically saying that true==false
and asks you to prove that over a statement/loop that may or may
not terminate.
http://coq.inria.fr/distrib/8.2/contribs/HoareTut.exgcd.html
«Basic Hoare logic is not well-suited for reasoning about
non-terminating programs. In total correctness, postconditions of
non-terminating programs are not provable. In partial
correctness, a non-terminating program satisfies any
(unsatisfiable) postcondition.»
