From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,a5cbf1d38f567a0e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!n35g2000yqm.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: Refinement & Abstraction question Date: Sun, 15 Nov 2009 01:35:03 -0800 (PST) Organization: http://groups.google.com Message-ID: <74c00506-1ff9-4c22-92bd-bb81d770a0cc@n35g2000yqm.googlegroups.com> References: NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: posting.google.com 1258277703 30778 127.0.0.1 (15 Nov 2009 09:35:03 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 15 Nov 2009 09:35:03 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: n35g2000yqm.googlegroups.com; posting-host=80.177.171.182; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 7.0; Windows NT 5.1; Trident/4.0; .NET CLR 1.1.4322; .NET CLR 2.0.50727; .NET CLR 3.0.4506.2152; .NET CLR 3.5.30729),gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:8104 Date: 2009-11-15T01:35:03-08:00 List-Id: On 14 Nov, 21:18, "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