From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: spec/body/rep (Was: Compilation error (GNAT bug?))
Date: Tue, 27 May 2014 18:41:46 +0200
Date: 2014-05-27T18:41:46+02:00 [thread overview]
Message-ID: <1loe63h8q0q1g.r9u22ub67h47.dlg@40tude.net> (raw)
In-Reply-To: 5384b302$0$6663$9b4e6d93@newsspool3.arcor-online.net
On Tue, 27 May 2014 17:45:07 +0200, G.B. wrote:
> On 27.05.14 10:55, Dmitry A. Kazakov wrote:
>> I have issues with this approach in general. The problem is that there is
>> no any check that the interfaces of the target-specific packages are same
>> in the sense that all target-independent clients were compilable with any
>> "implementation."
>
> Assuming that a universal expression of "compilability" in any
> configuration is nice, but likely impossible,
It is surely possible at the same level of scrutiny the language mandates
certain programs legal <=> compilable.
> would you still think
> that what Randy has called a semantics-denying fiction could
> be preserved for some aspects? For example,
>
> procedure Doubled (X : in out Natural)
> with Post => (if
> X'Old <= Natural'Last / 2
> then
> X = X'Old * 2
> else
> False),
> Import,
> External_Name => "d2";
>
> If the External_Name aspect of Doubled were moved to
> a representation unit tied to whatever Doubled lives in,
That is what I suggested. I don't care about aspects, there is no such
thing in real-life at all. There are specifications and implementations,
nothing else.
External_Name certainly belongs to the implementation as any definition of
a body does. No difference.
So if you moved it to the implementation and then switched implementations
with the targets, that will be all OK to me. Some implementations could
have a proper body of Doubled.
> then developing the program that calls Doubled should work
> up to a point, namely when Natural's representation finally
> matters.
It never matters if post-condition you wrote was meant proper
post-condition = checked at compile time.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
next prev parent reply other threads:[~2014-05-27 16:41 UTC|newest]
Thread overview: 13+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-05-20 18:32 Compilation error (GNAT bug?) Victor Porton
2014-05-20 18:43 ` Simon Wright
2014-05-20 22:22 ` spec/body/rep (Was: Compilation error (GNAT bug?)) Georg Bauhaus
2014-05-23 21:21 ` Randy Brukardt
2014-05-27 5:16 ` J-P. Rosen
2014-05-27 6:22 ` Niklas Holsti
2014-05-27 8:54 ` J-P. Rosen
2014-05-27 8:55 ` Dmitry A. Kazakov
2014-05-27 15:45 ` G.B.
2014-05-27 16:41 ` Dmitry A. Kazakov [this message]
2014-05-27 16:52 ` G.B.
2014-05-27 17:03 ` Dmitry A. Kazakov
2014-05-27 22:57 ` Randy Brukardt
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox