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,ad06d2d7cb045687 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.226.10 with SMTP id ro10mr12634526pbc.6.1328580315019; Mon, 06 Feb 2012 18:05:15 -0800 (PST) MIME-Version: 1.0 Path: lh20ni268845pbb.0!nntp.google.com!news1.google.com!goblin1!goblin.stu.neva.ru!news.tornevall.net!news.jacob-sparre.dk!pnx.dk!jacob-sparre.dk!ada-dk.org!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Mon, 6 Feb 2012 20:05:04 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <82wr86fzos.fsf@stephe-leake.org> <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com> <82k445fu9n.fsf@stephe-leake.org> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1328580312 7937 69.95.181.76 (7 Feb 2012 02:05:12 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 7 Feb 2012 02:05:12 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-02-06T20:05:04-06:00 List-Id: "Phil Thornley" wrote in message news:MPG.299868e7ebbd43b1989683@news.zen.co.uk... > In article , randy@rrsoftware.com says... ... > The original SPARK Rationale says: I don't much care why SPARK is the way it is -- it's obvious that it makes sense for a certain set of customers, and that's great. I want a tool that would be useful for typical Ada programs, and these are going to have dispatching and access types and exceptions and tasks ... There is no way that SPARK is ever going to be that tool, it would destroy its purpose. But I don't necessarily want complete proofs, and as I noted last week, I don't think that there is much value to complete proofs as a goal, because if you have a language that can describe the specifications well enough that you can prove the result, you no longer need the Ada code that's being proved (just execute the specification). We need "enough" proof, but not too much. I'm much more interested in proving that a subprogram meets its postconditions (including exception postconditions) given its parameter types and preconditions. SPARK insists that you go back to the bad old days of using essentially untyped arrays for data storage rather than typed pointers, using error codes and piles of exceptional logic rather than exceptions, and the like -- all of the reasons that I moved to Ada in the first place. It eliminates virtually everything that makes Ada better than "just another programming language", which is not a step forward for my uses. (Obviously, other people's experiences and needs will vary.) Yes, aliasing analysis is hard. That's the point -- if the typing of the underlying system is correct, it rarely could matter to a proof, and it would be fairly easy to point out the rare exceptions. Yes, you could write a case statement instead of using dispatching. Your program maintenance costs will skyrocket (having to rewrite all of those cases and reprove everything every time a new object type is added). Unless your program never changes after it's constructed, which is not remotely the case for anything I work on. > (Personally I wouldn't want to write a compiler at all .....) Well, there's the problem. :-) Real programmers always want to write a compiler (and already have written several). [Not necessarily for a language the size of Ada, though. That requires a form of insanity. ;-)] Randy.