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-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,6a0391eb7e0327d5 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-02-10 01:49:48 PST Path: archiver1.google.com!postnews1.google.com!not-for-mail From: rod.chapman@praxis-cs.co.uk (Rod Chapman) Newsgroups: comp.lang.ada Subject: Re: Ada style of passing 'in' parameters considered dangerous? Date: 10 Feb 2003 01:49:48 -0800 Organization: http://groups.google.com/ Message-ID: References: <86isvuzabx.fsf@hoastest1-8c.hoasnet.inet.fi> NNTP-Posting-Host: 213.155.153.242 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1044870588 11062 127.0.0.1 (10 Feb 2003 09:49:48 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 10 Feb 2003 09:49:48 GMT Xref: archiver1.google.com comp.lang.ada:33952 Date: 2003-02-10T09:49:48+00:00 List-Id: Antti Sykari wrote in message news:<86isvuzabx.fsf@hoastest1-8c.hoasnet.inet.fi>... > - If there are such cases, could it have been prevented by having > different policy in the language? Yes - use SPARK! > Do you think it would've been > better to force the programmer to specify the parameter passing > mechanism, for example? How? Forcing programmers to explicitly use access parameters, for instance, sounds like a really bad idea. SPARK is free from parameter passing dependencies. The language doesn't specify a mechanism (this would be a big mistake, since the language wouldn't then be a true subset of Ada...), but rather simply enforces language rules so that it is impossible to write a program where the mechanism chosen by a compiler can ever result in differing dynamic semantics at run-time. These rules are checked by the Examiner. All violations are detected statically (in polynomial time) for incomplete programs (basically meaning the rules are chekcable only using the specification of called units, not their bodies...very important for doing analysis when you haven't actually finished writing the program yet!) - Rod, SPARK Team