From: "Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org>
Subject: Re: Why .ads as well as .adb?
Date: Mon, 3 Jun 2019 19:00:20 +0200
Date: 2019-06-03T19:00:20+02:00 [thread overview]
Message-ID: <qd3jn6$kn8$1@dont-email.me> (raw)
In-Reply-To: <28facad3-c55f-4ef2-8ef8-004925b7d1f1@googlegroups.com>
On 6/2/19 2:48 AM, John Perry wrote:
>
> As far as I can tell, though, Ada has stuck with the two separate files, rather than, say, generating an .ads from an .adb with export markup.
>
> Is there a reason Ada hasn't moved to this simpler structure?
First, let me point out that your specification is GNAT-specific, but your body
is compiler-independent. I'm going to presume that the generation of the spec
from the body was faulty.
Others have given you the good reasons related to S/W engineering in the large
(more than 1 person). They provide a formal and compiler-checked way to state
what each person is working on, and allow the development of parts of the S/W
that depend on other parts that have not been implemented yet.
I have not seen any responses that address the use of specs to represent and
check high-level design decisions. This can be very helpful.
Nor have I seen any responses that deal with specs as a way to deal with the
limitations of the human brain. When a system reaches a certain size, whether
developed by a single person or a team, it becomes impossible to keep the entire
system in one's head. Specs reduce the amount of information that must be retained.
I recall reading a quote by a famous S/W engineer: "I have only a small brain
and must learn to live with it." I don't recall who, and I can't find it on
line. Reducing the amount of information kept in the brain is what he meant by
learning to live with it. Separate specs are a mechanism for that.
In another post, you wrote
> So I was surprised that some people made absolute negations of the possibility along these lines:
>
> "You can't generate specification from implementation."
>
> I especially wonder this since one of them had just referred to gnatchop, whose online documentation provides an example that does precisely that [1].
Note that gnatchop does not generate specifications from bodies, and the example
does not show that. It shows an input file containing 2 compilation units, a
spec and a body. gnatchop produces a single file for each compilation unit in
its input.
--
Jeff Carter
"I fart in your general direction."
Monty Python & the Holy Grail
05
next prev parent reply other threads:[~2019-06-03 17:00 UTC|newest]
Thread overview: 88+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-06-02 0:48 Why .ads as well as .adb? John Perry
2019-06-02 5:42 ` J-P. Rosen
2019-06-02 6:39 ` Dmitry A. Kazakov
2019-06-03 7:35 ` Maciej Sobczak
2019-06-03 7:57 ` J-P. Rosen
2019-06-03 19:49 ` Keith Thompson
2019-06-04 8:03 ` Maciej Sobczak
2019-06-03 8:13 ` Dmitry A. Kazakov
2019-06-03 19:51 ` Keith Thompson
2019-06-03 20:18 ` Dmitry A. Kazakov
2019-06-04 8:24 ` Maciej Sobczak
2019-06-04 9:33 ` Dmitry A. Kazakov
2019-06-05 9:04 ` Maciej Sobczak
2019-06-05 12:48 ` Dmitry A. Kazakov
2019-06-05 17:12 ` G. B.
2019-06-05 18:50 ` Optikos
2019-06-05 22:57 ` Randy Brukardt
2019-06-04 22:28 ` Randy Brukardt
2019-06-05 8:28 ` Maciej Sobczak
2019-06-05 9:20 ` J-P. Rosen
2019-06-05 9:28 ` Paul Rubin
2019-06-05 10:11 ` Niklas Holsti
2019-06-05 12:58 ` Maciej Sobczak
2019-06-05 14:28 ` Niklas Holsti
2019-06-06 7:34 ` Maciej Sobczak
2019-06-06 19:51 ` Keith Thompson
2019-06-06 20:27 ` J-P. Rosen
2019-06-06 21:12 ` Randy Brukardt
2019-06-06 21:17 ` Randy Brukardt
2019-06-06 22:08 ` Dennis Lee Bieber
2019-06-07 7:59 ` Maciej Sobczak
2019-06-07 10:42 ` alby.gamper
2019-06-07 16:59 ` Dennis Lee Bieber
2019-06-07 14:10 ` Brad Moore
2019-06-07 23:37 ` Paul Rubin
2019-06-08 1:16 ` Brad Moore
2019-06-08 7:34 ` Simon Wright
2019-06-08 17:44 ` G.B.
2019-06-08 21:41 ` Keith Thompson
2019-06-09 0:40 ` Paul Rubin
2019-06-09 18:56 ` Keith Thompson
2019-06-09 20:35 ` John Perry
2019-06-09 21:15 ` Niklas Holsti
2019-06-09 22:37 ` John Perry
2019-06-10 9:01 ` Simon Wright
2019-06-10 13:15 ` Simon Wright
2019-06-10 9:22 ` Niklas Holsti
2019-06-09 21:37 ` Simon Wright
2019-06-09 22:40 ` John Perry
2019-06-10 9:07 ` Simon Wright
2019-06-09 21:46 ` Niklas Holsti
2019-06-10 17:11 ` Dennis Lee Bieber
2019-06-08 4:57 ` Randy Brukardt
2019-06-08 23:57 ` Optikos
2019-06-09 0:43 ` Paul Rubin
2019-06-10 8:17 ` Maciej Sobczak
2019-06-10 19:10 ` G.B.
2019-06-10 22:07 ` Randy Brukardt
2019-06-11 0:32 ` Optikos
2019-06-11 15:39 ` Brad Moore
2019-06-11 16:14 ` John Perry
2019-06-11 16:46 ` Shark8
2019-06-11 19:29 ` John Perry
2019-06-14 6:12 ` Brad Moore
2019-06-14 21:51 ` John Perry
2019-06-14 16:29 ` djakoogler
2019-06-11 18:19 ` joakimds
2019-06-11 15:49 ` Jeffrey R. Carter
2019-06-07 7:36 ` Niklas Holsti
2019-06-05 22:41 ` Randy Brukardt
2019-06-06 3:34 ` Keith Thompson
2019-06-06 7:29 ` Maciej Sobczak
2019-06-06 15:30 ` John Perry
2019-06-06 15:41 ` Brad Moore
2019-06-06 19:42 ` Keith Thompson
2019-06-06 16:37 ` Dennis Lee Bieber
2019-06-02 9:59 ` joakimds
2019-06-02 20:14 ` G.B.
2019-06-03 13:37 ` John Perry
2019-06-03 14:50 ` Niklas Holsti
2019-06-03 19:23 ` John Perry
2019-06-03 21:04 ` Niklas Holsti
2019-06-03 18:51 ` Lucretia
2019-06-03 19:32 ` John Perry
2019-06-03 17:00 ` Jeffrey R. Carter [this message]
2019-06-03 18:59 ` Lucretia
2019-06-03 19:29 ` John Perry
2019-06-03 20:00 ` Jeffrey R. Carter
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox