Re: Refinement & Abstraction question

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 14 Nov, 21:18, "mbrk...@googlemail.com" <mbrk...@googlemail.com>
wrote:

> General question , what is the deference between keeping inherit
> statement in ADS file rather than moving it to the ADB file.
>
> Is there a rule ? or it is against the hiding principle?

Yes there is a rule and it is about hiding.

The rule is that the inherit annotation goes with a package
specification (the .ads file) and it is illegal to put it on a package
body (the .adb file).

The single exception to this rule is that the main program goes in
an .adb file and it will have inherit annotations - but the main
program is the only procedure that can be declared outside a package.

The rule is there to avoid information being hidden - even though it
appears to break the principle of information hiding.  If an
inheriting package (A) only references the inherited package (B) in
its annotations (because A's body does not call any operations in B)
then the requirement for the inherit forces a dependency in the
annotations that isn't there in the code.

But SPARK enforces the reference to package B in the annotations of A
because the abstract 'own' data of B will be included in the
information flow implemented by operations in A, and this dependency
must not be hidden.  The dependency in this case is only to the data
abstractions of B and not to any part of its implementation - so
changes to the implementation of B that don't affect its data
abstractions won't have any effect on A.

The only situation I can think of where the inherit might be avoided
is if package B has no abstract own data (an abstract data type) and A
only uses that data type for local data within its operations.  This
is probably quite unusual, and the requirement for the inherit won't
be transitive (ie packages inheriting A won't also be required to
inherit B).

Hope this helps.

Cheers,

Phil