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=-0.9 required=5.0 tests=BAYES_00,FROM_NUMERIC_TLD autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,34257fd17abeba14 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!border1.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newspeer1.nwr.nac.net!bbc!news-peer-lilac.gradwell.net!not-for-mail From: "Stuart" Newsgroups: comp.lang.ada References: <1155718392.684202.17080@p79g2000cwp.googlegroups.com> Subject: Re: Code safety and information hiding Date: Wed, 16 Aug 2006 12:18:07 +0100 X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.2180 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.2180 Message-ID: <44e2fc24$1_1@glkas0286.greenlnk.net> X-Original-NNTP-Posting-Host: glkas0286.greenlnk.net NNTP-Posting-Host: 20.133.0.1 X-Trace: 1155727100 news.gradwell.net 633 dnews/20.133.0.1:27900 X-Complaints-To: news-abuse@gradwell.net Xref: g2news2.google.com comp.lang.ada:6225 Date: 2006-08-16T12:18:07+01:00 List-Id: To follow up on what Rod has said in reply to: "Maciej Sobczak" wrote in message news:ebuj47$bal$1@sunnews.cern.ch... wrote in message news:1155718392.684202.17080@p79g2000cwp.googlegroups.com... >> The issue with this example is the apparent strong coupling between the >> specification of Rand (of the whole package, in fact) and the >> implementation details that pop up in specs in terms of the Seed name >> used in annotations. > > SPARK promotes the hiding of _detail_, but not the hiding of > _information_. > > The package spec you cite _does_ need to announce the existance of > "Seed" (but not its type, structure, or anything else). You are also > correct to identify that choosing the name "Seed" is crucial, since > changing it later can have a non-trivial impact on clients of this > package. An important point identified by the SPARK annotation is that you have chosen to implement it as an Abstract State Machine (single instance shared by all clients), rather than an Abstract Data Type that can have multiple independent instances (with the Seed as a parameter). As to the choice of name - I thought that SPARK's data refinement rules allowed you to change the view (effectively including the names used) between package specification and package body. >> I don't find the above to be particularly disturbing, but I'm tempted to >> conclude that in SPARK increased code safety has the price of reduced >> information hiding, which itself was always considered to be a good >> engineering practice. Rod's distinction between detail and information is a good one. It should also be remembered that the objective of SPARK is to allow you to reason about what your program will do. Often, in less rigorous design processes, you might assume that a subprogram you use has no unexpected consequences (e.g. side-effects). SPARK is much more rigorous - it makes sure that subprograms have no side-effects: the consequence is that _all_ effects of a subprogram must be recorded (e.g. updating the Seed in the Random number example). Regards -- Stuart Palin