From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Interesting article on ARG work
Date: Thu, 5 Apr 2018 16:23:53 -0500
Date: 2018-04-05T16:23:53-05:00 [thread overview]
Message-ID: <pa645a$1lg$1@franka.jacob-sparre.dk> (raw)
In-Reply-To: 1e3a9818-7c9a-4a8e-a6fb-ebaabd2570f7@googlegroups.com
"Mehdi Saada" <00120260a@gmail.com> wrote in message
news:1e3a9818-7c9a-4a8e-a6fb-ebaabd2570f7@googlegroups.com...
...
>.. One thing I found (a bit) irritating from a beginner point of view,
> is that normal visibility rules still still holds in contracts/assertions.
> It
> would be much easier to write contracts about conditions of (at
> least) things declared in the private part. It would be nonsensical to
> let them reach the body though, that I can understand. But why not
> packages' private part ?
A subprogram contract is just that - a contract between the caller and
called subprogram. That means the caller needs to be able to understand the
contents of the contract, and given that they are not supposed to depend on
the private part, the contract can't either.
Imagine that items in the private part were allowed. Perhaps we'd have a
contract like:
package Something is
type Bar is ...;
procedure Proc (Foo : in out Bar)
with Pre => Is_Groddy (Foo);
private
function Is_Groddy (Foo : in Bar) return Boolean;
end Something;
Now, the caller is not supposed to call Something.Proc when Is_Groddy is
false (that's the contract). Perhaps the caller wants to make the test
themselves (think of how often you test for null with access types before
making a call):
if Is_Groddy (My_Bar) then
Proc (My_Bar);
else
-- Some alternative code.
end if;
But the above is illegal, because Is_Groddy is in the private part and not
available to the callers of Proc. This leaves the programmer with only bad
options: make the call unconditionally and hope that My_Bar is in fact
Groddy -- or handle the Assertion_Errror (generally more expensive than a
test). (And if you are doing static checking, you end up depending
explicitly on the private part, meaning you are no longer hiding it in any
way.)
Regardless of what private information was in the contract, it is not useful
to the caller (unless they also break privacy and inspect the private part).
That pretty much defeats the purpose of making it private in the first
place.
Randy.
next prev parent reply other threads:[~2018-04-05 21:23 UTC|newest]
Thread overview: 57+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-04-02 3:32 Interesting article on ARG work Randy Brukardt
2018-04-02 14:49 ` Dan'l Miller
2018-04-03 16:34 ` Bojan Bozovic
2018-04-03 22:33 ` Randy Brukardt
2018-04-04 2:12 ` Bojan Bozovic
2018-04-04 15:05 ` Dan'l Miller
2018-04-04 15:30 ` gerdien.de.kruyf
2018-04-04 16:09 ` Dan'l Miller
2018-04-04 22:30 ` Randy Brukardt
2018-04-04 22:43 ` Paul Rubin
2018-04-05 0:44 ` Mehdi Saada
2018-04-05 21:23 ` Randy Brukardt [this message]
2018-04-05 2:05 ` Bojan Bozovic
2018-04-05 22:12 ` Randy Brukardt
2018-04-06 13:35 ` Bojan Bozovic
2018-04-07 2:01 ` Randy Brukardt
2018-04-05 7:21 ` Dmitry A. Kazakov
2018-04-05 22:18 ` Randy Brukardt
2018-04-06 7:30 ` Dmitry A. Kazakov
2018-04-07 2:25 ` Randy Brukardt
2018-04-07 10:11 ` Dmitry A. Kazakov
2018-04-07 15:27 ` Dan'l Miller
2018-04-07 15:59 ` Dmitry A. Kazakov
2018-04-08 0:14 ` Dan'l Miller
2018-04-08 7:46 ` Dmitry A. Kazakov
2018-04-08 19:48 ` Dan'l Miller
2018-04-08 20:09 ` Dmitry A. Kazakov
2018-04-09 3:50 ` Dan'l Miller
2018-04-09 6:40 ` Jan de Kruyf
2018-04-09 7:43 ` Dmitry A. Kazakov
2018-04-09 13:40 ` Dan'l Miller
2018-04-09 14:13 ` Dmitry A. Kazakov
2018-04-09 14:36 ` Dan'l Miller
2018-04-09 14:44 ` Dmitry A. Kazakov
2018-04-09 15:03 ` Dan'l Miller
2018-04-09 16:12 ` Niklas Holsti
2018-04-09 16:30 ` Dmitry A. Kazakov
2018-04-09 16:45 ` Niklas Holsti
2018-04-09 17:33 ` Dan'l Miller
2018-04-09 19:47 ` Dmitry A. Kazakov
2018-04-09 20:24 ` Randy Brukardt
2018-04-10 8:17 ` Dmitry A. Kazakov
2018-04-09 18:08 ` Dan'l Miller
2018-04-09 21:17 ` Niklas Holsti
2018-04-09 22:09 ` Dan'l Miller
2018-04-10 19:23 ` Niklas Holsti
2018-04-10 19:46 ` Dan'l Miller
2018-04-15 7:50 ` Niklas Holsti
2018-04-15 13:31 ` Dan'l Miller
2018-04-15 18:37 ` Niklas Holsti
2018-04-09 20:14 ` Randy Brukardt
2018-04-06 23:49 ` Dan'l Miller
2018-04-12 10:21 ` Marius Amado-Alves
2018-04-15 13:07 ` Ada conditional compilation and program variants Niklas Holsti
2018-05-07 8:41 ` Jacob Sparre Andersen
2018-04-06 13:35 ` Interesting article on ARG work Marius Amado-Alves
2018-04-07 2:15 ` 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