Prev: More Ada in Cryptography.
Next: What Ada can do for Cryptography.
From: Claude on 18 Jun 2010 02:07
On Jun 17, 8:33 am, Yannick Duchêne (Hibou57)
<yannick_duch...(a)yahoo.fr> wrote:
> Hello,
>
> (This topic will probably not be the most exiting topic to some people).
>
> When I use SPARK, or even when I don't use SPARK while I still have SPARK  
> design style in mind (even with Pascal which I still use), I have like any  
> one else, to forget about exceptions.
>
> So, let us talk and comment about design strategies in this area (if  
> someones wish to).

Hello Yannick

You are talking about Ada. Just add annotation and you get SPARK and
static analysis.

SPARK is about
- Data and information flow analysis annotations ensure that data
are used in the expected way.
- Proof of absence of run-time errors that can spare exception error
handling and defensive programming.

Just have a look on the Phil Torney web site (SparkSure) and download
his Proof of Absence of Run-Time Error tutorial
http://www.sparksure.com/resources/Proof_Annotations.zip

It worth to have a glance at it...

Claude
From: Phil Thornley on 18 Jun 2010 04:06
On 17 June, 16:33, Yannick Duchêne (Hibou57)
<yannick_duch...(a)yahoo.fr> wrote:
> Hello,
>
> (This topic will probably not be the most exiting topic to some people).
>
> When I use SPARK, or even when I don't use SPARK while I still have SPARK  
> design style in mind (even with Pascal which I still use), I have like any  
> one else, to forget about exceptions.
>
> The only one thing which seems simple and clean enough I could figure, is  
> to use a Boolean variable, named “OK”, and a sequence of “if OK then”  
> statements. That is, execution of one sequence of statements, which set OK  
> to False is something goes wrong, and execute clean-up statements by the  
> way. Then a next sequence of statements wrapped in a “if OK then” which do  
> the same, and so on with next statements groups which are also wrapped in  
> a “if OK then” (as many as needed).
>
> Although this seems clean and maintainable enough to me so far, I was  
> still wondering how other people deal with this (and may be by the way, I  
> may have comment about why my way could be bad in some way).
>
> Note: a similar strategy may also obviously applies to fulfill the “only  
> one single exit point” requirement.
>
> So, let us talk and comment about design strategies in this area (if  
> someones wish to).

(Perhaps not an entirely serious suggestion, but...)
The only way of interrupting a code sequence in SPARK is the exit
statement for a loop, so one possibility might be to create a 'single
pass' loop with an unconditional exit at the end.

Unfortunately such an unconditional exit is illegal, so you have to
use 'exit when True;'

Also there may be flow errors for some or all of the 'exit when'
statements (if the OK values only depend on the program inputs) - but
here we can put an accept statement - which will usefully document
that the loop is a not a real loop.

--# accept F, 40, "This is a single pass loop.";
OK := True;
loop
Some complicated code that might set OK;
exit when not OK;
Some more complicated code that might set OK;
exit when not OK;
Some more code;
exit when True;
end loop;

:-)

Cheers,

Phil
From: Martin on 18 Jun 2010 04:49
On Jun 18, 9:06 am, Phil Thornley <phil.jpthorn...(a)gmail.com> wrote:
> On 17 June, 16:33, Yannick Duchêne (Hibou57)
>
>
>
> <yannick_duch...(a)yahoo.fr> wrote:
> > Hello,
>
> > (This topic will probably not be the most exiting topic to some people)..
>
> > When I use SPARK, or even when I don't use SPARK while I still have SPARK  
> > design style in mind (even with Pascal which I still use), I have like any  
> > one else, to forget about exceptions.
>
> > The only one thing which seems simple and clean enough I could figure, is  
> > to use a Boolean variable, named “OK”, and a sequence of “if OK then”  
> > statements. That is, execution of one sequence of statements, which set OK  
> > to False is something goes wrong, and execute clean-up statements by the  
> > way. Then a next sequence of statements wrapped in a “if OK then” which do  
> > the same, and so on with next statements groups which are also wrapped in  
> > a “if OK then” (as many as needed).
>
> > Although this seems clean and maintainable enough to me so far, I was  
> > still wondering how other people deal with this (and may be by the way, I  
> > may have comment about why my way could be bad in some way).
>
> > Note: a similar strategy may also obviously applies to fulfill the “only  
> > one single exit point” requirement.
>
> > So, let us talk and comment about design strategies in this area (if  
> > someones wish to).
>
> (Perhaps not an entirely serious suggestion, but...)
> The only way of interrupting a code sequence in SPARK is the exit
> statement for a loop, so one possibility might be to create a 'single
> pass' loop with an unconditional exit at the end.
>
> Unfortunately such an unconditional exit is illegal, so you have to
> use 'exit when True;'
>
> Also there may be flow errors for some or all of the 'exit when'
> statements (if the OK values only depend on the program inputs) - but
> here we can put an accept statement - which will usefully document
> that the loop is a not a real loop.
>
> --# accept F, 40, "This is a single pass loop.";
> OK := True;
> loop
>    Some complicated code that might set OK;
>    exit when not OK;
>    Some more complicated code that might set OK;
>    exit when not OK;
>    Some more code;
>    exit when True;
> end loop;
>
> :-)
>
> Cheers,
>
> Phil

No there's a fancy 'goto'! :-)

-- Martin
From: mockturtle on 18 Jun 2010 13:16
On Jun 18, 10:49 am, Martin <martin.do...(a)btopenworld.com> wrote:
> (snip)
> > OK := True;
> > loop
> >    Some complicated code that might set OK;
> >    exit when not OK;
> >    Some more complicated code that might set OK;
> >    exit when not OK;
> >    Some more code;
> >    exit when True;
> > end loop;
>
> > :-)
>
> > Cheers,
>
> > Phil
>
> No there's a fancy 'goto'! :-)
>
> -- Martin

Well, I do not know if 'goto's are allowed in SPARK, but that is the
solution that sometimes I use when I need to write code in the-
language-whose-name-is-a-single-letter :-). I know that it could
sound heretical, but this is one of the two cases where, I believe,
using goto is not so bad. I am thinking something like

procedure Very_Complex_Stuff (OK : out Boolean) is
begin
OK := True; -- Be optimistic :-)
Open_some_file (OK);
if not OK then
goto Exit_now;
end if;

Allocate_Some_Memory (OK);
if not OK then
goto Undo_Open;
end if;

Contact_DB (OK);
if not OK then
goto Undo_Mem;
end if;

goto Exit_Now;

<<Undo_Mem>>
Deallocate_Memory;

<<Undo_Open>>
Close_File;

<<Exit_Now>>
end;

I agree that this will not win the prize for the best code ever, but
if you choose your labels with care it can turn out an acceptable
solution.


From: Alexandre K on 18 Jun 2010 17:51

> Well, I do not know if 'goto's are allowed in SPARK, but that is the
> solution that sometimes I use when I need to write code in the-
> language-whose-name-is-a-single-letter :-).  I know that it could
> sound heretical, but this is one of the two cases where, I believe,
> using goto is not so bad.  I am thinking something like

Hi everyone,

Well, Goto are, as exceptions, not allowed in Spark.
To answer to Yannick, the way to replace exception is to use Boolean,
or Enumerates in an "out" parameter.
It is the case when you need to use an Ada program that uses
exceptions, and you have to write
a package specification with Spark and hide the implementation in the
body. (--# hide).
The Spark_IO package is an example of hiding the use of Ada.Text_IO,
and of course File exception.

Also, I think we should not use exception to control the flow of the
program.

Alex.
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5
Prev: More Ada in Cryptography.
Next: What Ada can do for Cryptography.