Arthur,

If I wanted to get theoretical, I would think about a different reaction
to a pre- and post-condition violation:

  * If a service pre-condition is violated, then that service is called
    when the system is in a "consistent", but "inconvenient" state -
    like calling a "storage.read() require: this.isOpen() { ... }" after
    "storage.close() ensure: !this.isOpen() { ... }" has already been
    called. If we throw on a pre-condition viollation, the system state
    remains "consistent" (I'm assuming preconditions don't change the
    system state).
  * If a service post-condition is violated, then that service has a bug
    in it, and the system state is not guaranteed to be "consistent"
    anymore. The only safe choice here is, indeed, to halt.

But then, again, both violations mean a bug in the code so I agree with
you when you say "stop running after a contract violation"
(incidentally, when I designed my own language that supported a P-B-C,
then any contract violation did cause a termination with a printed stack
trace, so I guess I'm on the same wavelength as group #2, even if
subconsciously). My mumbling about a "bad_contract" exception was caused
by the existence of a "bad_cast" exception which, if ever thrown by a
"dynamic_cast<T&>", also indicates a bug in the code - but a bug that is
handled via the "resume" semantics: "...catch (bad_cast &) { ... }".

Many thanks again for your response,

     Andrey Kapustin


On 30/06/2020 18:33, Arthur O'Dwyer via Std-Proposals wrote:
> On Tue, Jun 30, 2020 at 1:15 PM andrei--- via Std-Proposals
> <std-proposals_at_[hidden]
> <mailto:std-proposals_at_[hidden]>> wrote:
>
> Good afternoon,
>
> Thanks for the VERY useful insight into the
> programming-by-contract work.
>
> I don't see why the "group #1" wants to continue after a contract
> violation - it's like trying to call "double sqrt(double x)
> require: x >= 0 { ... }" as "sqrt(-1)" - the obvious choice would
> be to throw something like "bad_contract" on a violation (which
> should then never be "checked"). I'll read up on this subject
> further, so thanks again.
>
> FYI, "throw an exception of type bad_contract, which can be caught
> higher up" is the very definition of "continue running the program
> after a contract violation."
> If you want to /*stop*/ running after a contract violation, then you
> have to actually halt the program; you can't say "let's just jump over
> here and keep going."
>
> –Arthur
>