* exiting a bloc @ 2000-09-02 20:10 Mathias Dolidon 2000-09-02 20:39 ` Mathias Dolidon 2000-09-02 21:01 ` Robert Dewar 0 siblings, 2 replies; 24+ messages in thread From: Mathias Dolidon @ 2000-09-02 20:10 UTC (permalink / raw) Hello. I am very new to Ada and trying to write some small programs. In a program which searches primary numbers, I would like to exit a bloc which is embedded in a loop, without exiting the loop : for...loop intruction; bloc : begin -- the matter is here end bloc; end loop; I looked everywhere about how to do this but I found nothing. Is this possible ? Thank you very much ! Mathias -- http://www.mdlabs.ovh.org ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-02 20:10 exiting a bloc Mathias Dolidon @ 2000-09-02 20:39 ` Mathias Dolidon 2000-09-02 21:01 ` Robert Dewar 1 sibling, 0 replies; 24+ messages in thread From: Mathias Dolidon @ 2000-09-02 20:39 UTC (permalink / raw) > Hello. I am very new to Ada and trying to write some small programs. In > a program which searches primary numbers, I would like to exit a bloc > which is embedded in a loop, without exiting the loop : > > for...loop > intruction; > > bloc : > begin > -- the matter is here > end bloc; > end loop; > > I looked everywhere about how to do this but I found nothing. Is this > possible ? Thank you very much ! > Mathias I did it like this : instead of declaring a bloc, I declare a loop withan exit instruction before "end loop", but it doesn't seem very clean to me ! Isn't there a more "official" way ? -- http://www.mdlabs.fr.st ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-02 20:10 exiting a bloc Mathias Dolidon 2000-09-02 20:39 ` Mathias Dolidon @ 2000-09-02 21:01 ` Robert Dewar 2000-09-02 22:34 ` Mathias Dolidon 2000-09-05 17:52 ` Richard Riehle 1 sibling, 2 replies; 24+ messages in thread From: Robert Dewar @ 2000-09-02 21:01 UTC (permalink / raw) In article <39B15EA8.88DB58AB@netcourrier.com>, Mathias Dolidon <matd@netcourrier.com> wrote: > for...loop > intruction; > > bloc : > begin > -- the matter is here > end bloc; > end loop; THe obvious answer is that a goto could be used, however, it is almost certain that if we saw the entire code we would suggest some other method. In particular, it is not at all clear why you are using a block at all, it appears useless but of course we do not have your entire code. Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-02 21:01 ` Robert Dewar @ 2000-09-02 22:34 ` Mathias Dolidon [not found] ` <86snrhkfep.fsf@acm.org> 2000-09-05 17:52 ` Richard Riehle 1 sibling, 1 reply; 24+ messages in thread From: Mathias Dolidon @ 2000-09-02 22:34 UTC (permalink / raw) > The obvious answer is that a goto could be used, however, it is > almost certain that if we saw the entire code we would suggest > some other method. In particular, it is not at all clear why > you are using a block at all, it appears useless but of course > we do not have your entire code. Here is the entire code : ------------------------------------------- with ada.text_io, ada.integer_text_io; use ada.text_io, ada.integer_text_io; with ada.numerics.elementary_functions; use ada.numerics.elementary_functions; procedure nbr_prem is nombre_en_cours, diviseur, racine : positive; begin put_line("-- Recherche des nombres premiers de 1 �" & positive'image(positive'last) & " --"); new_line; put_line(positive'image(1)); put_line(positive'image(2)); put_line(positive'image(3)); for nombre_en_cours in 3..positive'last loop racine := positive(sqrt(float(nombre_en_cours))) + 2; test: loop for diviseur in 2..racine loop exit test when nombre_en_cours rem diviseur = 0; end loop; put_line(positive'image(nombre_en_cours)); exit; end loop test; end loop; end nbr_prem; ---------------------------------------- You see here that I have used a loop with an unconditionnal exit to simulate a block, but I think it would be cleaner with a real block. Don't tell me about the algorithm ! This is just to try out the Ada language. Thank you Mathias ^ permalink raw reply [flat|nested] 24+ messages in thread
[parent not found: <86snrhkfep.fsf@acm.org>]
* Re: exiting a bloc [not found] ` <86snrhkfep.fsf@acm.org> @ 2000-09-03 15:46 ` Mathias Dolidon 0 siblings, 0 replies; 24+ messages in thread From: Mathias Dolidon @ 2000-09-03 15:46 UTC (permalink / raw) Laurent Guerby a �crit : > > > I think an explicit boolean and an if statement after the "test" loop > look better than two loops here. See the code at the end of this post. > > Also, in Ada a for statement declare its indice, so you don't need to > declare them before (or if you do, the declare are hidden inside the > loop statement). GNAT 3.13 does warn about it in your original program: > > nbr_prem.adb:9:07: warning: "nombre_en_cours" is never assigned a value > nbr_prem.adb:9:24: warning: "diviseur" is never assigned a value > > Hope this helps, > > -- > Laurent Guerby <guerby@acm.org> Merci beaucoup ! ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-02 21:01 ` Robert Dewar 2000-09-02 22:34 ` Mathias Dolidon @ 2000-09-05 17:52 ` Richard Riehle 2000-09-06 2:06 ` Ted Dennison 2000-09-06 7:00 ` Ray Blaak 1 sibling, 2 replies; 24+ messages in thread From: Richard Riehle @ 2000-09-05 17:52 UTC (permalink / raw) Robert Dewar wrote: in response to article article <39B15EA8.88DB58AB@netcourrier.com> by Mathias Dolidon <matd@netcourrier.com>: > THe obvious answer is that a goto could be used, however, it is > almost certain that if we saw the entire code we would suggest > some other method. In particular, it is not at all clear why > you are using a block at all, it appears useless but of course > we do not have your entire code. This raises another interesting question regarding Ada design style. I know of one manager with responsibility for embedded Ada software who prohibits declare blocks in the code. In his mind, a declare block is an ad hoc construct that demonstrates insufficient attention to the overall design. In particular, when one is tempted to code a declare block, he insists it be promoted to a nested procedure accompanied, if necessary, by a pragma Inline. His point-of-view evolved over many years of watching declare blocks grow to cover several pages, become more convulted with the nesting of additional declare blocks during program maintenance, and transmogrify into long passages of increasingly unreadable code. It seems the declare block may be something akin to the Q&D programs we used to write (waddaya mean "used to", cries the chorus) where sloppy coding style was OK because the program was "small and no one would ever want to used it again anyway." So, are declare blocks, echoing the ancient Jeremiad of Dijkstra, "considered dangerous" ? Richard Riehle ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-05 17:52 ` Richard Riehle @ 2000-09-06 2:06 ` Ted Dennison 2000-09-06 9:41 ` Philip Anderson 2000-09-06 7:00 ` Ray Blaak 1 sibling, 1 reply; 24+ messages in thread From: Ted Dennison @ 2000-09-06 2:06 UTC (permalink / raw) Richard Riehle wrote: > Robert Dewar wrote: > > This raises another interesting question regarding Ada design style. I > know of one manager > with responsibility for embedded Ada software who prohibits declare > blocks in the code. > In his mind, a declare block is an ad hoc construct that demonstrates > insufficient attention > to the overall design. In particular, when one is tempted to code a > declare block, he insists > it be promoted to a nested procedure accompanied, if necessary, by a > pragma Inline. I know I pretty much follow that rule myself. But I'm not sure I'd like to see it elevated to Law. I do occasionaly like to use "declare" for sizing arrays (particularly strings) dynamicly on the stack. I think I've also used them in the "accept" alternatives of server tasks or in branches of large command-processing case statements to declare local variables that are unique to that alternative. About the only other reason I ever use a declare is to declare local variables that are used in the exception code of a block's exception handler. It'd be a bit excessive to create a new routine just because the exception handler needs a variable. It makes sense to limit the variable's scope to the block, since that's the only place its used and the block is already there. -- T.E.D. Home - mailto:dennison@telepath.com Work - mailto:dennison@ssd.fsi.com WWW - http://www.telepath.com/dennison/Ted/TED.html ICQ - 10545591 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-06 2:06 ` Ted Dennison @ 2000-09-06 9:41 ` Philip Anderson 2000-09-06 13:54 ` Ted Dennison 0 siblings, 1 reply; 24+ messages in thread From: Philip Anderson @ 2000-09-06 9:41 UTC (permalink / raw) Ted Dennison wrote: > > I know I pretty much follow that rule myself. But I'm not sure I'd like to > see it elevated to Law. I do occasionaly like to use "declare" for sizing > arrays (particularly strings) dynamicly on the stack. I think I've also used > them in the "accept" alternatives of server tasks or in branches of large > command-processing case statements to declare local variables that are > unique to that alternative. > > About the only other reason I ever use a declare is to declare local > variables that are used in the exception code of a block's exception > handler. It'd be a bit excessive to create a new routine just because the > exception handler needs a variable. It makes sense to limit the variable's > scope to the block, since that's the only place its used and the block is > already there. I'd agree with that in general, but it's a not unreasonable restriction to impose if restrictions are being imposed. Declare blocks are excluded in SPARK, and it makes sense there; most of the situations where you and I might use it are not applicable in SPARK anyway - no dynamic arrays, tasks or exceptions. Branches of case statements could arise, but it would seem more readable to call a procedure if one is that complicated. -- hwyl/cheers, Philip Anderson Alenia Marconi Systems Cwmbr�n, Cymru/Wales ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-06 9:41 ` Philip Anderson @ 2000-09-06 13:54 ` Ted Dennison 2000-09-06 21:10 ` Robert Dewar 0 siblings, 1 reply; 24+ messages in thread From: Ted Dennison @ 2000-09-06 13:54 UTC (permalink / raw) Philip Anderson wrote: > Ted Dennison wrote: > > > > arrays (particularly strings) dynamicly on the stack. I think I've also used > > them in the "accept" alternatives of server tasks or in branches of large > > command-processing case statements to declare local variables that are > > unique to that alternative. > > anyway - no dynamic arrays, tasks or exceptions. Branches of case > statements could arise, but it would seem more readable to call a > procedure if one is that complicated. That's quite true for a complicated branch. But I wasn't talking about a complicated branch. I was talking about a simple branch in a large case statement (like one I wrote for a embedded device using Alsys's SPARK compiler :-). This kind of thing happens in command processors a lot. Many of the branches may need variables that no other branch requires. You could make each small branch a subprogram. But that would give you tons of little 3-line subprograms, and you *still* have the huge case statement. Of course one way to handle this now is to use tagged types and dynamic dispatching. But if the commands come in from outside the Ada system (as they did in the system I mentioned above) that won't work. There's no simple way to convert a command ID into a tagged type's tag. I'd also dispute the idea that since SPARK disallows a lot of Ada constructs, its OK to disallow more of them by fiat. To the contrary, I think you *need* all the language features you can get in SPARK. For instance, pointers are *not* disallowed in SPARK (at least not by the compiler I used). The allocator "new" was not available, but that's not the same thing. But I found it invaluable to be able to use pointers (which I acquired by unchecked_conversion'ing addresses). Many other developers on the project acted as if pointers were prohibited. So they had to achieve the same effect using "for use at" overlays, which caused no end of troubles during integration (in addition to being erronious code when the types weren't always the same). -- T.E.D. Home - mailto:dennison@telepath.com Work - mailto:dennison@ssd.fsi.com WWW - http://www.telepath.com/dennison/Ted/TED.html ICQ - 10545591 ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-06 13:54 ` Ted Dennison @ 2000-09-06 21:10 ` Robert Dewar 2000-09-06 23:33 ` Ed Falis 0 siblings, 1 reply; 24+ messages in thread From: Robert Dewar @ 2000-09-06 21:10 UTC (permalink / raw) In article <39B64E94.F081DCAB@telepath.com>, Ted Dennison <dennison@telepath.com> wrote: > (like one I wrote for a embedded device using Alsys's SPARK compiler :-). That's the first I have heard of Alsys having a compiler for SPARK, are you sure you mean what you say here? Remember that SPARK is not just an Ada subset, it is a superset of a subset, since the assertions are a critical part of the syntax and semantics of SPARK, and I do not know of any compiler outside Praxis that compiles this language currently. I mention this, because I often find that people think of SPARK, quite incorrectly, as simply an Ada subset. Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-06 21:10 ` Robert Dewar @ 2000-09-06 23:33 ` Ed Falis 2000-09-07 0:39 ` Robert Dewar [not found] ` <39B72109.89DFAB8C@telepath.com> 0 siblings, 2 replies; 24+ messages in thread From: Ed Falis @ 2000-09-06 23:33 UTC (permalink / raw) I suspect Ted meant SPARC. I never saw one for SPARK while I was there. - Ed Robert Dewar wrote: > In article <39B64E94.F081DCAB@telepath.com>, > Ted Dennison <dennison@telepath.com> wrote: >> (like one I wrote for a embedded device using Alsys's SPARK > compiler :-). > > That's the first I have heard of Alsys having a compiler for > SPARK, are you sure you mean what you say here? Remember that > SPARK is not just an Ada subset, it is a superset of a subset, > since the assertions are a critical part of the syntax and > semantics of SPARK, and I do not know of any compiler outside > Praxis that compiles this language currently. > > I mention this, because I often find that people think of > SPARK, quite incorrectly, as simply an Ada subset. > > > Sent via Deja.com http://www.deja.com/ > Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-06 23:33 ` Ed Falis @ 2000-09-07 0:39 ` Robert Dewar [not found] ` <39B72109.89DFAB8C@telepath.com> 1 sibling, 0 replies; 24+ messages in thread From: Robert Dewar @ 2000-09-07 0:39 UTC (permalink / raw) In article <PM000370A5FE179FB4@Dogen.ne.mediaone.net>, Ed Falis <efalis@mediaone.net> wrote: > I suspect Ted meant SPARC. I never saw one for SPARK while I was there. Ah yes, that sounds likely, Unfortunately English is not strongly typed (otherwise we would not mix up hardware architecturers and programming languages :-) Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
[parent not found: <39B72109.89DFAB8C@telepath.com>]
* Re: exiting a bloc [not found] ` <39B72109.89DFAB8C@telepath.com> @ 2000-09-07 12:34 ` Ed Falis 2000-09-08 10:33 ` Ian Caldwell 0 siblings, 1 reply; 24+ messages in thread From: Ed Falis @ 2000-09-07 12:34 UTC (permalink / raw) Ah, now it becomes clear. That was the old "SMART" (Small Ada Run-Time) that was packaged as an option with 68K and X86 targeted cross-compilers. The analogy to SPARK may have come up because it was used as the basis of a safety certification package that could be incorporated into customers' materials. - Ed Ted Dennison wrote: > Ed Falis wrote: > >> I suspect Ted meant SPARC. I never saw one for SPARK while I was > there. > I suppose confusion on that point is a disticnt possibility, as it was > over > 10 years ago, and it happened to be hosted on a SPARC box (targeted > to a > Motorolla 68020). I went looking for info on the compiler, but it > apparently > no longer exists. There isn't even any info in the 83 validation list > on it. > But I guess that shouldn't suprise me, since it was a subset of Ada. > > But I do distictly remember the topic comming up with Thompson in > relation > to the compiler's feature set. Perhaps what I'm remembering was some > Thompson sales guy comparing it to SPARK (aka: lying). Or perhaps I'm > just > hallucinating. :-) > > I went looking for some SPARK info on the web, and I can tell right > away > that the compiler I used had more Ada features than SPARK seems to. > For > instance, it *did* have acces types, just no allocator or > Unchecked_Deallocation. It didn't have tasking. But I don't remember > it > having anything like SPARK's "Mandatory Annotations". > > -- > T.E.D. > > Home - mailto:dennison@telepath.com Work - > mailto:dennison@ssd.fsi.com > WWW - http://www.telepath.com/dennison/Ted/TED.html ICQ - 10545591 > > ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-07 12:34 ` Ed Falis @ 2000-09-08 10:33 ` Ian Caldwell 2000-09-08 13:35 ` r_c_chapman 2000-09-09 1:48 ` Robert Dewar 0 siblings, 2 replies; 24+ messages in thread From: Ian Caldwell @ 2000-09-08 10:33 UTC (permalink / raw) At least one of the Alsys 'SMART' system, that was produced for one customer, had the requirment to compile the SPARK subset of Ada. I think that all the Alsys 'SMART' system would compile the SPARK subset of Ada. In article <PM000370B0EBA888B3@Dogen.ne.mediaone.net>, efalis@mediaone.net says... > >Ah, now it becomes clear. That was the old "SMART" (Small Ada Run-Time) >that was packaged as an option with 68K and X86 targeted >cross-compilers. The analogy to SPARK may have come up because it was >used as the basis of a safety certification package that could be >incorporated into customers' materials. > >- Ed > ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-08 10:33 ` Ian Caldwell @ 2000-09-08 13:35 ` r_c_chapman 2000-09-09 1:52 ` Robert Dewar 2000-09-12 11:30 ` Ian Caldwell 2000-09-09 1:48 ` Robert Dewar 1 sibling, 2 replies; 24+ messages in thread From: r_c_chapman @ 2000-09-08 13:35 UTC (permalink / raw) In article <8paf97$ceb$1@trog.dera.gov.uk>, icaldwell@dera.gov.uk (Ian Caldwell) wrote: > At least one of the Alsys 'SMART' system, that was produced for one customer, > had the requirment to compile the SPARK subset of Ada. I think that all the > Alsys 'SMART' system would compile the SPARK subset of Ada. Arrghh! Clarification follows: SPARK - an annotated subset of Ada from Praxis Critical Systems. SPARC(tm) - Computer architecture - Sun Microsystems & SPARC Itnl Inc. SMART - Small Ada83 runtime system from Alsys/TSP/Aonix C-SMART - SMART with certification package. Everybody got that!?!?! And for desserts - the shocking realisation that Robert got something wrong on c.l.a - Praxis certainly don't make a compiler for SPARK - we make a static analysis tool called the Examiner. SPARK is compiled with any standard Ada compiler, including those hosted on and/or targetting SPARC(tm) and or using [C-]SMART as a runtime (or RAVEN, VADSsc, ApexMARK, GNORT, Integrity etc. etc.)! Phew! - Rod, Praxis Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-08 13:35 ` r_c_chapman @ 2000-09-09 1:52 ` Robert Dewar 2000-09-12 11:30 ` Ian Caldwell 1 sibling, 0 replies; 24+ messages in thread From: Robert Dewar @ 2000-09-09 1:52 UTC (permalink / raw) In article <8papum$kaf$1@nnrp1.deja.com>, r_c_chapman@my-deja.com wrote: > And for desserts - the shocking realisation that Robert got > something wrong on c.l.a - Praxis certainly don't > make a compiler for SPARK - we make a static analysis > tool called the Examiner. > > SPARK is compiled with any standard Ada compiler, > including those hosted on and/or targetting SPARC(tm) > and or using [C-]SMART as a runtime (or RAVEN, VADSsc, > ApexMARK, GNORT, Integrity etc. etc.)! Actually I sort of think of Examiner as a compiler for SPARK in the sense that a critical part of any compiler is semantic verification that the program is legal, and that is what the examiner does. Yes, there is also the little detail of generating code once this semantic checking is complete, but any old Ada compiler can do that :-) So really a SPARK compiler must do both annotation checking and the normal code generation of a compiler, so the way you get a compiler for SPARK today is to put the Examiner together with a compiler (such as GNAT :-). So Rod is quite right, I should not have said that Praxis has a compiler for SPARK, I should have said that they make the most critical part of the SPARK compiler! Actually a full blown integrated compiler for SPARK might well be able to take advantage of the annotations to improve code quality, eliminate checks etc, but so far no one has produced such a beast. Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-08 13:35 ` r_c_chapman 2000-09-09 1:52 ` Robert Dewar @ 2000-09-12 11:30 ` Ian Caldwell 2000-09-12 20:13 ` Robert Dewar 1 sibling, 1 reply; 24+ messages in thread From: Ian Caldwell @ 2000-09-12 11:30 UTC (permalink / raw) Just to clarify a bit more, one of the meanings of the C in C-SMART was Certifiable and not Certified. In article <8papum$kaf$1@nnrp1.deja.com>, r_c_chapman@my-deja.com says... > > > >Arrghh! Clarification follows: > >SPARK - an annotated subset of Ada from Praxis Critical Systems. >SPARC(tm) - Computer architecture - Sun Microsystems & SPARC Itnl Inc. >SMART - Small Ada83 runtime system from Alsys/TSP/Aonix >C-SMART - SMART with certification package. > >Everybody got that!?!?! > >And for desserts - the shocking realisation that Robert got >something wrong on c.l.a - Praxis certainly don't >make a compiler for SPARK - we make a static analysis >tool called the Examiner. > >SPARK is compiled with any standard Ada compiler, >including those hosted on and/or targetting SPARC(tm) >and or using [C-]SMART as a runtime (or RAVEN, VADSsc, >ApexMARK, GNORT, Integrity etc. etc.)! > >Phew! > - Rod, Praxis > > The views expressed herein are entirely those of the writer and do not represent the views, policy or understanding of any other person or official body. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-12 11:30 ` Ian Caldwell @ 2000-09-12 20:13 ` Robert Dewar 0 siblings, 0 replies; 24+ messages in thread From: Robert Dewar @ 2000-09-12 20:13 UTC (permalink / raw) In article <8pl43r$ivi$2@trog.dera.gov.uk>, icaldwell@dera.gov.uk (Ian Caldwell) wrote: > Just to clarify a bit more, one of the meanings of the C in > C-SMART was Certifiable and not Certified. The important distinction here is that it is entire applications that are certified, not components of them. So what a product like C-SMART entails is software together with all the materials that need to be used in incorporating it into the certification of the entire application, where C-SMART is one component. This is important to understand, we have come across customers quite sure they wanted certifiED stuff. In fact of course the C of C-SMART does not capture quite enough, because the idea isn't just that C-SMART is certifiable, but rather that it's (relatively) easy to do the certification, since all the hard work has been done already. The same kind of considerations apply to libraries and runtime executives, kernels and operating systems. Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-08 10:33 ` Ian Caldwell 2000-09-08 13:35 ` r_c_chapman @ 2000-09-09 1:48 ` Robert Dewar 2000-09-12 11:24 ` Ian Caldwell 1 sibling, 1 reply; 24+ messages in thread From: Robert Dewar @ 2000-09-09 1:48 UTC (permalink / raw) In article <8paf97$ceb$1@trog.dera.gov.uk>, icaldwell@dera.gov.uk (Ian Caldwell) wrote: > At least one of the Alsys 'SMART' system, that was produced for one customer, > had the requirment to compile the SPARK subset of Ada. I think that all the > Alsys 'SMART' system would compile the SPARK subset of Ada. Right, but talking about the "SPARK subset of Ada" is misleading sales talk. SPARK is *not* a subset of Ada. The annotations are a fundamental part of the SPARK language. Yes, there is a language that is defined as SPARK without any its annotations, and that is what compilers might well (actually most certainly *should*) be able to compile, but this is NOT SPARK. The distinction is important, because if you think of the SPARK annotations as merely some unimportant documentation, you are definitely missing the point :-) Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-09 1:48 ` Robert Dewar @ 2000-09-12 11:24 ` Ian Caldwell 2000-09-12 20:14 ` Robert Dewar 0 siblings, 1 reply; 24+ messages in thread From: Ian Caldwell @ 2000-09-12 11:24 UTC (permalink / raw) When I used "the SPARK subset of Ada" I meant SPARK without any of its annotations. I know that not the full SPARK language. Maybe I should have used the Ada subset of SPARK (meaning the part of SPARK that is Ada). In article <8pc4tc$8j1$1@nnrp1.deja.com>, robert_dewar@my-deja.com says... > >In article <8paf97$ceb$1@trog.dera.gov.uk>, > icaldwell@dera.gov.uk (Ian Caldwell) wrote: > >> At least one of the Alsys 'SMART' system, that was produced >for one customer, >> had the requirment to compile the SPARK subset of Ada. I think >that all the >> Alsys 'SMART' system would compile the SPARK subset of Ada. > >Right, but talking about the "SPARK subset of Ada" is misleading >sales talk. SPARK is *not* a subset of Ada. The annotations are >a fundamental part of the SPARK language. > >Yes, there is a language that is defined as SPARK without any >its annotations, and that is what compilers might well (actually >most certainly *should*) be able to compile, but this is NOT >SPARK. The distinction is important, because if you think of >the SPARK annotations as merely some unimportant documentation, >you are definitely missing the point :-) > > >Sent via Deja.com http://www.deja.com/ >Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-12 11:24 ` Ian Caldwell @ 2000-09-12 20:14 ` Robert Dewar 2000-09-13 8:34 ` Philip Anderson 0 siblings, 1 reply; 24+ messages in thread From: Robert Dewar @ 2000-09-12 20:14 UTC (permalink / raw) In article <8pl3qa$ivi$1@trog.dera.gov.uk>, icaldwell@dera.gov.uk (Ian Caldwell) wrote: > When I used "the SPARK subset of Ada" I meant SPARK without any of its > annotations. I know that not the full SPARK language. Maybe I should have used > the Ada subset of SPARK (meaning the part of SPARK that is Ada). It would be convenient (and perhaps avoid confusion) to have a clear name for that subset :-) Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-12 20:14 ` Robert Dewar @ 2000-09-13 8:34 ` Philip Anderson 2000-09-13 11:02 ` Peter Amey 0 siblings, 1 reply; 24+ messages in thread From: Philip Anderson @ 2000-09-13 8:34 UTC (permalink / raw) Robert Dewar wrote: > > In article <8pl3qa$ivi$1@trog.dera.gov.uk>, > icaldwell@dera.gov.uk (Ian Caldwell) wrote: > > When I used "the SPARK subset of Ada" I meant SPARK without > any of its > > annotations. I know that not the full SPARK language. Maybe I > should have used > > the Ada subset of SPARK (meaning the part of SPARK that is > Ada). > > It would be convenient (and perhaps avoid confusion) to have > a clear name for that subset :-) Praxis refer to the overlap between SPARK and Ada as "the common kernel"; the SPARK core is then this common kernel + the core annotations (there are also optional proof annotations). The SPARK Ada kernel is probably the least ambiguous term. For those who don't know, the SPARK annotations take the form of Ada comments with a defined syntax, all beginning --# (or --$ in our case), and so a SPARK program is legal Ada and can be compiled by any Ada compiler; the SPARK Examiner is an additional tool which does not compile but verifies the SPARK code (the Ada kernel + annotations). In addition, something like Rational's Apex Ada Analyser can be set up to analyse an Ada program and flag non-SPARK Ada, but that does nothing with annotations of course. -- hwyl/cheers, Philip Anderson Alenia Marconi Systems Cwmbr�n, Cymru/Wales ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-13 8:34 ` Philip Anderson @ 2000-09-13 11:02 ` Peter Amey 0 siblings, 0 replies; 24+ messages in thread From: Peter Amey @ 2000-09-13 11:02 UTC (permalink / raw) In article <39BF3C11.CA3A9347@amsjv.com>, Philip Anderson <phil.anderson@amsjv.com> wrote: > Robert Dewar wrote: > > > > In article <8pl3qa$ivi$1@trog.dera.gov.uk>, > > icaldwell@dera.gov.uk (Ian Caldwell) wrote: > > > When I used "the SPARK subset of Ada" I meant SPARK without > > any of its > > > annotations. I know that not the full SPARK language. Maybe I > > should have used > > > the Ada subset of SPARK (meaning the part of SPARK that is > > Ada). > > > > It would be convenient (and perhaps avoid confusion) to have > > a clear name for that subset :-) > > Praxis refer to the overlap between SPARK and Ada as "the common > kernel"; the SPARK core is then this common kernel + the core > annotations (there are also optional proof annotations). The SPARK Ada > kernel is probably the least ambiguous term. > > For those who don't know, the SPARK annotations take the form of Ada > comments with a defined syntax, all beginning --# (or --$ in our case), > and so a SPARK program is legal Ada and can be compiled by any Ada > compiler; the SPARK Examiner is an additional tool which does not > compile but verifies the SPARK code (the Ada kernel + annotations). In > addition, something like Rational's Apex Ada Analyser can be set up to > analyse an Ada program and flag non-SPARK Ada, but that does nothing > with annotations of course. > It is important to realise, however, that without the mandatory annotations it is extremely hard (impossible without a 'whole program' analysis) to say whether a piece of code is written in SPARK or not. It is only the presence of annotations that makes, for example, aliasing and function side effects (both prohibited in SPARK) detectable in reasonable computation times or in incomplete programs. The elimination of errors at the coding stage is one of the factors that makes SPARK use so cost effective; certainly it is better than waiting until the code is finished and then trying to find errors retrospectively. Analysers (other than the SPARK Examiner of course) which claim to check for SPARK compliance only do very crude checking for major prohibited constructs such as tasking or the use of "new". Peter Sent via Deja.com http://www.deja.com/ Before you buy. ^ permalink raw reply [flat|nested] 24+ messages in thread
* Re: exiting a bloc 2000-09-05 17:52 ` Richard Riehle 2000-09-06 2:06 ` Ted Dennison @ 2000-09-06 7:00 ` Ray Blaak 1 sibling, 0 replies; 24+ messages in thread From: Ray Blaak @ 2000-09-06 7:00 UTC (permalink / raw) Richard Riehle <laoXhai@ix.netcom.com> writes: > I know of one manager with responsibility for embedded Ada software who > prohibits declare blocks in the code [...nested procedures are better...] His > point-of-view evolved over many years of watching declare blocks grow to > cover several pages, become more convulted with the nesting of additional > declare blocks during program maintenance, and transmogrify into long > passages of increasingly unreadable code. This doesn't make sense to me. If the problem is large blocks of code, then the solution is to break the large blocks into smaller blocks. Declare blocks themselves are not the problem, and banning them doesn't fix the problem. After all, nested procedures can also grow as well, until the over all routine is simply huge and unwieldy. The rule should simply be: "do things right!". Use the right language language features for the situation, so that the result is beautiful crystaline code. Other stupid rules: no recursion, no instantiations in procedures, no nested procedures, no access types... I once saw someone, in accordance to the no access types rule, implement an abstract string referencing scheme using private integers to index into a pool of string "chunks". Basically he reimplemented pointers all over again, with the same lost and dangling reference bugs being possible. Using access types directly would have been much much simpler, faster, easier to understand and maintain, as well as more amenable to the automated detection of memory leaks by system tools. The moral of the story is that banning language features by fiat is stupid. One should instead understand why a feature should not be used in certain situations, and what is the right feature to use instead, or at least what can be done to use the feature in the right way. > So, are declare blocks, echoing the ancient Jeremiad of Dijkstra, > "considered dangerous" ? I don't see how, any more than routines in general can be dangerous. -- Cheers, The Rhythm is around me, The Rhythm has control. Ray Blaak The Rhythm is inside me, blaak@infomatch.com The Rhythm has my soul. ^ permalink raw reply [flat|nested] 24+ messages in thread
end of thread, other threads:[~2000-09-13 11:02 UTC | newest] Thread overview: 24+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2000-09-02 20:10 exiting a bloc Mathias Dolidon 2000-09-02 20:39 ` Mathias Dolidon 2000-09-02 21:01 ` Robert Dewar 2000-09-02 22:34 ` Mathias Dolidon [not found] ` <86snrhkfep.fsf@acm.org> 2000-09-03 15:46 ` Mathias Dolidon 2000-09-05 17:52 ` Richard Riehle 2000-09-06 2:06 ` Ted Dennison 2000-09-06 9:41 ` Philip Anderson 2000-09-06 13:54 ` Ted Dennison 2000-09-06 21:10 ` Robert Dewar 2000-09-06 23:33 ` Ed Falis 2000-09-07 0:39 ` Robert Dewar [not found] ` <39B72109.89DFAB8C@telepath.com> 2000-09-07 12:34 ` Ed Falis 2000-09-08 10:33 ` Ian Caldwell 2000-09-08 13:35 ` r_c_chapman 2000-09-09 1:52 ` Robert Dewar 2000-09-12 11:30 ` Ian Caldwell 2000-09-12 20:13 ` Robert Dewar 2000-09-09 1:48 ` Robert Dewar 2000-09-12 11:24 ` Ian Caldwell 2000-09-12 20:14 ` Robert Dewar 2000-09-13 8:34 ` Philip Anderson 2000-09-13 11:02 ` Peter Amey 2000-09-06 7:00 ` Ray Blaak
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox