From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Ada vs Eiffel
Date: Mon, 14 Oct 2019 18:13:09 +0200
Date: 2019-10-14T18:13:09+02:00 [thread overview]
Message-ID: <qo26qk$6mo$1@gioia.aioe.org> (raw)
In-Reply-To: 871rvfl5vr.fsf@gmail.com
On 2019-10-14 17:10, Saša Janiška wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>
>> IMO, Eiffel treats contracts wrong.
>
> Can you say something more in regard? I'm really curious to learn...
A contract cannot be asserted or checked at run-time. That is not a
contract, that is a behavior. Introducing a check does not add safety
unless its failure is handled. If not, it is just a bug with or without
the check.
Most of Ada debugging is related to unhandled exceptions from run-time
checks. A proper contract is one proved statically. This is what SPARK
is for.
This does not mean you need no checks, it means that they must be
treated properly, considering a possibility of failure and the program
state should such failure happens.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
next prev parent reply other threads:[~2019-10-14 16:13 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-10-14 14:05 Ada vs Eiffel Saša Janiška
2019-10-14 15:01 ` Dmitry A. Kazakov
2019-10-14 15:10 ` Saša Janiška
2019-10-14 16:13 ` Dmitry A. Kazakov [this message]
2019-10-14 17:24 ` Jeffrey R. Carter
2019-10-14 19:37 ` Saša Janiška
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox