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 autolearn=ham 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!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!130.59.10.21.MISMATCH!kanaga.switch.ch!news-zh.switch.ch!switch.ch!cernne03.cern.ch!cern.ch!news From: Maciej Sobczak Newsgroups: comp.lang.ada Subject: Re: Code safety and information hiding Date: Wed, 16 Aug 2006 15:23:47 +0200 Organization: CERN - European Laboratory for Particle Physics Message-ID: References: <1155718392.684202.17080@p79g2000cwp.googlegroups.com> <44e2fc24$1_1@glkas0286.greenlnk.net> NNTP-Posting-Host: abpc10883.cern.ch Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: sunnews.cern.ch 1155734626 22123 (None) 137.138.37.241 X-Complaints-To: news@sunnews.cern.ch User-Agent: Thunderbird 1.5.0.5 (X11/20060801) In-Reply-To: <44e2fc24$1_1@glkas0286.greenlnk.net> Xref: g2news2.google.com comp.lang.ada:6226 Date: 2006-08-16T15:23:47+02:00 List-Id: Stuart wrote: > 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). I understand it. It's clear to me now that the spec should declare any interaction of the given subprogram with its environment and global variables are part of it - but it also became clear that with adding 'global' annotations the network of known and checked dependencies is getting much denser. It's this density of dependencies that has struck me at the beginning. -- Maciej Sobczak : http://www.msobczak.com/ Programming : http://www.msobczak.com/prog/