From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Introductory Presentations, especially aimed at C++ programmers!
Date: Thu, 8 Dec 2016 09:38:06 +0100
Date: 2016-12-08T09:38:06+01:00 [thread overview]
Message-ID: <o2b65e$1bu5$1@gioia.aioe.org> (raw)
In-Reply-To: f3abc4c7-9009-40eb-ac09-ad984c8d3fec@googlegroups.com
On 08/12/2016 09:08, Maciej Sobczak wrote:
> The problem is - you did not provide any evidence to claim that
> those same humans would not make such errors in Ada.
>
> SPARK is a game-changer in this area - but there are too few
> long-lived internet-oriented open-source projects in SPARK to make a
> realistic comparison either. That is, if for whatever reason it is
> unrealistic to write such projects in SPARK, then SPARK is not a
> solution, either.
That's right. Exception contracts are long overdue and the design of
proofs must allow mixed strategies instead of all-or-nothing. In most
cases it would be enough to statically prove absence of exceptions.
However, in the given case the proof must be about "no exception when
registry key value is less than N" That goes more towards a full
correctness proof.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
next prev parent reply other threads:[~2016-12-08 8:38 UTC|newest]
Thread overview: 52+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-07-10 12:24 Introductory Presentations, especially aimed at C++ programmers! John McCabe
2009-07-10 21:49 ` jimmaureenrogers
2009-07-10 23:37 ` wwilson
2009-07-11 0:07 ` jimmaureenrogers
2009-07-12 4:00 ` wwilson
2009-07-11 8:15 ` Stephen Leake
2009-07-15 6:43 ` Jean-Pierre Rosen
2016-12-07 17:06 ` john
2016-12-07 17:44 ` Luke A. Guest
2016-12-07 18:35 ` Jeffrey R. Carter
2016-12-07 23:03 ` Randy Brukardt
2016-12-07 23:47 ` Jeffrey R. Carter
2016-12-08 0:08 ` Paul Rubin
2016-12-09 22:01 ` Randy Brukardt
2016-12-09 22:18 ` Jeffrey R. Carter
2016-12-13 0:53 ` Randy Brukardt
2016-12-13 3:21 ` Jeffrey R. Carter
2016-12-13 21:15 ` Robert A Duff
2016-12-13 22:05 ` Jeffrey R. Carter
2016-12-13 22:52 ` Robert A Duff
2016-12-14 0:02 ` Jeffrey R. Carter
2016-12-13 23:05 ` Randy Brukardt
2016-12-14 0:13 ` Jeffrey R. Carter
2016-12-14 22:48 ` Randy Brukardt
2016-12-15 0:00 ` Jeffrey R. Carter
2016-12-15 10:46 ` Maciej Sobczak
2016-12-16 7:37 ` Paul Rubin
2016-12-15 20:14 ` Niklas Holsti
2016-12-15 20:27 ` Jeffrey R. Carter
2016-12-15 21:04 ` Niklas Holsti
2016-12-15 21:40 ` Jeffrey R. Carter
2016-12-16 7:41 ` Paul Rubin
2016-12-13 22:50 ` Randy Brukardt
2016-12-14 0:08 ` Jeffrey R. Carter
2016-12-14 1:01 ` Shark8
2016-12-08 8:08 ` Maciej Sobczak
2016-12-08 8:38 ` Dmitry A. Kazakov [this message]
2016-12-08 10:25 ` Paul Rubin
2016-12-08 13:39 ` Maciej Sobczak
2016-12-09 1:30 ` Paul Rubin
2016-12-09 8:31 ` J-P. Rosen
2016-12-09 8:58 ` Paul Rubin
2016-12-09 9:18 ` J-P. Rosen
2016-12-09 9:27 ` Paul Rubin
2016-12-09 10:49 ` J-P. Rosen
2016-12-09 19:58 ` Jeffrey R. Carter
2016-12-09 8:35 ` G.B.
2016-12-09 8:57 ` Paul Rubin
2016-12-09 22:15 ` Randy Brukardt
2016-12-09 21:58 ` Randy Brukardt
2016-12-08 8:23 ` Maciej Sobczak
2016-12-08 18:54 ` Adam Jensen
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox