exiting a bloc

exiting a bloc

[Mathias Dolidon]

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

Re: exiting a bloc

[Mathias Dolidon]

> 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

Re: exiting a bloc

[Robert Dewar]

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.

Re: exiting a bloc

[Mathias Dolidon]

> 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

Re: exiting a bloc

[Mathias Dolidon]

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 !

Re: exiting a bloc

[Richard Riehle]

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

Re: exiting a bloc

[Ted Dennison]

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

Re: exiting a bloc

[Ray Blaak]

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.

Re: exiting a bloc

[Philip Anderson]

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

Re: exiting a bloc

[Ted Dennison]

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

Re: exiting a bloc

[Robert Dewar]

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.

Re: exiting a bloc

[Ed Falis]

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.

Re: exiting a bloc

[Robert Dewar]

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.

Re: exiting a bloc

[Ed Falis]

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
>
>

Re: exiting a bloc

[Ian Caldwell]

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
>

Re: exiting a bloc

[r_c_chapman]

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.

Re: exiting a bloc

[Robert Dewar]

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.

Re: exiting a bloc

[Robert Dewar]

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.

Re: exiting a bloc

[Ian Caldwell]

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.

Re: exiting a bloc

[Ian Caldwell]

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. 

Re: exiting a bloc

[Robert Dewar]

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.

Re: exiting a bloc

[Robert Dewar]

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.

Re: exiting a bloc

[Philip Anderson]

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

Re: exiting a bloc

[Peter Amey]

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.