| Yeah, i remember our previous "discussion" on this topic. You were the guy arguing that Formal Method/Verification means only the use of static analysis and verification using SMT/SAT solvers while i was arguing that Formal Methods were far more broader involving multiple levels, a bunch of runtime aspects etc. This is often the easier place to start for programmers since they don't need to learn complex concepts/terminologies initially but can gradually buildup to it. I also note that i gave you a bunch of references in support of my arguments. > The ideal way to do runtime-checked DbC is not with simple asserts, it's with proper first-class preconditions and postconditions at the language level. Not quite. DbC should be taught using only simple runtime asserts so that programmers can grasp the essence instead of confusing it with syntactic sugar which is irrelevant to the overall concepts/ideas. Once they grok this they can exercise DbC in any language eg. minimal C language. Furthermore they can now be led to the idea of doing it statically by mapping asserts to verification conditions and thence solved. This can lead to Frama-C and finally to a full-blown verification aware language like Dafny with all the bells-and-whistles. > It wouldn't be nice to have to manually ensure that both old and new states of variables are in-scope for postcondition checking. I can imagine that being not just tedious, but error-prone. Dijkstra has already given mechanical transformation rules for this in his wp-calculus. Tedious/error-prone is subjective since for something like a embedded health-monitor it is necessary. > Some aspect of the program's state, yes, and hopefully that's all it does. > Interesting to think about the edge-cases here though. Depending on the language, it could accidentally side-effect, or even invoke undefined behaviour, and so actively derail the program. Can't blame DbC for that though, that's a question of language safety. This is solely the programmer's responsibility and his knowledge of his implementation language. We have already discussed this in our previous discussion. > I'm not sure I follow here. You don't use asserts to steer flow-control, you use them to check aspects of program state. An assert is a predicate and therefore an implicit conditional. When true, only a subset of the input state space is allowed in. When false, the program is halted. This is what i mean by "steering" i.e. the running program is a trajectory through a state space which we enforce by the usage of our asserts. > That doesn't constitute a proof of correctness, no more than last time you and I discussed this. [0] Depending on the language, it wouldn't even necessarily prove the correctness of that particular trace, as you haven't proven that you haven't accidentally invoked undefined behaviour. > You hold a minority opinion on this, please stop presenting it as settled fact. We had already discussed this and i had already pointed out that is how "correct-by-construction" approach works whether done informally or formally by a programmer. It is your opinion which is narrow and in certain aspects wrong. Your examples of UB is simply a red herring since i have already pointed out that the programmer needs to be aware of this (and his language's optimizer). Dijkstra for example invented his GCL and taught his class to use wp-calculus to derive preconditions from postconditions for every executable statement by hand to demonstrate proof of correctness. > I'm not sure why you'd think I don't already know that. That was aimed more at the OP article than you. However, when i see your comments w.r.t. UB, i wonder. One needs to know one's language's types and their bounds, sequence points and how it relates to expressions/statements to avoid UB. |