From: AdaMagica <christ-usch.grein@t-online.de>
Subject: Re: Ada syntax questions
Date: Sat, 19 Dec 2020 09:01:53 -0800 (PST) [thread overview]
Message-ID: <c1eefcb2-8b54-4e07-9184-65b357fe1f06n@googlegroups.com> (raw)
In-Reply-To: <5fdde913$0$3238$426a74cc@news.free.fr>
DrPi schrieb am Samstag, 19. Dezember 2020 um 12:50:45 UTC+1:
> Calling a function can have side effects. Accessing an array or a
> variable can't have side effects.
The declaration of the function is a contract about pre and post conditions,
albeit in Ada incomplete. In SPARK, the contract is firm.
As a user of the function, you have to believe the programmer that he follows the contract.
If the implementation needs a side effect, so be it.
If on the other hand you are a maintainer or are chasing a bug,
you have to check the requirements first,
not the body of the function. This comes later.
> > You seem to be implying this is bad; why?
> Reading the code can't tell you the writer's intentions.
The intentions are in the requirements (or in the accompanying comments, you hope
they up to date and not wrong).
If there are none, good luck.
next prev parent reply other threads:[~2020-12-19 17:01 UTC|newest]
Thread overview: 35+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-12-17 22:39 Ada syntax questions DrPi
2020-12-17 23:18 ` Gabriele Galeotti
2020-12-18 8:26 ` Jeffrey R. Carter
2020-12-18 9:18 ` Dmitry A. Kazakov
2020-12-18 16:55 ` Mart van de Wege
2020-12-18 17:38 ` Björn Lundin
2020-12-18 19:35 ` Niklas Holsti
2020-12-20 21:59 ` Keith Thompson
2020-12-22 1:04 ` Randy Brukardt
2020-12-22 8:00 ` Dmitry A. Kazakov
2020-12-23 1:23 ` Randy Brukardt
2020-12-23 8:59 ` Dmitry A. Kazakov
2020-12-24 4:06 ` Randy Brukardt
2020-12-24 9:37 ` Dmitry A. Kazakov
2020-12-22 13:48 ` AdaMagica
2020-12-20 21:59 ` Keith Thompson
2020-12-21 8:08 ` Dmitry A. Kazakov
2020-12-18 23:09 ` Stephen Leake
2020-12-19 11:50 ` DrPi
2020-12-19 12:40 ` Dmitry A. Kazakov
2020-12-19 17:13 ` Andreas ZEURCHER
2020-12-19 17:49 ` Dmitry A. Kazakov
2020-12-19 18:40 ` Andreas ZEURCHER
2020-12-19 19:37 ` Dmitry A. Kazakov
2020-12-19 22:11 ` Andreas ZEURCHER
2020-12-20 8:47 ` Dmitry A. Kazakov
2020-12-20 16:53 ` Andreas ZEURCHER
2020-12-22 0:58 ` Randy Brukardt
2020-12-22 2:39 ` Andreas ZEURCHER
2020-12-22 10:05 ` Stéphane Rivière
2020-12-25 9:34 ` G.B.
2020-12-19 17:01 ` AdaMagica [this message]
2020-12-19 21:51 ` Stephen Leake
2020-12-19 22:20 ` Andreas ZEURCHER
2020-12-20 14:10 ` DrPi
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox