[rramadass]

DbC is the Policy (i.e. what/why) and Asserts are the Mechanism (i.e. how) (https://en.wikipedia.org/wiki/Separation_of_mechanism_and_po...) DbC can be implemented in any language that provides an assert-like mechanism (whether named "assert" or not). An Assert merely validates the state of a program at a particular point during execution. You use it to steer the program to go through only the correct subset of the state space of the program. You could do this pre/post every executable statement (i.e. write proof of correctness) or use a higher-level structured methodology like DbC which is far more practical. The given resources address both.

The point is that when using asserts you think about correctness w.r.t. specifications and nothing else. To think of it as simply validating arguments or in terms of effects on optimization is quite the wrong thing to do.

PS: I don't bother about upvotes/downvotes but am often reminded of the following Sherlock Holmes quote when i see HN's reaction to deeper subjects ;-)

Pshaw, my dear fellow, what do the public, the great unobservant public, who could hardly tell a weaver by his tooth or a compositor by his left thumb, care about the finer shades of analysis and deduction!"

[MaxBarraclough]

> DbC is the Policy (i.e. what/why) and Asserts are the Mechanism

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.

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.

> An Assert merely validates the state of a program at a particular point during execution.

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.

> You use it to steer the program to go through only the correct subset of the state space of the program

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.

> You could do this pre/post every executable statement (i.e. write proof of correctness)

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.

> The point is that when using asserts you think about correctness w.r.t. specifications and nothing else. To think of it as simply validating arguments or in terms of effects on optimization is quite the wrong thing to do.

I'm not sure why you'd think I don't already know that.

[0] https://news.ycombinator.com/item?id=44675668

[rramadass]

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.