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,ea5071f634c2ea8b X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.28.135 with SMTP id b7mr7782663pbh.8.1322133336558; Thu, 24 Nov 2011 03:15:36 -0800 (PST) Path: lh20ni12508pbb.0!nntp.google.com!news1.google.com!goblin1!goblin.stu.neva.ru!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail From: Brian Drummond Newsgroups: comp.lang.ada Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug. Date: Thu, 24 Nov 2011 11:15:35 +0000 (UTC) Organization: A noiseless patient Spider Message-ID: References: <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com> <3snehoqgs8ia$.1nobjem6g6hx6$.dlg@40tude.net> <128rdz2581345$.c4td19l7qp9z$.dlg@40tude.net> <16ipwvpdavifr$.17bxf7if7f6kh$.dlg@40tude.net> <4ecb78b1$0$6643$9b4e6d93@newsspool2.arcor-online.net> <1iofgbqznsviu$.phvidtvxlyj4$.dlg@40tude.net> <4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net> <4ecbdfdb$0$6629$9b4e6d93@newsspool2.arcor-online.net> <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> <1ecuhb030iugz.4q1hfjx371xa.dlg@40tude.net> <4ecc393d$0$7625$9b4e6d93@newsspool1.arcor-online.net> <124aq618dmove.884jj64mzm6w$.dlg@40tude.net> <1jxx617mf2cqf$.1j076axdq83mr$.dlg@40tude.net> <1cjufyo57vlpg$.11kf45cs5vnb7.dlg@40tude.net> Mime-Version: 1.0 Injection-Date: Thu, 24 Nov 2011 11:15:35 +0000 (UTC) Injection-Info: mx04.eternal-september.org; posting-host="DkTdSjxOCm6DqG+Uf7eArg"; logging-data="12446"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19OUBJ8x7GmW5Yvo5M2REm4Bfp4eSqFX7o=" User-Agent: Pan/0.134 (Wait for Me; GIT cb32159 master) Cancel-Lock: sha1:UhVP13Y+xJ4aQxnsLjORjTfmPsI= Xref: news1.google.com comp.lang.ada:19112 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Date: 2011-11-24T11:15:35+00:00 List-Id: On Thu, 24 Nov 2011 08:07:45 +0000, Simon Wright wrote: > "Dmitry A. Kazakov" writes: >> >> Should it mean that you don't care about separation of implementation >> and interface? > > What I think I was trying to say was that it doesn't seem to me to make > a lot of difference whether the pre/post-conditions are dynamic. > Providing, of course, I've understood your point. I think it does. > To take Georg's example of the stack, I don't see how you're going to > express the fact that its capacity is bounded other than by comments > about constraint errors or by preconditions. > > I seem to be tempted into speculations about SPARK at this point. Stacks > seem to be a rather dangerous construct from the point of view of > proving correctness, logic not being very good at counting. Indeed. But if you also prohibit recursion, maximum stack use is provable. Spark is interesting in that some implementation facts (but not really details) do leak into the annotations (contracts) in the specification, though not into the Ada code for the specification. It has strategies to hide the details (this procedure modifies the state in that package, via an accessor) which are "refined" internally in the package implementation (the accessor modifies stack contents, stack pointer). But the state of the art seems to be that for contracts to be statically determinable, you must restrict how you program, compared to full Ada. In this world, I come down on the side of: dynamically determinable contracts may not be perfect, but they are a lot better than nothing. I would use them and try to create tests to catch them out. Ada is full of such implicit contracts, though they may have other names; some statically determinable... for i in my_array'range loop -- I is contracted to be in range and some dynamically determinable a * 1000000 -- raises Constraint_Error if violated and I don't see any objections to these (maybe from C programmers!) so I think only good can come of the ability to create additional contracts. Unless perhaps the programmer gains a false sense of security from having written contracts. But how is that any different from using the implicit ones? Perhaps the best that can be hoped for is an assessment of each contract by the compiler (or proof tool), and a "WARNING: may raise exception" for the not-proven, to minimise such complacency. - Brian