SPARK

SPARK

[programmer]

I have been to various web sites like www.sparkada.com in an effort
to research the SPARK language.

Is SPARK Examiner the only SPARK language tool available?

What is the cost?

Are there any open source alternatives?

I am fascinated by the concept of verifying correctness
completely at compiler/pre-compile time.

Answers to my questions and any additional information
would be greatly appreciated.

Thanks.

Re: SPARK

[Hambut]

"programmer" <nospam@nowhere.com> wrote in message news:<UUzb7.42923$uj2.7462172@news02.optonline.net>...
> I have been to various web sites like www.sparkada.com in an effort
> to research the SPARK language.
> 
> Is SPARK Examiner the only SPARK language tool available?

Yes.

> 
> What is the cost?

Well you certainly couldn't contemplate buying it personally.  Perhaps
one of the readers from Praxis might want to comment.

You can get a restricted version in the back to the SPARK book by John
Barnes (Unfortunately I don't have it to hand, and so can't give the
correct title).  I think it's restricted with respect to size of
software it will analyse,and to the level of analysis it carried out.

> 
> Are there any open source alternatives?

Not that I'm aware of.  Now there's an idea for a useful tool someone
could develop as open source........

<snip>

Re: SPARK

[Hambut]

Here's a link to John Barne's book "High Integrity Ada":

http://www.amazon.co.uk/exec/obidos/ASIN/0201175177/202-2966724-2375825

Re: SPARK

[Peter Amey]

programmer wrote:
> 
> I have been to various web sites like www.sparkada.com in an effort
> to research the SPARK language.
> 
> Is SPARK Examiner the only SPARK language tool available?
> 
> What is the cost?
> 
> Are there any open source alternatives?
> 
> I am fascinated by the concept of verifying correctness
> completely at compiler/pre-compile time.
> 
> Answers to my questions and any additional information
> would be greatly appreciated.


Thanks for the interest (and to Hambut who provided some accurate
answers).

There are two aspects to SPARK: the language definition and the analysis
tool (the Examiner).  The ingredients are complementary because it the
tightness of the language definition which permits deep analysis to be
performed in computationally efficient ways.  It also allows the
analysis to be performed on incomplete programs, during development,
which is vital if the approach is to save time and money.

I often characterize SPARK as an "Ada amplifier".  If you think of all
the things like strong typing, constraint checking etc. that makes Ada
efficient at error prevention and early error detection then add in a
whole raft of extra checks ranging from system wide data flow analysis
up to proof of exception freedom then that is SPARK.  (Incidently, to
pick up on another thread in CLA, proof of exception freedom would also
be a proof of invulnerability to buffer overflow attacks without any
run-time overhead.)

The language definition is freely available as is the paper that lays
the foundations of the Examiner's method of data and information flow
analysis.  So, if you are really keen, much of the requirements
specification for an open source alternative to the Examiner exists. 
You should be warned, however, that I have spent most of the last 10
years of my life, with some very high quality help, writing and
improving the Examiner (which BTW is written in SPARK and analyses and
approves of itself) so the task is not one for the faint hearted.

The Barnes book has recently been updated and the publishers have not
done a very good job of telling people about it: if you try and get a
copy and are told it is out of print then tell them they are wrong!  The
demo Examiner is limited only in size; all analysis options are
available.

Finally, those whose appetites have been whetted may like to know that
we are running an open SPARK course in the USA from 24th - 28th
September.  Details on www.sparkada.com

Peter


-- 
---------------------------------------------------------------------------   
      __         Peter Amey,  
        )                    Praxis Critical Systems Ltd
       /                     20, Manvers Street, Bath, BA1 1PX
      / 0        Tel: +44 (0)1225 466991
     (_/         Fax: +44 (0)1225 469006
                 http://www.praxis-cs.co.uk/

--------------------------------------------------------------------------

Re: SPARK

[McDoobie]

Peter Amey wrote:
> 
> programmer wrote:
> 
>>I have been to various web sites like www.sparkada.com in an effort
>>to research the SPARK language.
>>
>>Is SPARK Examiner the only SPARK language tool available?
>>
>>What is the cost?
>>
>>Are there any open source alternatives?
>>
>>I am fascinated by the concept of verifying correctness
>>completely at compiler/pre-compile time.
>>
>>Answers to my questions and any additional information
>>would be greatly appreciated.
>>
> 
> 
> Thanks for the interest (and to Hambut who provided some accurate
> answers).
> 
> There are two aspects to SPARK: the language definition and the analysis
> tool (the Examiner).  The ingredients are complementary because it the
> tightness of the language definition which permits deep analysis to be
> performed in computationally efficient ways.  It also allows the
> analysis to be performed on incomplete programs, during development,
> which is vital if the approach is to save time and money.
> 
> I often characterize SPARK as an "Ada amplifier".  If you think of all
> the things like strong typing, constraint checking etc. that makes Ada
> efficient at error prevention and early error detection then add in a
> whole raft of extra checks ranging from system wide data flow analysis
> up to proof of exception freedom then that is SPARK.  (Incidently, to
> pick up on another thread in CLA, proof of exception freedom would also
> be a proof of invulnerability to buffer overflow attacks without any
> run-time overhead.)
> 
> The language definition is freely available as is the paper that lays
> the foundations of the Examiner's method of data and information flow
> analysis.  So, if you are really keen, much of the requirements
> specification for an open source alternative to the Examiner exists. 
> You should be warned, however, that I have spent most of the last 10
> years of my life, with some very high quality help, writing and
> improving the Examiner (which BTW is written in SPARK and analyses and
> approves of itself) so the task is not one for the faint hearted.
> 
> The Barnes book has recently been updated and the publishers have not
> done a very good job of telling people about it: if you try and get a
> copy and are told it is out of print then tell them they are wrong!  The
> demo Examiner is limited only in size; all analysis options are
> available.
> 
> Finally, those whose appetites have been whetted may like to know that
> we are running an open SPARK course in the USA from 24th - 28th
> September.  Details on www.sparkada.com
> 
> Peter
> 
> 
> 

This is something I'd certainly like to get my hands on. The problem is 
that it costs too damn much!

But, perhaps, instead of re-creating the entire Spark toolchain, one(or 
a group) could create a new toolchain, or an Open Source(or Free 
Software) subset of Spark geared around things that Open Source 
programmers use most often.
I'm sure Praxis could reap a bundle of they were to put together a 
package geared(and priced) towards individual developers, in addition to 
the huge Corporate and Military systems they work with right now. Even 
just a small, but carefully chosen subset of the Spark system, priced 
right, and sitting on the shelf at CompUSA would not only make them 
loads of money(assuming they market it properly), but would likely 
attract large numbers of developers to Ada in general. Not to mention 
making at least a small percentage of overall improvement in the types 
of software being developed today.

Just a thought. Maybe it's wishful thinking.

I would jump at the chance to develop a similar LGPLd package. The 
problem is that I dont have the amount of experience doing actual 
engineering that would be required to develop anything worthwhile. 
However, I'd certainly be glad to work under someone who does.

Thoughts? Possibilities? Potential?

What do the SPARK guys think?

McDoobie
chris@dont.spam.me

SPARK

[Soeren.Henssel-Rasmussen]

Chris,

have a look on the Anna toolset from Stanford:
	Research website	=> http://pavg.stanford.edu/
	Download		=>
ftp://pavg.stanford.edu/pub/anna/anna.intro  (remove "anna.intro" to see all
files)

I worked on the tools a couple of years ago, but has not used it since.  

regards  /soren
Søren Henssel-Rasmussen 
soeren.henssel-rasmussen@nokia.com 

Re: SPARK

[McDoobie]

Soeren.Henssel-Rasmussen@nokia.com wrote:
> Chris,
> 
> have a look on the Anna toolset from Stanford:
> 	Research website	=> http://pavg.stanford.edu/
> 	Download		=>
> ftp://pavg.stanford.edu/pub/anna/anna.intro  (remove "anna.intro" to see all
> files)
> 
> I worked on the tools a couple of years ago, but has not used it since.  
> 
> regards  /soren
> S�ren Henssel-Rasmussen 
> soeren.henssel-rasmussen@nokia.com 
> 
> 

Thanks for the reference.  You can be sure I'll be spending some time 
getting used to these tools. Hopefully, as my experience grows, I'll be 
able to submit some contributions to the project.

McDoobie
chris@dont.spam.me

Re: SPARK

[Peter Amey]

I should, perhaps, have mentioned in my earlier reply that we do provide
fully-supported SPARK tool sets for academic use.  Details are on
sparkada.com.  I appreciate that this does not directly help
hobbyists/enthusiasts/very small projects; we will keep thinking of ways
to serve these potential users.

Peter

Re: SPARK

[Prof Karl Kleine]

Peter Amey <peter.amey@praxis-cs.co.uk> wrote:
[.....]
> The Barnes book has recently been updated and the publishers have not
> done a very good job of telling people about it: if you try and get a
> copy and are told it is out of print then tell them they are wrong!  The
> demo Examiner is limited only in size; all analysis options are
> available.
[.....]

Peter, I just checked the 'SPARK Book' entry on the www.sparkada.com site
and there is an offer of an update of the demo software on the CDROM, but
it does not say anything about the update of the book itself. Yes, I do
own a private copy (of course, being a serious person :-).

Two questions:

 -- Is there an update paper for the book itself, or something to this effect?

 -- How do I recognize the updated book? New isbn? "second edition" in title? 

Thanks!
Karl Kleine

Re: SPARK

[Rod Chapman]

Prof Karl Kleine <kleine@fh-jena.de> wrote in message news:<9la53h$k62$1@beta.szi.fh-jena.de>...
> Peter, I just checked the 'SPARK Book' entry on the www.sparkada.com site
> and there is an offer of an update of the demo software on the CDROM, but
> it does not say anything about the update of the book itself. Yes, I do
> own a private copy (of course, being a serious person :-).
> 
> Two questions:
> 
>  -- Is there an update paper for the book itself, or something to this effect?

Your best bet is to read the Examiner release 5 release note which is
on www.sparkada.com under "Downloads".

By request, we will also send anyone the full SPARK definition.  This
is less easy to read than the book, though (i.e. it's written
in "LRM-speak" rather than "Barnes-speak").

>  -- How do I recognize the updated book? New isbn? "second edition" in title? 

Strictly speaking, it is a second _printing_ (with updates) of the
first edition.  It has "Reprinted with revisions 2000" on the
copyright page,
and the CDROM in the back is labelled "Release 2.00 August 2000"

ISBN is the same.

Hope that helps,
 Rod Chapman
 SPARK Products Manager,
 Praxis Critical Systems
 rod@praxis-cs.co.uk

timeouts

[Brian May]

Hello,

I have a written a communications protocols, for Windows, in Ada,
using the GNAT compiler for Windows. This is my attempt at
implementing the MAP27 protocol (used for talking to trunk radios).

The main protocol is implemented as a separate task along the lines of
the following code. This code is simplified from my actual code, and
only shows the what I consider relevant to this bug, based on print
messages. Any mistakes in syntax are probably copy errors.

I should be able to provide full code on request, but need to confirm
this first.

task body State_Machine_Task is
     timer_enabled : Boolean := True;
     expire_time : Duration := clock + 0.1;
...
begin
   ...
   Put(Log.Debug,"----------------------------------------");
   Put(...);
   Put(timer_enabled,expire_time);
   Put(...);

   while Continue loop
       case SMT.DTE_State is
       when ... => 
            select
                accept ...
                ...
            or
                ...
            or 
               when timer_enabled =>
               delay until expire_time;
               
               print ("In.Link_Establishment_Timeout");

               expire_time := clock + 0.1;
            end select;
       
       when ... =>
            ...

       ...

       end case;                   
   end loop;
end;
   

Generally speaking, the program does all this fine, and constantly
prints the expired message, as required.

However, occasionally something goes wrong, and while it prints the
expiration time OK, it takes ages to print the "expired"
message. e.g. one occasion the event was 7 hours late. This puzzles
me, because every time the timer is incremented by 0.1 seconds, and my
understanding is that the timer should trigger if the current time is
greater then the expiration time.

To be precise, at 1:50:57 am the timer was incremented, and the select
reentered, and at 9:12:59 the timer expired. The actual log produced
is below:

1:50:57 DLL DEBUG Activity_Timer: disabled
1:50:57 DLL DEBUG Link_Failure_Detection_Timer: disabled
1:50:56 DLL DEBUG In.Link_Establishment_Timeout
1:50:56 DLL DEBUG Out.Link_Request( 14, 1, 1)
1:50:56 T50 DEBUG TX Packet Packet( 22  16  2  1  14  1  1  16  3  138  9 )
1:50:57 DLL DEBUG Out.Link_Request return
1:50:57 DLL DEBUG ----------------------------------------
1:50:57 DLL DEBUG looping state=RESET_WAIT
1:50:57 DLL DEBUG Link_Establishment_Timer time 1:50:57
1:50:57 DLL DEBUG Retry_Timer: disabled
1:50:57 DLL DEBUG Acknowledgement_Timer: disabled
1:50:57 DLL DEBUG Activity_Timer: disabled
1:50:57 DLL DEBUG Link_Failure_Detection_Timer: disabled
9:12:59 DLL DEBUG In.Link_Establishment_Timeout
9:12:59 DLL DEBUG Out.Link_Request( 14, 1, 1)
9:12:59 T50 DEBUG TX Packet Packet( 22  16  2  1  14  1  1  16  3  138  9 )
9:12:59 DLL DEBUG Out.Link_Request return
9:12:59 DLL DEBUG ----------------------------------------
9:12:59 DLL DEBUG looping state=RESET_WAIT
9:12:59 DLL DEBUG Link_Establishment_Timer time 9:12:59
9:12:59 DLL DEBUG Retry_Timer: disabled
9:12:59 DLL DEBUG Acknowledgement_Timer: disabled
9:12:59 DLL DEBUG Activity_Timer: disabled
9:12:59 DLL DEBUG Link_Failure_Detection_Timer: disabled

The fact that the time decrements from 57 seconds to 56 seconds seems
weird in itself. It could be due to some obscure round of error in my
code to print the time, but I can't imagine where this would occur. In
all cases the current value of Clock is used, and it isn't stored
anywhere. Or it could be some sort of time synchronisation tool on the
computer, I am not aware of anything like this though.

During this wait, all evidence points to the fact that the
timer_enabled and expire_time variables are correct, they cannot be
changed from other tasks, and that it was waiting in the select
statement. During this time, the task appears to respond to other
select events fine. I haven't yet tested if the timeout starts working
again after entering the select again, as the structure of the code
doesn't make this easy.

What is going on? Strict real-time behaviour is not required, but 7
hours instead of 0.1 seconds is slightly on the extreme side.


Any ideas?
Thanks in advance.


PS. In hindsight, the "timer_enabled" variable may not be required, as
I can use the state variable instead and probably simplify some of the
code, but I am skeptical this is causing the problem.
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Jeffrey Carter]

Brian May wrote:

> What is going on? Strict real-time behaviour is not required, but 7
> hours instead of 0.1 seconds is slightly on the extreme side.

Is it possible that the task is handling other branches of the select 
and doesn't take the timeout branch during this time?

-- 
Jeff Carter
"I'm particularly glad that these lovely children were
here today to hear that speech. Not only was it authentic
frontier gibberish, it expressed a courage little seen
in this day and age."
Blazing Saddles
88

Re: timeouts

[Brian May]

>>>>> "Jeffrey" == Jeffrey Carter <spam@spam.com> writes:

    Jeffrey> Is it possible that the task is handling other branches
    Jeffrey> of the select and doesn't take the timeout branch during
    Jeffrey> this time?

I have logging statements for every possible branch, and nothing shows
up.

It could be a bug in the logging function too, I guess, but I can't
think of any reason why they would indefinitely hang (pretty straight
forward, no loops, etc). When it does start again, the data looks
valid, no obvious errors either. Then again, I probably should really
fix the logging function to log to disk, not just the screen...
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Steve]

What version of GNAT?
I vaguely recall a gnat bug having to do with time.  Unfortunately I can't
recall the particulars.  Maybe someone else on the list will remember.

Steve
(The Duck)


"Brian May" <bam@snoopy.apana.org.au> wrote in message
news:sa4smakuhzq.fsf@snoopy.apana.org.au...
> Hello,
>
> I have a written a communications protocols, for Windows, in Ada,
> using the GNAT compiler for Windows. This is my attempt at
> implementing the MAP27 protocol (used for talking to trunk radios).
>
> The main protocol is implemented as a separate task along the lines of
> the following code. This code is simplified from my actual code, and
> only shows the what I consider relevant to this bug, based on print
> messages. Any mistakes in syntax are probably copy errors.
>
> I should be able to provide full code on request, but need to confirm
> this first.
>
> task body State_Machine_Task is
>      timer_enabled : Boolean := True;
>      expire_time : Duration := clock + 0.1;
> ...
> begin
>    ...
>    Put(Log.Debug,"----------------------------------------");
>    Put(...);
>    Put(timer_enabled,expire_time);
>    Put(...);
>
>    while Continue loop
>        case SMT.DTE_State is
>        when ... =>
>             select
>                 accept ...
>                 ...
>             or
>                 ...
>             or
>                when timer_enabled =>
>                delay until expire_time;
>
>                print ("In.Link_Establishment_Timeout");
>
>                expire_time := clock + 0.1;
>             end select;
>
>        when ... =>
>             ...
>
>        ...
>
>        end case;
>    end loop;
> end;
>
>
> Generally speaking, the program does all this fine, and constantly
> prints the expired message, as required.
>
> However, occasionally something goes wrong, and while it prints the
> expiration time OK, it takes ages to print the "expired"
> message. e.g. one occasion the event was 7 hours late. This puzzles
> me, because every time the timer is incremented by 0.1 seconds, and my
> understanding is that the timer should trigger if the current time is
> greater then the expiration time.
>
> To be precise, at 1:50:57 am the timer was incremented, and the select
> reentered, and at 9:12:59 the timer expired. The actual log produced
> is below:
>
> 1:50:57 DLL DEBUG Activity_Timer: disabled
> 1:50:57 DLL DEBUG Link_Failure_Detection_Timer: disabled
> 1:50:56 DLL DEBUG In.Link_Establishment_Timeout
> 1:50:56 DLL DEBUG Out.Link_Request( 14, 1, 1)
> 1:50:56 T50 DEBUG TX Packet Packet( 22  16  2  1  14  1  1  16  3  138
 9 )
> 1:50:57 DLL DEBUG Out.Link_Request return
> 1:50:57 DLL DEBUG ----------------------------------------
> 1:50:57 DLL DEBUG looping state=RESET_WAIT
> 1:50:57 DLL DEBUG Link_Establishment_Timer time 1:50:57
> 1:50:57 DLL DEBUG Retry_Timer: disabled
> 1:50:57 DLL DEBUG Acknowledgement_Timer: disabled
> 1:50:57 DLL DEBUG Activity_Timer: disabled
> 1:50:57 DLL DEBUG Link_Failure_Detection_Timer: disabled
> 9:12:59 DLL DEBUG In.Link_Establishment_Timeout
> 9:12:59 DLL DEBUG Out.Link_Request( 14, 1, 1)
> 9:12:59 T50 DEBUG TX Packet Packet( 22  16  2  1  14  1  1  16  3  138
 9 )
> 9:12:59 DLL DEBUG Out.Link_Request return
> 9:12:59 DLL DEBUG ----------------------------------------
> 9:12:59 DLL DEBUG looping state=RESET_WAIT
> 9:12:59 DLL DEBUG Link_Establishment_Timer time 9:12:59
> 9:12:59 DLL DEBUG Retry_Timer: disabled
> 9:12:59 DLL DEBUG Acknowledgement_Timer: disabled
> 9:12:59 DLL DEBUG Activity_Timer: disabled
> 9:12:59 DLL DEBUG Link_Failure_Detection_Timer: disabled
>
> The fact that the time decrements from 57 seconds to 56 seconds seems
> weird in itself. It could be due to some obscure round of error in my
> code to print the time, but I can't imagine where this would occur. In
> all cases the current value of Clock is used, and it isn't stored
> anywhere. Or it could be some sort of time synchronisation tool on the
> computer, I am not aware of anything like this though.
>
> During this wait, all evidence points to the fact that the
> timer_enabled and expire_time variables are correct, they cannot be
> changed from other tasks, and that it was waiting in the select
> statement. During this time, the task appears to respond to other
> select events fine. I haven't yet tested if the timeout starts working
> again after entering the select again, as the structure of the code
> doesn't make this easy.
>
> What is going on? Strict real-time behaviour is not required, but 7
> hours instead of 0.1 seconds is slightly on the extreme side.
>
>
> Any ideas?
> Thanks in advance.
>
>
> PS. In hindsight, the "timer_enabled" variable may not be required, as
> I can use the state variable instead and probably simplify some of the
> code, but I am skeptical this is causing the problem.
> -- 
> Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Jeffrey Carter]

Brian May wrote:

> It could be a bug in the logging function too, I guess, but I can't
> think of any reason why they would indefinitely hang (pretty straight
> forward, no loops, etc). When it does start again, the data looks
> valid, no obvious errors either. Then again, I probably should really
> fix the logging function to log to disk, not just the screen...

The fact that the logged times decrease seems to indicate that the 
logging package is doing something funny.

-- 
Jeff Carter
"Sons of a silly person."
Monty Python & the Holy Grail
02

Re: timeouts

[Brian May]

>>>>> "Steve" == Steve  <nospam_steved94@comcast.net> writes:

    Steve> What version of GNAT?  I vaguely recall a gnat bug having
    Steve> to do with time.  Unfortunately I can't recall the
    Steve> particulars.  Maybe someone else on the list will remember.

GNAT 3.15p for Windows. I believe this is the latest version.
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Brian May]

>>>>> "Jeffrey" == Jeffrey Carter <spam@spam.com> writes:

    Jeffrey> The fact that the logged times decrease seems to indicate that the
    Jeffrey> logging package is doing something funny.

Nothing that I can see:

        function Strip(Value : in String) return String is
                I : Natural := Value'First;
                Continue : Boolean := True;
        begin
                while I <= Value'Last and Continue loop
                        if Value(I) = ' ' then
                                I := I + 1;
                        else
                                Continue := False;
                        end if;
                end loop;
                return Value(I..Value'Last);
        end Strip;

        function To_String(The_Time : in Time) return String is
                Duration : Integer;
                H : Integer range 0..23;
                M : Integer range 0..60;
                S : Integer range 0..60;
        begin
                Duration := Integer(Seconds(The_Time));

                S := Duration mod 60;
                Duration := (Duration-S)/60;

                M := Duration mod 60;
                Duration := (Duration-M)/60;

                H := Duration mod 24;

                return Strip(Integer'Image(H))&":"
                        &Strip(Integer'Image(M))&":"
                        &Strip(Integer'Image(S));
        end To_String;


        procedure Message(Module : in Module_Type;
                          Level : in Level_Type;
                          Text : in String) is
        begin
                if Display(Module,Level) then
                        Put_Line(To_String(Clock)&" "
                                &Module_Type'Image(Module)&" "
                                &Level_Type'Image(Level)&" "
                                &Text);
                end if;
        end Message;


Sure, the Duration := Integer(...) line may round the time up
(according to info I got in another thread), but I still fail to see
why a later log message should log an earlier time.
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Stephen Leake]

Brian May <bam@snoopy.apana.org.au> writes:

> Sure, the Duration := Integer(...) line may round the time up
> (according to info I got in another thread), but I still fail to see
> why a later log message should log an earlier time.

Are the log messages all output by one thread (a logging thread)? If
not, it would be easy for a low-priority thread to start a message,
get interrupted by a high-priority thread, and thus get messages that
appear to be out of time order.

-- 
-- Stephe

Re: timeouts

[Brian May]

>>>>> "Stephen" == Stephen Leake <stephen_leake@acm.org> writes:

    Stephen> Are the log messages all output by one thread (a logging
    Stephen> thread)? If not, it would be easy for a low-priority
    Stephen> thread to start a message, get interrupted by a
    Stephen> high-priority thread, and thus get messages that appear
    Stephen> to be out of time order.

No, in this case all log messages were output by one thread,
only. There are other threads running, but I turned off logging in
order to simplify debugging.

hmmm... I probably should work out a way to separate log entries by
thread though... I wonder what the easiest way is to do this...
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Jeff C,]

"Brian May" <bam@snoopy.apana.org.au> wrote in message 
news:sa4vffbreja.fsf@snoopy.apana.org.au...
>>>>>> "Steve" == Steve  <nospam_steved94@comcast.net> writes:
>
>    Steve> What version of GNAT?  I vaguely recall a gnat bug having
>    Steve> to do with time.  Unfortunately I can't recall the
>    Steve> particulars.  Maybe someone else on the list will remember.
>
> GNAT 3.15p for Windows. I believe this is the latest version.
> -- 
> Brian May <bam@snoopy.apana.org.au>

It is the latest public version of GNAT but not the latest version. If you
were an Ada Core Technologies customer they are up to version ~5.02

If you want to stay with public releases you might want to give gcc 3.4.1 a 
try.

There are pre-built binaries available for windows at the mingw site. Note 
that if you have
never used mingw before you should consider downloading not only the 
compiler but also the msys and
MinGW packages.

Of course this is a lot to download just to "see if it works" if you network 
connection is slow...

Re: timeouts

[Jeffrey Carter]

Brian May wrote:

> Nothing that I can see:
> 
>         function Strip(Value : in String) return String is
>                 I : Natural := Value'First;
>                 Continue : Boolean := True;
>         begin
>                 while I <= Value'Last and Continue loop
>                         if Value(I) = ' ' then
>                                 I := I + 1;
>                         else
>                                 Continue := False;
>                         end if;
>                 end loop;
>                 return Value(I..Value'Last);
>         end Strip;

Ada.Strings.Fixed.Trim?

>         function To_String(The_Time : in Time) return String is
>                 Duration : Integer;
>                 H : Integer range 0..23;
>                 M : Integer range 0..60;
>                 S : Integer range 0..60;
>         begin
>                 Duration := Integer(Seconds(The_Time));
> 
>                 S := Duration mod 60;
>                 Duration := (Duration-S)/60;
> 
>                 M := Duration mod 60;
>                 Duration := (Duration-M)/60;
> 
>                 H := Duration mod 24;
> 
>                 return Strip(Integer'Image(H))&":"
>                         &Strip(Integer'Image(M))&":"
>                         &Strip(Integer'Image(S));

This can give things like "7:16:3", which I consider ugly.

PragmARC.Images.Image lets you say

Image (H, Width => 2, Zero_Filled => True);

which can produce prettier time images.

PragmARC.Date_Handler uses this internal procedure to split the seconds 
value from Ada.Calendar into hour, minute, and seconds:

procedure Split (Seconds : in out Calendar.Day_Duration;
                  Hour    :    out Hour_Number;
                  Minute  :    out Minute_Number)
is
    Seconds_Per_Minute : constant := 60;
    Minutes_Per_Hour   : constant := 60;
    Seconds_Per_Hour   : constant := Minutes_Per_Hour *
                                     Seconds_Per_Minute;
begin -- Split
    if Seconds >= Calendar.Day_Duration'Last then
       Seconds := 0.0;
       Hour    := 0;
       Minute  := 0;

       return;
    end if;

    Hour := Integer'Max (Integer (Seconds / Seconds_Per_Hour - 0.5),
                         Hour_Number'First);
    Seconds := Seconds - Calendar.Day_Duration (Hour) * Seconds_Per_Hour;
    Minute := Integer'Max (Integer (Seconds / Seconds_Per_Minute - 0.5),
                           Minute_Number'First);
    Seconds := Seconds - Calendar.Day_Duration (Minute) *
                         Seconds_Per_Minute;
end Split;

where

subtype Hour_Number   is Integer range 0 .. 23;
subtype Minute_Number is Integer range 0 .. 59;

FWIW.

>         end To_String;

-- 
Jeff Carter
"Now go away or I shall taunt you a second time."
Monty Python & the Holy Grail
07

Re: timeouts

[Brian May]

>>>>> "Jeff" == Jeff C, <jcreem@yahoo.com> writes:

    Jeff> It is the latest public version of GNAT but not the latest
    Jeff> version. If you were an Ada Core Technologies customer they
    Jeff> are up to version ~5.02

    Jeff> If you want to stay with public releases you might want to
    Jeff> give gcc 3.4.1 a try.

    Jeff> There are pre-built binaries available for windows at the
    Jeff> mingw site. Note that if you have never used mingw before
    Jeff> you should consider downloading not only the compiler but
    Jeff> also the msys and MinGW packages.

As I am using cygwin, I tried the latest cygwin mingw gcc ada
compiler. 3.3.3-3

Unfortunately, my initial attempt has failed with an undefined symbol:
_max_path_len when attempting to compile AWS (required by my
application).

Is there anything else I can try? It would kind of look bad for Ada if
I had to rewrite the mostly working code in another language because
of suspected compiler bugs.

Also, for the record, I used a better routine to display the time,
there were no glitches, but it still hangs. I suspect it is related to
the number of times the select statement is entered, it seems to take
many hours before it will crash (eg. greater then 12 hours with the
select statement being entered 2 to 3 times a second). When it does
crash, everything else in the application still works fine (including
AWS server and other events in the same select statement), but this
doesn't help much without the timeouts.

    Jeff> Of course this is a lot to download just to "see if it
    Jeff> works" if you network connection is slow...


Ok, my 2 cents on the thread on why Ada is not popular: No freely
available compiler that is reliable, with known bugs fixed, and can
compile available code.

(I am basing this statement on the following assumption: there is a
bug related to time handling, it is present in GNAT-3.15p, and it is
the bug I am encountering).
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Pascal Obry]

Brian May <bam@snoopy.apana.org.au> writes:

> As I am using cygwin, I tried the latest cygwin mingw gcc ada
> compiler. 3.3.3-3
> 
> Unfortunately, my initial attempt has failed with an undefined symbol:
> _max_path_len when attempting to compile AWS (required by my
> application).
> 
> Is there anything else I can try? 

Yes using the MingW compiler and not the one provided with Cygwin.

> It would kind of look bad for Ada if
> I had to rewrite the mostly working code in another language because
> of suspected compiler bugs.

Well, the GNAT Cygwin port is recent and does not support tasking AFAIK. The
MingW compiler should be more stable. If this is not the case why not use GNAT
3.15p which is (for a long time now) working fine for many projects.

> Ok, my 2 cents on the thread on why Ada is not popular: No freely
> available compiler that is reliable, with known bugs fixed, and can
> compile available code.

That's just not true. GNAT 3.15p is certainly stable. On UNIX platforms the
GNAT compiler which comes with GCC 3.4 is working fine AFAIK. And the MingW
(Windows) port of this compiler should be in good shape.

Pascal.

-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|              http://www.obry.org
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595

Re: timeouts

[Georg Bauhaus]

Pascal Obry <pascal@obry.org> wrote:
 
:> Ok, my 2 cents on the thread on why Ada is not popular: No freely
:> available compiler that is reliable, with known bugs fixed, and can
:> compile available code.
: 
: That's just not true. GNAT 3.15p is certainly stable. On UNIX platforms the
: GNAT compiler which comes with GCC 3.4 is working fine AFAIK. And the MingW
: (Windows) port of this compiler should be in good shape.
 
Is the fact that GCC 3.4.1 runs the ACATS withouth a single
failure an indication of a compiler that you can not rely on?
(BTW, GCC 3.3.3's Ada part is not among users' favorites, afaikt.)

Otherwise, do producers of compilers for "non-Ada" languages
manage to convey the impression that their compilers don't
have bugs? I think that C++ compilers, or Eiffel compilers, or ...,
are praised to support almost all of the respective language
and libraries. Are there different expectations of an Ada
compiler?


-- Georg

Re: timeouts

[Jean-Marc Bourguet]

Georg Bauhaus <sb463ba@l1-hrz.uni-duisburg.de> writes:

> Otherwise, do producers of compilers for "non-Ada" languages
> manage to convey the impression that their compilers don't
> have bugs? 

As a user of compilers for other languages: no.

> I think that C++ compilers, or Eiffel compilers, or ..., are praised
> to support almost all of the respective language and libraries.

I can't write about Eiffel but C++ compilers tend to support different
variants of subset of standard C++.  And there is only one C++
compiler which claims support for the complete standard, which is
dated 98.  All others have no supported features.

Yours,

-- 
Jean-Marc

Re: timeouts

[Stephen Leake]

Brian May <bam@snoopy.apana.org.au> writes:

> It would kind of look bad for Ada if I had to rewrite the mostly
> working code in another language because of suspected compiler bugs.

Hmm. What other compiler (for any language) do you feel has no bugs?

Personally, I don't trust _any_ compiler if I don't have a support
contract for it.

> Ok, my 2 cents on the thread on why Ada is not popular: No freely
> available compiler that is reliable, with known bugs fixed, and can
> compile available code.

Again, what other compiler meets this criteria? GCC C, maybe. _not_
GCC C++; I have lots of code that won't compile. But C is not a very
modern language, and I'll take GNAT 3.15p over the latest GCC C
compiler any day.

-- 
-- Stephe

Re: timeouts

[Jano]

Steve wrote:
> What version of GNAT?
> I vaguely recall a gnat bug having to do with time.  Unfortunately I can't
> recall the particulars.  Maybe someone else on the list will remember.

I was bitten by it. It involves Gnat 3.15p on Windows. Delays can 
mis-delay for unknown periods of time, effectively suggesting that tasks 
are locked when they are not.

I'm not sure if it is needed to use Ada.Real_Time mixed with 
Ada.Calendar for it to trigger... in any case, if the OP is using this 
platform, he should patch it just in case anyway.

And I concur with some other poster: is too bad that the latest public 
release of gnat for windows carries two or three traps like this not 
mentioned in the users guide for NT. These are long-time known and fixed 
bugs, at least a link in the download page to some bugs page would be of 
interest (that's to say, if nobody at ACT is interested in or have the 
time to re-package 3.15p or make a new public release).

Re: timeouts

[Steve]

"Brian May" <bam@snoopy.apana.org.au> wrote in message
news:sa4n00iit7g.fsf@snoopy.apana.org.au...
[snip]> Ok, my 2 cents on the thread on why Ada is not popular: No freely
> available compiler that is reliable, with known bugs fixed, and can
> compile available code.
>

Gee, I've never met ANY compiler (free or otherwise) with all known bugs
fixed.
... but then again I've only been programming professionally for 20 years.

Hmmm... Maybe if they re-implemented GNAT in SPARK ;-)

Steve
(The Duck)

> (I am basing this statement on the following assumption: there is a
> bug related to time handling, it is present in GNAT-3.15p, and it is
> the bug I am encountering).
> -- 
> Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Georg Bauhaus]

Steve <nospam_steved94@comcast.net> wrote:
: 
: Hmmm... Maybe if they re-implemented GNAT in SPARK ;-)

Will that produce an Ada compiler with a number of capacity limits?

-- Georg

Re: timeouts

[Randy Brukardt]

"Jano" <notelacreas@porfavor.no> wrote in message
news:2p63roFgloq0U1@uni-berlin.de...
> Steve wrote:
> > What version of GNAT?
> > I vaguely recall a gnat bug having to do with time.  Unfortunately I
can't
> > recall the particulars.  Maybe someone else on the list will remember.
>
> I was bitten by it. It involves Gnat 3.15p on Windows. Delays can
> mis-delay for unknown periods of time, effectively suggesting that tasks
> are locked when they are not.

The problem I recall (it happened in Janus/Ada, too, because it's actually
caused by a patch in the OS for a hardware problem) is that
QueryPerformanceCounter leaps forward by large amounts. Depending on how
Ada.Calendar is written, that can have bizarre effects. I believe that Tom
Moran created a patch for GNAT's Ada.Calendar for that; I don't know if
3.15p has it, but if not, you should try applying it. (Even better is
getting a machine without the faulty chipset, but that's not always
practical!)

                            Randy.

Re: timeouts

[tmoran]

>... QueryPerformanceCounter leaps forward by large amounts. Depending on how
>Ada.Calendar is written, that can have bizarre effects. I believe that Tom
>Moran created a patch for GNAT's Ada.Calendar for that; ...

See the comp.lang.ada thread containing

> Subject: Re: Problems with a TIMER
>
> Date: 2003-01-28 10:42:28 PST
>
> > The target is a processor x86 Family 6 Model 7 Stepping 3 AT/AT COMPATIBLE
> > The results change if I use video-outputs or not (PUT("START TIMER"),
> > PUT("-"), PUT("TIME OUT") are now commented into the code).
> > Why?
>   In what way do the results change?  What compiler, OS, and motherboard
> chip set do you have - see MS Knowledgebase article Q274323.
>   There was a problem with certain chipsets and MS Windows that caused
> the machine clock to appear to jump forward 2**24 ticks (several seconds)
> if you did multiple clock reads with less than several microseconds
> between them.  Gnat 3.15 fixed that, but introduced a new clock error,
> which I reported and they say they've fixed for future versions.  Janus
> has a version with the fix, but I don't know about other compilers.

Re: timeouts

[Brian May]

>>>>> "Pascal" == Pascal Obry <pascal@obry.org> writes:

    Pascal> Yes using the MingW compiler and not the one provided with
    Pascal> Cygwin.

cygwin calls their compiler mingw, so I would have assumed that they
are the same. Is this assumption incorrect?

    Pascal> Well, the GNAT Cygwin port is recent and does not support
    Pascal> tasking AFAIK. The MingW compiler should be more
    Pascal> stable. If this is not the case why not use GNAT 3.15p
    Pascal> which is (for a long time now) working fine for many
    Pascal> projects.

Are we going around in circles here? It is Gnat 3.15p that I am
currently using and relying on, and this is the compiler which
(according to others) has known bugs in timer code under Windows
(unfortunately I can't use Unix/Linux, but that would be my ideal
solution).

Sorry if I misunderstood you.
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Brian May]

>>>>> "Stephen" == Stephen Leake <stephen_leake@acm.org> writes:

    Stephen> Hmm. What other compiler (for any language) do you feel
    Stephen> has no bugs?

If I report a bug in the GCC C compiler, for example, then I can
access the fix as soon as it is applied to CVS (if I really want
it). There is also a publicly available list of bugs, so I can tell if
it really is a compiler bug or a bug in my code.

With GNAT, I do not get the fix when it is developed, but have to wait
until it is fixed in the free version.

According to another poster, this problem was known January 2003, that
is over one and a half years ago.

    Stephen> Personally, I don't trust _any_ compiler if I don't have
    Stephen> a support contract for it.

This might work for you, and it might work very well. It doesn't work
for everyone.

My understanding is that the support contracts are aimed at large
projects by large companies. If you are a small company, developing
software tools that don't contribute directly to company profits, then
a support contract may not be an option.

Even if I am wrong here, then a support contract is not really an
option when exclusively developing open source software.

Not that I have a problem with the business model that if you want the
newest features you have to pay for them, but I think an exception
needs to be made for bugs that cause valid code to fail in mysterious
ways.

If you want Ada to become popular, then it is necessarily for bug
fixes to be available to everyone too, including open source software
developers and companies that can't/won't pay for a support
contract. Otherwise that will just become yet another excuse for not
adopting Ada.

    Stephen> Again, what other compiler meets this criteria? GCC C,
    Stephen> maybe. _not_ GCC C++; I have lots of code that won't
    Stephen> compile. But C is not a very modern language, and I'll
    Stephen> take GNAT 3.15p over the latest GCC C compiler any day.

Also: With C or C++ you don't rely on the compiler so much to provide
high level objects. If, for instance, the package you relied on to
provide timers fails you can switch to another library.

In my case the solutions I have seen don't seem feasible:

* use Linux.

* purchase support contract. I have to convince the company that Ada
  is going to be more reliable first. I am not off to a good
  start. This isn't a major project that will generate heaps of
  income, rather its an expensive project (due to poor language choice
  by people who didn't understand its limitations) that everyone would
  prefer to forget about.

  It is very possible that I may be able to make this open source
  software too, so others can use it.

* use mingw compiler - I used that GNAT 3.14p compiler because it was
  my understanding it would be more reliable - has this changed now?

* use external library for timer stuff. Involves rewriting it.

* use another language. Involves rewriting it.
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Brian May]

>>>>> "Jano" == Jano  <notelacreas@porfavor.no> writes:

    Jano> And I concur with some other poster: is too bad that the
    Jano> latest public release of gnat for windows carries two or
    Jano> three traps like this not mentioned in the users guide for
    Jano> NT. These are long-time known and fixed bugs, at least a
    Jano> link in the download page to some bugs page would be of
    Jano> interest (that's to say, if nobody at ACT is interested in
    Jano> or have the time to re-package 3.15p or make a new public
    Jano> release).

If I had known about the bugs before hand, I would have taken some
other approach to avoid the limitations or waited until the bug is
fixed before porting the code over to Ada.

Even if I developed the code, if the bugs were documented somewhere I
could find, then I can verify it was a compiler bug and not a bug in
my code. Normally, suspected compiler bugs are really hidden bugs in
my code... As it is, I couldn't verify this until raising the issue on
this newsgroup, and even here, I had to wait for firm verification
(not that I am complaining).

What other known traps exist?
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Brian May]

>>>>> "tmoran" == tmoran  <tmoran@acm.org> writes:

    >> Subject: Re: Problems with a TIMER
    >> 
    >> Date: 2003-01-28 10:42:28 PST

Unfortunately that post seems to have expired ages ago from my news
server, but thanks anyway for the reference.

    >> between them.  Gnat 3.15 fixed that, but introduced a new clock error,
    >> which I reported and they say they've fixed for future versions.  Janus
    >> has a version with the fix, but I don't know about other compilers.

I am guessing this is the problem I have encountered.
-- 
Brian May <bam@snoopy.apana.org.au>

SPARK

[Brian May]

>>>>> "Georg" == Georg Bauhaus <sb463ba@l1-hrz.uni-duisburg.de> writes:

    Georg> Steve <nospam_steved94@comcast.net> wrote:
    Georg> : Hmmm... Maybe if they re-implemented GNAT in SPARK ;-)

    Georg> Will that produce an Ada compiler with a number of capacity limits?

Dare I ask, what is SPARK?

I gather it is some tool to make Ada programs even more reliable?
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Brian May]

>>>>> "Jeff" == Jeff C, <jcreem@yahoo.com> writes:

    Jeff> There are pre-built binaries available for windows at the
    Jeff> mingw site. Note that if you have never used mingw before
    Jeff> you should consider downloading not only the compiler but
    Jeff> also the msys and MinGW packages.

Can I just verify:

I download from the following site:

<URL:http://sourceforge.net/project/showfiles.php?group_id=2435>

There seem to be a large number of files, and I don't know what files
I need.

I assume I need the following files:

MSYS-1.0.10.exe
MinGW-3.1.0-1.exe
w32api-2.5.tar.gz

What files do I need for the compiler?

Do I need to remove GNAT 3.15p before installing these?
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Björn Persson]

Brian May wrote:

>>>>>>"tmoran" == tmoran  <tmoran@acm.org> writes:
> 
>     >> Subject: Re: Problems with a TIMER
>     >> 
>     >> Date: 2003-01-28 10:42:28 PST
> 
> Unfortunately that post seems to have expired ages ago from my news
> server, but thanks anyway for the reference.

It's archived at Google:

http://www.google.se/groups?lr=&ie=UTF-8&th=6b08c4709e045cb4&seekm=maAZ9.68865%24rM2.42454%40rwcrnsc53&frame=off

-- 
Björn Persson                              PGP key A88682FD
                    omb jor ers @sv ge.
                    r o.b n.p son eri nu

Re: timeouts

[Stephen Leake]

Brian May <bam@snoopy.apana.org.au> writes:

> With GNAT, I do not get the fix when it is developed, but have to wait
> until it is fixed in the free version.

This is changing, as GNAT is integrated into the gcc releases.

> If you want Ada to become popular, then it is necessarily for bug
> fixes to be available to everyone too, including open source software
> developers and companies that can't/won't pay for a support
> contract. Otherwise that will just become yet another excuse for not
> adopting Ada.

I don't really care if Ada is "popular". People should use the tools
they think are appropriate. I only care that Ada is available; I'm
comfortable that the current market will support the current vendors
for a long time.

If people choose not to use a language because the free compilers
aren't good enough for them, that's ok by me.

>     Stephen> Again, what other compiler meets this criteria? GCC C,
>     Stephen> maybe. _not_ GCC C++; I have lots of code that won't
>     Stephen> compile. But C is not a very modern language, and I'll
>     Stephen> take GNAT 3.15p over the latest GCC C compiler any day.
> 
> Also: With C or C++ you don't rely on the compiler so much to provide
> high level objects. If, for instance, the package you relied on to
> provide timers fails you can switch to another library.

The problem you encountered is a bug in a particular Intel chip, for a
particular version of Windows. That has nothing to do with the
language or library you are using.

> In my case the solutions I have seen don't seem feasible:
> 
> * use Linux.
> 
> * purchase support contract. I have to convince the company that Ada
>   is going to be more reliable first. I am not off to a good
>   start. This isn't a major project that will generate heaps of
>   income, rather its an expensive project (due to poor language choice
>   by people who didn't understand its limitations) that everyone would
>   prefer to forget about.
> 
>   It is very possible that I may be able to make this open source
>   software too, so others can use it.
> 
> * use mingw compiler - I used that GNAT 3.14p compiler because it was
>   my understanding it would be more reliable - has this changed now?

Yes.

> * use external library for timer stuff. Involves rewriting it.
> 
> 
> * use another language. Involves rewriting it. 

You've also been offered a patch, which is what you were looking for
in the first place.

-- 
-- Stephe

Re: timeouts

[tmoran]

>In my case the solutions I have seen don't seem feasible:

Comparing my version of s-osprim.adb and the one from ACT, I note the
addition of one (initialization) line:

Comparing files S-OSPRIM.ADB and L:S-OSPRIM.ADB
***** S-OSPRIM.ADB
         Long_Long_Float (Sec_Unit));
      Base_Monotonic_Clock := Base_Clock;
   end Get_Base_Time;
***** L:S-OSPRIM.ADB
         Long_Long_Float (Sec_Unit));
   end Get_Base_Time;
*****

***** S-OSPRIM.ADB

Of course you'll then need to compile s-osprim.adb with the compiler
option that lets to recompile system components (which I don't recall
off the top of my head) and you'll have to recompile the things that
depend on s-osprim.adb (IIRC that's more than you would expect).

Is the current GCC Gnat more robust than 3.15p, or is it still beta?
ie, should we (Windows) 3.15p users switch, or continue waiting?

Re: timeouts

[Brian May]

>>>>> "tmoran" == tmoran  <tmoran@acm.org> writes:

    tmoran> Is the current GCC Gnat more robust than 3.15p, or is it
    tmoran> still beta?  ie, should we (Windows) 3.15p users switch,
    tmoran> or continue waiting?

I get the distinct impression that it is now time to switch...

PS. Thanks to everyone who has so far attempted to help me with this
issue.
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Jano]

Randy Brukardt wrote:
 > Jano wrote:
>>I was bitten by it. It involves Gnat 3.15p on Windows. Delays can
>>mis-delay for unknown periods of time, effectively suggesting that tasks
>>are locked when they are not.
> 
> 
> The problem I recall (it happened in Janus/Ada, too, because it's actually
> caused by a patch in the OS for a hardware problem) is that
> QueryPerformanceCounter leaps forward by large amounts. Depending on how
> Ada.Calendar is written, that can have bizarre effects. I believe that Tom
> Moran created a patch for GNAT's Ada.Calendar for that; I don't know if
> 3.15p has it, but if not, you should try applying it. (Even better is
> getting a machine without the faulty chipset, but that's not always
> practical!)

This one is a different problem, as someone as already pointed. It 
involved certain chipsets/motherboards only.

Re: timeouts

[Jano]

Brian May wrote:
>>>>>>"Jano" == Jano  <notelacreas@porfavor.no> writes:
> 
> 
>     Jano> And I concur with some other poster: is too bad that the
>     Jano> latest public release of gnat for windows carries two or
>     Jano> three traps like this not mentioned in the users guide for
>     Jano> NT. These are long-time known and fixed bugs, at least a
>     Jano> link in the download page to some bugs page would be of
>     Jano> interest (that's to say, if nobody at ACT is interested in
>     Jano> or have the time to re-package 3.15p or make a new public
>     Jano> release).

> What other known traps exist?

Not as bad as this one, but:

* The select call in the Gnat.Sockets package has a bug and isn't 
reliable. Each call to Gnat.Sockets.Stream allocates memory that you 
should free (Undocumented).

* Not exactly a bug, but the priorities in System.Priority are more than 
the ones that windows offers. They're transparently mapped and *merged* 
which can give unexpected results. This is explained in the system.ads 
file but not in the users guide. This one is specially frustrating when 
you're taught the amazing Ada tasking capabilities, try to experiment in 
the free Gnat compiler, read in the users guide that it has strict Annex 
D compliance and then you start to get funny results.

BTW I have ready the patch (I use it rutinely in my windows programs) 
you need for the delay matter. Mail me to public .at. mosteo dot com if 
you're interested in it. I prefer to include it in my sources that 
recompile the Gnat runtime, so any person compiling them doesn't need to 
worry about patching his Gnat.

I want to clarify that I have not any grudge against ACT. I simply find 
disturbing that a pointer to these known issues isn't present in the 
users guide (which is what you're repeatedly told to read when you are a 
novice asking novice questions). I've lost some time over these issues 
and that's the reason that when someone faces them I quickly respond. 
Not resentment or something like that. I really love to have Gnat 
available for free.

Kind regards,

A. Mosteo.

Re: SPARK

[Georg Bauhaus]

Brian May <bam@snoopy.apana.org.au> wrote:
:>>>>> "Georg" == Georg Bauhaus <sb463ba@l1-hrz.uni-duisburg.de> writes:
: 
:    Georg> Steve <nospam_steved94@comcast.net> wrote:
:    Georg> : Hmmm... Maybe if they re-implemented GNAT in SPARK ;-)
: 
:    Georg> Will that produce an Ada compiler with a number of capacity limits?
: 
: Dare I ask, what is SPARK?
: 
: I gather it is some tool to make Ada programs even more reliable?

http://www.sparkada.com/


-- Georg

Re: timeouts

[Georg Bauhaus]

Brian May <bam@snoopy.apana.org.au> wrote:
: 
: What files do I need for the compiler?

If you start here,
http://www.mingw.org/download.shtml

you can see a list of gcc-3.4.1* candidate release archives.
Combine the gcc*3.4.1-* archives you want, after reading
gcc-3.4.1-release_notes.txt, which explains why there is
more than one part.

-- Georg

Re: timeouts

[Brian May]

>>>>> "Jeffrey" == Jeffrey Carter <spam@spam.com> writes:

    Jeffrey> PragmARC.Date_Handler uses this internal procedure to split the
    Jeffrey> seconds value from Ada.Calendar into hour, minute, and seconds:

I found PragmARC.Date_Handler the Image function, and am now using it.

For some weird reason, when I compile my program with the latest
mingw32 GNAT compiler, it constantly prints "N = 1" on a separate line
on its own whenever I call the Image function. If I remove the call to
the Image function, the N = 1 goes away. Sometimes I get two, most of
the time I only get one. Any ideas why? This didn't happen with Gnat
3.15p. Not a show stopper, it just irks me that I can't explain this
difference in behaviour. Will continue investigating.

Also with GNAT 3.15 this would work, but it come up with a compiler
error on mingw32:

with Types;
use Types;
use type Byte;

I had to change it to

with Types;
use Types;
use type Types.Byte;

Strange. Not sure which behaviour is correct.

Anyway, I am now running my program compiled with mingw32 and will see
it if still crashes...

When installing mingw32, I found I had to keep GNAT 3.15p installed,
so I can keep with win32ada bindings installed. They appear to work
fine with mingw32. Is there anyway I can install the win32ada bindings
without GNAT 3.15p?

Thanks.
-- 
Brian May <bam@snoopy.apana.org.au>

Cygwin and gcc-ada 3.4.1 (was Re: timeouts)

[Jano]

I have a doubt after all this talk about the convenience of migrating to 
3.4.1:

* I see the Mingw is in candidate status (may be good enough).

* If I'd choose to use the cygwin one, would the executables produced 
require the cygwin1.dll? (I suppose so, this is my doubt).

Would you say that is definitely preferable to use 3.4.1 over a patched 
3.15p?

Thanks in advance,

A. Mosteo.

Re: timeouts

[Jeffrey Carter]

Brian May wrote:

> I found PragmARC.Date_Handler the Image function, and am now using it.
> 
> For some weird reason, when I compile my program with the latest
> mingw32 GNAT compiler, it constantly prints "N = 1" on a separate line
> on its own whenever I call the Image function. If I remove the call to
> the Image function, the N = 1 goes away. Sometimes I get two, most of
> the time I only get one. Any ideas why? This didn't happen with Gnat
> 3.15p. Not a show stopper, it just irks me that I can't explain this
> difference in behaviour. Will continue investigating.

The only things I can think of are:

1. There's some debugging outputs in the mingw32 version of the compiler

2. You've modified the PragmARCs to include this output

Since I presume you'd remember if you'd done 2., that leaves 1. as the 
only thing I can think of.

> Also with GNAT 3.15 this would work, but it come up with a compiler
> error on mingw32:
> 
> with Types;
> use Types;
> use type Byte;
> 
> I had to change it to
> 
> with Types;
> use Types;
> use type Types.Byte;
> 
> Strange. Not sure which behaviour is correct.

This is an error in GNAT 3.15p. The visibility of "use" should not take 
effect in the context clauses, but GNAT 3.15p applies it there. The 2nd 
version is correct.

-- 
Jeff Carter
"Have you gone berserk? Can't you see that that man is a ni?"
Blazing Saddles
38

Re: timeouts

[Pascal Obry]

Brian May <bam@snoopy.apana.org.au> writes:

> >>>>> "Pascal" == Pascal Obry <pascal@obry.org> writes:
> 
>     Pascal> Yes using the MingW compiler and not the one provided with
>     Pascal> Cygwin.
> 
> cygwin calls their compiler mingw, so I would have assumed that they
> are the same. Is this assumption incorrect?

Yes, it is incorrect. Try using the compiler here: http://www.mingw.org/

Pascal.

-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|              http://www.obry.org
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595

Re: timeouts

[Stephen Leake]

Brian May <bam@snoopy.apana.org.au> writes:

> >>>>> "Jeffrey" == Jeffrey Carter <spam@spam.com> writes:
> 
>     Jeffrey> PragmARC.Date_Handler uses this internal procedure to split the
>     Jeffrey> seconds value from Ada.Calendar into hour, minute, and seconds:
> 
> I found PragmARC.Date_Handler the Image function, and am now using it.
> 
> For some weird reason, when I compile my program with the latest
> mingw32 GNAT compiler, it constantly prints "N = 1" on a separate line
> on its own whenever I call the Image function. If I remove the call to
> the Image function, the N = 1 goes away. Sometimes I get two, most of
> the time I only get one. Any ideas why? This didn't happen with Gnat
> 3.15p. Not a show stopper, it just irks me that I can't explain this
> difference in behaviour. Will continue investigating.

I had a similar problem, and tracked it down to a "pragma Debug" in
the GNAT sources for Ada.Text_IO. Try compiling without -gnata. Mine
went away with the next release of GNAT (5.02a1).

> Also with GNAT 3.15 this would work, but it come up with a compiler
> error on mingw32:
> 
> with Types;
> use Types;
> use type Byte;
> 
> I had to change it to
> 
> with Types;
> use Types;
> use type Types.Byte;
> 
> Strange. Not sure which behaviour is correct.

The Annotated Language Reference Manual 8.4 (6) has a note that says
"The scope does not include context_clauses themselves". So 'byte' is
_not_ supposed to be visible before the start of the package
declaration; the second version is correct. This would also work:

with Types;
use Types;
package Foo is
   use type Byte;
...
end package Foo;

> Anyway, I am now running my program compiled with mingw32 and will
> see it if still crashes...
> 
> When installing mingw32, I found I had to keep GNAT 3.15p installed,
> so I can keep with win32ada bindings installed. They appear to work
> fine with mingw32. Is there anyway I can install the win32ada bindings
> without GNAT 3.15p?

That used to be possible in earlier versions of GNAT. But the
installer has gotten simpler, I suspect because GNAT customer base is
getting less sophisticated as it gets bigger :). 

You can just copy the Win32Ada binding directories, then uninstall
GNAT 3.15p. Or just keep 3.15p installed, but not in you path. That
way you can test the two compilers against each other.

-- 
-- Stephe

Re: timeouts

[Brian May]

>>>>> "Stephen" == Stephen Leake <stephen_leake@acm.org> writes:

    Stephen> I had a similar problem, and tracked it down to a "pragma
    Stephen> Debug" in the GNAT sources for Ada.Text_IO. Try compiling
    Stephen> without -gnata. Mine went away with the next release of
    Stephen> GNAT (5.02a1).

Hmmm... Interesting... That is probably my problem. Yes, I am
compiling with -gnata, too.

When it annoys me enough I will try removing the -gnata. So far, I
haven't reached this threshold.

Anyway, to followup on my original problem:

With gnat 3.15p, after approx 12 hours, my timeouts stopped working
and/or took excessively long (e.g. in the order of hours instead of
0.1 of a second).

With mingw32 3.4.1, candidate release, after 12 hours, timeouts were
still working. Unfortunately, instead of 0.1 seconds, each one was 4.6
seconds. This is on a XP computer with no other applications
running[1]. While this is OK for my application, I am concerned that
there is still something wrong...

If I restart the application, it comes good.

I have another theory, it could be a problem with my logging code
(weird theory, I know) that prints the date & time. In order to rule
this out, I am now using Ada.Text_IO.Put_Line directly without
printing the date and time immediately before the select statement,
and at the start of each event, and this should enable to be prove
that the delay really is in the select statement.

Note:

[1] Interestingly, task manager reported 50% CPU used by the msys
terminal.  After I restarted the process the CPU usage dropped to less
then 1%. To me, this makes absolutely no sense, as surely more CPU
would be required to update the screen when it is getting updated
several times a second, not when there was a 4.6 second delay?
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[tmoran]

>still working. Unfortunately, instead of 0.1 seconds, each one was 4.6
>seconds. This is on a XP computer with no other applications

4.6 or 4.686967565160 = 2**24/(3*1_193_182) ?

Re: timeouts

[Brian May]

>>>>> "tmoran" == tmoran  <tmoran@acm.org> writes:

    >> still working. Unfortunately, instead of 0.1 seconds, each one was 4.6
    >> seconds. This is on a XP computer with no other applications

    tmoran> 4.6 or 4.686967565160 = 2**24/(3*1_193_182) ?

According to the time displayed, at least when I looked this morning,
it was 4.60, accurate to two decimal places.

Sorry if I am thick, but what significance does 2**24/(3*1_193_182)
hold?
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Stephen Leake]

Brian May <bam@snoopy.apana.org.au> writes:

> >>>>> "Stephen" == Stephen Leake <stephen_leake@acm.org> writes:
> 
>     Stephen> I had a similar problem, and tracked it down to a "pragma
>     Stephen> Debug" in the GNAT sources for Ada.Text_IO. Try compiling
>     Stephen> without -gnata. Mine went away with the next release of
>     Stephen> GNAT (5.02a1).
> 
> Hmmm... Interesting... That is probably my problem. Yes, I am
> compiling with -gnata, too.

The 'pragma Debug' was in one of the generic packages, so it gets
compiled when you instantiate it. Hmm. I just grep'ed in 

GNAT-3.15p/lib/gcc-lib/pentium-mingw32msv/2.8.1/adainclude/

for "pragma Debug", and found 40 hits. But the are all in the tasking
packages. Have you applied any patches?

> <delete summary of Win32 issues>

I realize this isn't going to help you, but this is an example of why
Windows is known as neither reliable nor real-time.

-- 
-- Stephe

Re: timeouts

[tmoran]

>Sorry if I am thick, but what significance does 2**24/(3*1_193_182) hold?
  It isn't obvious? ;)
The original IBM PC had a timer running at 1.193182 MHz (they used cheap
timers built for TV sets).  These days PC descendants often use a small
multiple of that rate, eg, 3*1193182 ticks/sec, so 2**24 ticks takes
4.686968 seconds.  The chipset problem had to do with a 24 bit overflow,
and 4.6 seemed suspiciously close.  Of course the chipset problem ought to
have been fixed in any reasonably new hardware, so that may be a red herring...

Re: timeouts

[Brian May]

>>>>> "Stephen" == Stephen Leake <stephen_leake@acm.org> writes:

    Stephen> The 'pragma Debug' was in one of the generic packages, so
    Stephen> it gets compiled when you instantiate it. Hmm. I just
    Stephen> grep'ed in

    Stephen> GNAT-3.15p/lib/gcc-lib/pentium-mingw32msv/2.8.1/adainclude/

    Stephen> for "pragma Debug", and found 40 hits. But the are all in
    Stephen> the tasking packages. Have you applied any patches?

Strange. No I haven't applied any patches. However, this was mingw32
3.4.x, what you checked would appear to be GNAT 3.15p? Or am I
mistaken?

    Stephen> I realize this isn't going to help you, but this is an
    Stephen> example of why Windows is known as neither reliable nor
    Stephen> real-time.

Yes, no doubt Linux would solve all of these problems, and more...
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Brian May]

>>>>> "tmoran" == tmoran  <tmoran@acm.org> writes:

    tmoran> It isn't obvious? ;)

    tmoran> The original IBM PC had a timer running at 1.193182 MHz
    tmoran> (they used cheap timers built for TV sets).  These days PC
    tmoran> descendants often use a small multiple of that rate, eg,
    tmoran> 3*1193182 ticks/sec, so 2**24 ticks takes 4.686968
    tmoran> seconds.  The chipset problem had to do with a 24 bit
    tmoran> overflow, and 4.6 seemed suspiciously close.  Of course
    tmoran> the chipset problem ought to have been fixed in any
    tmoran> reasonably new hardware, so that may be a red herring...

Good theory.  Unfortunately, right now, on the same computer, it is
every 2.1 seconds.

In fact, it seems slow down the longer it is run. Need to verify this
theory.

Doesn't make a lot of sense.

Oh, and it definitely seems to be the select statement. I put a call
to Ada.Text_IO.Put_Line before the select statement, and immediately
when responding to an event. The delay occurs in between.
-- 
Brian May <bam@snoopy.apana.org.au>

Re: timeouts

[Stephen Leake]

Brian May <bam@snoopy.apana.org.au> writes:

> >>>>> "Stephen" == Stephen Leake <stephen_leake@acm.org> writes:
> 
>     Stephen> The 'pragma Debug' was in one of the generic packages, so
>     Stephen> it gets compiled when you instantiate it. Hmm. I just
>     Stephen> grep'ed in
> 
>     Stephen> GNAT-3.15p/lib/gcc-lib/pentium-mingw32msv/2.8.1/adainclude/
> 
>     Stephen> for "pragma Debug", and found 40 hits. But the are all in
>     Stephen> the tasking packages. Have you applied any patches?
> 
> Strange. No I haven't applied any patches. However, this was mingw32
> 3.4.x, what you checked would appear to be GNAT 3.15p? Or am I
> mistaken?

Yes, I checked 3.15p. I thought that's what you were using; my mail
reader wouldn't fetch the original post.

>     Stephen> I realize this isn't going to help you, but this is an
>     Stephen> example of why Windows is known as neither reliable nor
>     Stephen> real-time.
> 
> Yes, no doubt Linux would solve all of these problems, and more...

Hm. In _my_ line of work, Linux is no more realtime than Windows. I
use Lynx, or VxWorks.

-- 
-- Stephe

Re: timeouts

[Jano]

Brian May wrote:

> With gnat 3.15p, after approx 12 hours, my timeouts stopped working
> and/or took excessively long (e.g. in the order of hours instead of
> 0.1 of a second).

According to my experience, the bug can take any arbitrary amount of 
time to appear. I had a test program with intensive tasking which would 
trigger it in much less than 12 hours, usually around an hour and 
sometimes in 10 minutes.

Re: Cygwin and gcc-ada 3.4.1 (was Re: timeouts)

[Dr Steve Sangwine]

On Fri, 27 Aug 2004 12:31:52 +0200, Jano <notelacreas@porfavor.no>
wrote:

>I have a doubt after all this talk about the convenience of migrating to 
>3.4.1:
>
>* I see the Mingw is in candidate status (may be good enough).

I have been using MinGW/gcc 3.4.1 for some time, and not found any
problems with it (and I did find problems with earlier releases of
gcc 3).


>
>* If I'd choose to use the cygwin one, would the executables produced 
>require the cygwin1.dll? (I suppose so, this is my doubt).

I think so, the advantage of MinGW is that it produces code that will
run without any special DLLs.
>
>Would you say that is definitely preferable to use 3.4.1 over a patched 
>3.15p?

I would say yes, but I may not have exercised it enough and there is a
possibility you will hit a problem in 3.4.1 that is not present in
3.15p.

Steve Sangwine

>
>Thanks in advance,
>
>A. Mosteo.

SPARK

[Robert Matthews]

I see there is a discussion of SPARK over at LWN:
http://lwn.net/Articles/336656/

Robert

SPARK

[Yannick Duchêne (Hibou57)]

Hello,

Short title, “SPARK”, as short as a subset (joking)

I wanted to start some SPARK related questions, ... “GNAT packages in  
Linux” kept apart.


Well, sorry for that, my first question gonna be about license. The GPL  
applies to SPARK-GPL (oh? really?). How does it apply ? I'm dubious about  
it in this context, because using SPARK to check an implementation does  
not implies any kind of linking to any binary or library, and I did not  
see anywhere something stating there was license restrictions on the usage  
of SPARK annotations in Ada sources.

What are the concrete restrictions so ?



Hope this first question will get a short answer, so let us jump to the  
second question, which is intended to start with one major deal of SPARK  
for people who know/use Ada : Ada subset and restrictions (not to disclaim  
or disagree with, mostly to talk and understand more).

The Praxis reference for SPARK-95 says :

[Praxis SPARK95 3]
> SPADE-Pascal was developed essentially by excising from
> ISO-Pascal those features which were considered particularly
> “dangerous”, or which could give rise to intractable validation
> problems - such as variant records,
That said, variant record can be emulated by user or program too, as  
that's just what were doing many people when there was no language support  
for that. What is different when the Pascal or Ada variant record compared  
to a user or program doing explicitly the same ? May be the answer is just  
in one of the last three words : “explicitly” ?

Does this quotation from the Praxis's reference about SPARK suggests SPARK  
has some troubles with the implicit or the underlying ?

If SPARK could know about a formalization of what's going on with variant  
records, as explicit as would be the same made by the user or program,  
would that solve the trick ?

What would possibly make this difficult or non-trustable ?

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Thu, 13 May 2010 00:55:02 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> Hope this first question will get a short answer, so let us jump to the  
> second question, which is intended to start with one major deal of SPARK  
> for people who know/use Ada : Ada subset and restrictions (not to  
> disclaim or disagree with, mostly to talk and understand more).

An important quote every one should know about ; especially the last  
sentence:

[Praxis SPARK 95 (5)]
> Some readers may be dismayed to see so many features of Ada removed,
> and feel that SPARK is “too small”. It is by no means the largest
> subset of Ada which would be amenable to analysis by the techniques
> employed in SPADE, but it is significantly larger than SPADE-Pascal,
> which has been found adequate for a substantial number of
> safety-critical projects. The additional features which appear in
> SPARK (such as packages and private types) make programming simpler
> and safer, rather than complicate the verification task. Of course,
> the extent to which Ada must be simplified for high-integrity
> programming will be a matter of opinion: our preoccupation with
> simplicity is based on experience of what can be achieved with a
> high degree of confidence in practice, rather than what can be
> proved in principle.


-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Yannick Duchêne (Hibou57)]

Some quick though to feed the talk and give interested parties an  
opportunity to take part.

Although I can understand most of the restrictions SPARK applies (a big  
amount of them did not ever requires to use SPARK to be meaningful and  
beneficial and I do apply lot of them already), I still don't understand  
one : the restriction of not using derived type (except tagged type, which  
are supported by SPARK). What was the rational for that ?

Functions may have legitimate side effects, like for memoisation.  
Memoisation is a kind of optimization and optimizations should be  
transparent to clients. SPARK would requires to split it into two parts: a  
kind of “prepare/compute” procedure and a “get result” function ; the  
procedure being supposedly invoked prior to each function invokation. Did  
you ever face this ?

Block statements are not allowed in SPARK. Let say a procedure can do the  
same. Was this only to have one-matter-one-feature (avoid to have both  
block-statement and procedure, and keep only one) for the sake of  
simplicity or was there some other reasons properly dealing with  
verifiability ?

-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Thu, 13 May 2010 00:55:02 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> How does it apply ? I'm dubious about it in this context, because using  
> SPARK to check an implementation does not implies any kind of linking to  
> any binary or library, and I did not see anywhere something stating  
> there was license restrictions on the usage of SPARK annotations in Ada  
> sources.

At least the package SPARK_IO on Windows is MGPL :

[from SPARK_IO header]
-- As a special exception, if other files instantiate generics from this  
unit,
-- or you link this unit with other files to produce an executable, this  
unit
-- does not by itself cause the resulting executable to be covered by the  
GNU
-- General Public License. This exception does not however invalidate any  
other
-- reasons why the executable file might be covered by the GNU Public  
License.


-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[stefan-lucks]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 1713 bytes --]

On Thu, 13 May 2010, Yannick Duch�ne (Hibou57) wrote:

> Functions may have legitimate side effects, like for memoisation. Memoisation
> is a kind of optimization and optimizations should be transparent to clients.
> SPARK would requires to split it into two parts: a kind of �prepare/compute�
> procedure and a �get result� function ; the procedure being supposedly invoked
> prior to each function invokation. Did you ever face this ?

When working with SPARK, it is difficult *not* to face that. E.g., 
usually, you would write a pseudorandom number generator as 

  function Rnd return T is
  begin
    Global_State := f(Global_State);
    return g(Global_State);
  end; 

In SPARK, you have to replace the function RND by a procedure, which 
delivers the result as an out parameter. 

Very inconvenient! But reasonable:

Note that the result from evaluating an expression such as "Rnd + Rnd**2" 
depends on the order of evaluation, which isn't specified in the Ada 
standard. If we write I for the initial global state, then "Rnd + Rnd**2" 
can either evaluate to

  f(g(I) + f(f(g(I)))**2,

or to

  f(f(g(I))) + f(g(I))**2.

Such an unspecified behaviour makes static analysis very difficult. In 
principle, you would have to consider all possible orders of evaluation 
and check if something is going wrong. That would be very hard for SPARK, 
and, with a few legitimate exceptions, such that pseodorandom numbers, 
this is bad programming style anyway. Thus, SPARK prohibits this. 

-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Thu, 13 May 2010 11:28:03 +0200, <stefan-lucks@see-the.signature> a  
écrit:
> When working with SPARK, it is difficult *not* to face that. E.g.,
> usually, you would write a pseudorandom number generator as
>
>   function Rnd return T is
>   begin
>     Global_State := f(Global_State);
>     return g(Global_State);
>   end;
>
> In SPARK, you have to replace the function RND by a procedure, which
> delivers the result as an out parameter.

Yes, an example from Barnes gives the same:
Quote from  
http://people.cis.ksu.edu/~hatcliff/890-High-Assurance/Slides/Barnes-Ch-02-Language-Principles.pdf

    package Random_Numbers
    --# own Seed;
    --# initializes Seed;
    is

       procedure Random(X: out Float);
       --# global in out Seed;
       --# derives X, Seed from Seed;

    end Random_Numbers;

    package body Random_Numbers is

       Seed: Integer;
       Seed_Max: constant Integer := … ;

       procedure Random(X: out Float) is
       begin
          Seed := … ;
          X := Float(Seed) / Float(Seed_Max);
       end Random;

    begin -- initialization part
       Seed := 12345;
    end Random_Numbers


> Very inconvenient! But reasonable:

For that purpose, yes, as a radom generator is not a pure function.

> Note that the result from evaluating an expression such as "Rnd + Rnd**2"
> depends on the order of evaluation, which isn't specified in the Ada
> standard. If we write I for the initial global state, then "Rnd + Rnd**2"
> can either evaluate to
>
>   f(g(I) + f(f(g(I)))**2,
>
> or to
>
>   f(f(g(I))) + f(g(I))**2.
A function optimized (which save computing of already computed inputs)  
using memoisation, does not exposes this behavior.

> Such an unspecified behaviour makes static analysis very difficult. In
> principle, you would have to consider all possible orders of evaluation
> and check if something is going wrong. That would be very hard for SPARK,
> and, with a few legitimate exceptions, such that pseodorandom numbers,
> this is bad programming style anyway. Thus, SPARK prohibits this.
Indeed, there should not be any attempt to make proof on a language which  
would allow function whose result depends on the invokation time-stamp,  
and so whose result may depend on evaluation order.

Functions using memoisation are different case and are still pure  
function. What change between each invokation, is not the result, just the  
time to compute it (which may be shorter for some next invokation).

How to make it formal : may be giving the proof the function is the only  
one to access memoisation storage between function invokation, so, that  
this data are mechanically private to the function. Then, demonstrate  
there is two paths to the result : one which is the basic computation and  
one which retrieve the result of a similar previous computation. This  
latter step could rely on the computation of a key to access this data.  
Then demonstrate that for a given input, the computed key is always the  
same (input <-> key association). Now, the hard part may be to demonstrate  
the key is used to access the result which was computed previously for the  
same input that the one which was used to compute the key.

Obviously, the function should be the only one to access this data.

There is a concept in SPARK, the one of variable package and  
state-machines. May be there could be some room for a concept which could  
be something like function-package ?

Just some seed of an idea... will think about it some later day

-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Yannick Duchêne (Hibou57)]

An AdaCore/Praxis webinar, talks about a tool which make VCG files more  
readable, producing a graph representation of these, using GraphViz. This  
looks useful.

Go there to read or hear about it :  
http://www.adacore.com/home/products/gnatpro/webinars/ and choose “Getting  
started with SPARK (October 13, 2009)”, that's about in the last third  
part.

However, I was not able to find this in the SPARK installation directory  
and did not find more on the web.

Do someone know any points, docs or links ?

That's not required to run the Examiner nor the Simplifier, I know,  
however this really seems to make things more readable.

-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Rod Chapman]

On May 13, 5:54 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> An AdaCore/Praxis webinar, talks about a tool which make VCG files more  
> readable, producing a graph representation of these, using GraphViz. This  
> looks useful.

Run the Examiner with -vcg -debug=V
(see section 3.1.4 of the Examiner User Manual)...

Then go grab GraphViz from www.graphviz.org

Have fun...
 - Rod Chapman, SPARK Team, Praxis

Re: SPARK

[Yannick Duchêne (Hibou57)]

> Run the Examiner with -vcg -debug=V
> (see section 3.1.4 of the Examiner User Manual)...
OK. I had seen the debug option from the help command and though this was  
not the good one.
Finally, this is the “debug=d” which produce dot files for GraphViz.  
However, the v and V values also gives readable output in the form of a  
list (raw text).

Note for the Windows platform : the prefix for SPARK's command line  
switches is "/" instead of "-" ("/" is indeed the native Windows style for  
command line options).

> Have fun...
For sure I will :)


-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Rod Chapman]

On May 13, 8:43 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> > Run the Examiner with -vcg -debug=V
> > (see section 3.1.4 of the Examiner User Manual)...
>
> OK. I had seen the debug option from the help command and though this was  
> not the good one.
> Finally, this is the “debug=d” which produce dot files for GraphViz.  
> However, the v and V values also gives readable output in the form of a  
> list (raw text).

-debug=d dumps expression DAGS in DOT format.

-debug=v or V produces output on the screen AND also produces
DOT format for the VCG graph(s) alongside the generated .vcg
files.  if you use -debug=V and then look at the sequence of generated
graphs in numerical order, you'll see how the VC-generator works!

> Note for the Windows platform : the prefix for SPARK's command line  
> switches is "/" instead of "-" ("/" is indeed the native Windows style for  
> command line options).

We have now switched to use "-" on all platforms, so it's best
to use "-" on Windows now...
 - Rod

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Thu, 13 May 2010 22:05:05 +0200, Rod Chapman  
<roderick.chapman@googlemail.com> a écrit:
> -debug=d dumps expression DAGS in DOT format.
>
> -debug=v or V produces output on the screen AND also produces
> DOT format for the VCG graph(s) alongside the generated .vcg
> files.  if you use -debug=V and then look at the sequence of generated
> graphs in numerical order, you'll see how the VC-generator works!
Yes, was confused by previous runs which has left some .dot files in the  
place.

The HTML output (-html) seems also recommended, as it produce even more  
handily browsable stuff than only relying on the Location pane of GPS.

If this can ever be useful, here is a simple Windows script to generate  
all images for each dot files. For Windows users, you can then simply open  
any one image and watch all using the Windows image-slide capabilities.  
Doing so, you can quickly switch from one image to another, to see these  
like in a stroboscopic animation.

rem ----- Graphs_To_Images.bat ---------------------------

@echo off
cls

rem Set you input and input directory here. The Dot_Exe_Path variable
rem is the path to your dot binary. If in the PATH, simply leave it as
rem dot.exe. Input_Directory is the one you gave to the Examiner with its
rem output_directory option.
set Input_Directory=SPARK
set Output_Directory=Graphs_Images
set Dot_Exe_Path=dot.exe

rem Ensure the output directory exists
if not exist %Output_Directory% md %Output_Directory%

rem Cleanup the content of the output directory to not have
rem any previous images which would now be "garbages".
del /Q %Output_Directory%\*.png
del /Q %Output_Directory%\*.gif
del /Q %Output_Directory%\*.svg

rem For each .dot file in input directory, create a PNG image in output
rem directory. The images names are after the ones of the .dot files.
for %%f in (%Input_Directory%\*.dot) do %Dot_Exe_Path% -Tpng  
-o%Output_Directory%\%%~nf.png %%f

rem Cleanup .dot files as well, to not have a cluttered directory (we may
rem want to quickly find relevant .vcg and report files).
del /Q %Input_Directory%\*.dot

rem For safety, assign an empty strings to variables, as these are always
rem global with Windows cmd/bat files.
set Input_Directory=
set Output_Directory=
set Dot_Exe_Path=

rem ----- End of file ------------------------------------

-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Yannick Duchêne (Hibou57)]

Hello, once again playing with checker and examiner,

Within all the documentations installed with SPARK, there are some named  
SPARK_QRGn.pdf. The one SPARK_QRG1.pdf contains a summary of annotations  
to be used with the language.

I wonder if this document is part of the language definition or, if not,  
if I'm missing some documentations somewhere.

The reason of this doubt is, an example, the “--# assert ... ;” annotation  
which is documented in SPARK_QRG1, and in no other documentation I've  
read. I did not read all deeply at the time, and just had an overview of  
some. Anyway, I searched the “Examiner_UM.pdf”, “SPARK95.pdf” among others  
for “# assert” in the text, and did not found any occurrence. I can see it  
only in “SPARK_QRG1.pdf”.

Is this file part of the language definition or did I missed some relevant  
documentation elsewhere ?

-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Yannick Duchêne (Hibou57)]

The Quick Reference Card #1 talks about “type assertion”:

> A type assertion allows the user to specify the base type which the
> compiler will associate with a signed integer type. The base type
> must be supplied to the Examiner in the configuration file. This
> assertion allows the Examiner to generate VCs which are much more
> readily discharged [RTC 5.2].
>
> Example:
> type T is range 1 .. 10
> --# assert T’Base is Short_Short_Integer;

As the Examiner ignore any representation clauses [SPARK 95 (13.1)], it  
cannot care to any implicit representation clause either. So what's the  
purpose of this kind of assertions ? Does the examiner check something  
else which is not only the range ? Does it have something to deal with  
type conversions ?

-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Yannick Duchêne (Hibou57)]

Suspected error.

Unless I'm wrong for some reason, it seems the Quick Reference Card #1  
contains an error.

About “return annotation”, it give the following exemple:

    function Max(X, Y: Integer) return Integer;
    --# return M => (A >= B -> M = X) and
    --#             (B >= A -> M = Y);

What're A and B if they aren't X and Y ?

-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Yannick Duchêne (Hibou57)]

> The reason of this doubt is, an example, the “--# assert ... ;”  
> annotation which is documented in SPARK_QRG1, and in no other  
> documentation I've read. I did not read all deeply at the time, and just  
> had an overview of some. Anyway, I searched the “Examiner_UM.pdf”,  
> “SPARK95.pdf” among others for “# assert” in the text, and did not found  
> any occurrence. I can see it only in “SPARK_QRG1.pdf”.
>
> Is this file part of the language definition or did I missed some  
> relevant documentation elsewhere ?

Found : it is detailed in the file Examiner_GenVCs.pdf (Generation of VCs  
for SPARK Programs)


-- 
pragma Asset ? Is that true ? Waaww... great

Re: SPARK

[Phil Thornley]

On 14 May, 04:07, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> The Quick Reference Card #1 talks about “type assertion”:
>
> > A type assertion allows the user to specify the base type which the
> > compiler will associate with a signed integer type. The base type
> > must be supplied to the Examiner in the configuration file. This
> > assertion allows the Examiner to generate VCs which are much more
> > readily discharged [RTC 5.2].
>
> > Example:
> > type T is range 1 .. 10
> > --# assert T’Base is Short_Short_Integer;
>
> As the Examiner ignore any representation clauses [SPARK 95 (13.1)], it  
> cannot care to any implicit representation clause either. So what's the  
> purpose of this kind of assertions ? Does the examiner check something  
> else which is not only the range ? Does it have something to deal with  
> type conversions ?
>
> --
> pragma Asset ? Is that true ? Waaww... great

Yannick,

These base type assertions are used to get the ranges for overflow
checks - see Section 5 of Generation of RTCs for SPARK Programs
(GenRTCs).

The Examiner can't validate this assertion, so it's up to the user to
get it right (but you might be able to use compiler assertions to
check it).  It is safe to assert a smaller base type than the compiler
actually chooses, so the portability problem can be reduced by
specifying the smallest possible base type.

Cheers,

Phil

Re: SPARK

[Phil Thornley]

On 14 May, 05:15, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:

> > Is this file part of the language definition or did I missed some  
> > relevant documentation elsewhere ?
>
> Found : it is detailed in the file Examiner_GenVCs.pdf (Generation of VCs  
> for SPARK Programs)

Yannick,

As you are discovering, the documentation for the optional proof
assertions in SPARK is not easy to find (it is spread across several
documents, and rather scattered within those documents).

You might find it helps to look at the tutorials on www.sparksure.com
(one set for the proof annotations and one set for the Proof Checker).

Cheers,

Phil

Re: SPARK

[Rod Chapman]

> As you are discovering, the documentation for the optional proof
> assertions in SPARK is not easy to find (it is spread across several
> documents, and rather scattered within those documents).

Noted.  For SPARK Pro 9.0, we merged all the Proof material
into one manual and gave it the rather more obvious title "Proof
Manual".
We also produced a one-page clickable index to _all_ the manuals,
which has also proven useful.
 - Rod Chapman, SPARK Team

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Fri, 14 May 2010 10:17:50 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> As you are discovering, the documentation for the optional proof
> assertions in SPARK is not easy to find (it is spread across several
> documents, and rather scattered within those documents).
I wouldn't say so much. There was actually in the QR #1, a little “[VCG  
3]: ...” and at the bottom of the card, something like “[VCG] Generation  
of VCs for SPARK Programs”, so cross references are there ; this was just  
that I missed one file (I finally moved all release notes documents  
elsewhere to make the docs directory more handy).

> You might find it helps to look at the tutorials on www.sparksure.com
> (one set for the proof annotations and one set for the Proof Checker).
Seems good material :) The link goes to my bookmarks (will tell about it  
at fr.comp.lang.ada also).

-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Fri, 14 May 2010 10:11:29 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> It is safe to assert a smaller base type than the compiler
> actually chooses, so the portability problem can be reduced by
> specifying the smallest possible base type.
Oh, yes, I see. Thanks Phil

-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Thu, 13 May 2010 22:05:05 +0200, Rod Chapman  
<roderick.chapman@googlemail.com> a écrit:
> We have now switched to use "-" on all platforms, so it's best
> to use "-" on Windows now...
>  - Rod
At least with the integration to GPS on Windows, the project properties  
tab for Examiner, does not work if "-" is used : option not recognized and  
no feed back in the sheet view. Only "/" works there (may be this is  
different now with SPARK 9, I don't know).

An example to check : in the command line options input field (at the  
bottom), writing “-index_file=my_index.idx”, makes the the corresponding  
input field to become empty (at the top of the property sheet), and it  
comes back if “-index_file” is replaced with “/index_file”.

-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Yannick Duchêne (Hibou57)]

Anecdotal comment, surely not so much important :p

In multiple places in various documentations (of any sources), a sentence  
similar to “Proved by the Proof Checker” is used. Shouldn't this be  
“Proved with the Proof Checker” instead ? ... as the Proof Checker  
requires human interventions and is not automated.

-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Thu, 13 May 2010 05:06:23 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> Block statements are not allowed in SPARK. Let say a procedure can do  
> the same. Was this only to have one-matter-one-feature (avoid to have  
> both block-statement and procedure, and keep only one) for the sake of  
> simplicity or was there some other reasons properly dealing with  
> verifiability ?

Here is an answer:

A document from SparkSure ( http://www.sparksure.com/7.html ), namely  
Part4_Multiple_Paths.pdf, warns about consecutive conditional statements,  
giving the example of ten simple chained If statement which turns into  
1024 validation conditions. In this document, Phil logically advice to  
avoid such cases, using small procedures instead. Doing so, you end up  
with a single path instead of 1014.

So far this is not about blocks, however here comes the matter: block  
statements does not break such a chain of If statements and cannot be  
given annotations. Lack of annotations with block statement makes these  
ineffective to reach the goal of simplifying the program provability.

So why not annotations on block statements ? Well, simply because a block  
statement does not come with a signature and using a procedure instead of  
a block statement, requires you to better specify what was the role of  
that block. And adding extra-annotations to the language, to be used with  
blocks, would just load the language with unnecessary complications (not  
welcome in this area)

Finally, block statements are disallowed to help avoid explosive  
complexity.

-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Peter C. Chapin]

Yannick Duchêne (Hibou57) wrote:

>>
>>   f(g(I) + f(f(g(I)))**2,
>>
>> or to
>>
>>   f(f(g(I))) + f(g(I))**2.
> A function optimized (which save computing of already computed inputs)  
> using memoisation, does not exposes this behavior.

If it works properly, yes, but what if it doesn't?

> How to make it formal : may be giving the proof the function is the only  
> one to access memoisation storage between function invokation, so, that  
> this data are mechanically private to the function. Then, demonstrate  
> there is two paths to the result : one which is the basic computation and  
> one which retrieve the result of a similar previous computation. This  
> latter step could rely on the computation of a key to access this data.  
> Then demonstrate that for a given input, the computed key is always the  
> same (input <-> key association). Now, the hard part may be to demonstrate  
> the key is used to access the result which was computed previously for the  
> same input that the one which was used to compute the key.
> 
> Obviously, the function should be the only one to access this data.
> 
> There is a concept in SPARK, the one of variable package and  
> state-machines. May be there could be some room for a concept which could  
> be something like function-package ?

While this might be possible, it does sound rather complicated. I can see why
SPARK doesn't currently go down this path.

Peter

Re: SPARK

[Yannick Duchêne (Hibou57)]

Currently, I'm reading Phil's documents, the ones in the directory  
Proof_Annotations and especially looking at exercises (yes, he created  
some) in part 5 to 9 and 12.

Part 5, exercise 4, turns to be something interesting to me, as it leads  
me to some questions about the way the simplifier is using hypothesis.

I would like to be more explicit. Here is the relevant part (slightly  
modified)


    ---------------------------------------------------------------------
    -- Exercise 5.4
    ---------------------------------------------------------------------
    procedure Limit
      (X     : in out Integer;
       Lower : in     Integer;
       Upper : in     Integer)
    --# pre    Lower < Upper;
    --# post  ((X~ < Lower) -> (X = Lower)) and
    --#       ((X~ > Upper) -> (X = Upper)) and
    --#       (X in Lower .. Upper);
    is
    begin
       if X < Lower then
          X := Lower;
       elsif X > Upper then
          X := Upper;
       end if;
    end Limit;

    function Percent_Of_Range
      (Data    : Integer;
       Lowest  : Integer;
       Highest : Integer) return Percent_Type
    --# pre    (Lowest < Highest) and                        -- (1)
    --#        ((Highest - Lowest) <= Integer'Last) and      -- (2)
    --#        (((Highest - Lowest) * 100) <= Integer'Last); -- (3)
    --#
    is
       Local_Data : Integer;
       Part : Integer;
       Whole : Integer;
    begin
       Local_Data := Data;                                   -- (4)
       Limit (Local_Data, Lowest, Highest);                  -- (5)
       Part := Local_Data - Lowest;                          -- (6)
       Whole := Highest - Lowest;                            -- (7)
       return Percent_Type((Part * 100) / Whole);            -- (8)
    end Percent_Of_Range;


What's funny here, is about precondition line (2). If it is removed, the  
precondition become “(Lowest < Highest) and (((Highest - Lowest) * 100) <=  
Integer'Last)” and the simplifier fails to prove line (6) : it cannot  
prove the result will be lower than Integer'Last. I first though “(Highest  
- Lowest) * 100 <= Integer'Last” would be enough to also implies “Highest  
- Lowest < Integer'Last” ; it seems it is not. If you add precondition  
part (2), there is no more trouble with line (6).

Is this because of the way it is using hypotheses or is this because it  
miss some built-in rules to get all benefits from precondition part (3) ?

Now, there is still another unproved condition... at line (8), the  
simplifier cannot prove “((Local_Data - Lowest) * 100) / (Highest -  
Lowest) <= 100”. A first anecdote : funny to see it has expanded variables  
Part and Whole.

I wanted to solve in three steps and added the following between (6) and  
(7)


       --# assert Part <= Whole; -- (6.1)
       --# assert (Part * 100) <= (Whole * 100); -- (6.2)
       --# assert ((Part * 100) / Whole) <= ((Whole * 100) / Whole); --  
(6.3)


But the simplifier was not able to prove (6.1) nor (6.3) and was still not  
able to prove (8). About (6.2), and wanted to have a test, and added the  
following between (6.2) and (6.3):


       --# assert ((Part * 100) <= (Whole * 100)) ->
       --#        (((Part * 100) / Whole) <= ((Whole * 100) / Whole));


It was not able to prove it. Do I miss something or does it simply means  
the simplifier does not know about a rule which seems basic to me, that is  
(A <= B) -> ((A / C) <= (B / C)) ? ... which is still valid for integer  
arithmetic.

-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Yannick Duchêne (Hibou57)]

> It was not able to prove it. Do I miss something or does it simply means  
> the simplifier does not know about a rule which seems basic to me, that  
> is (A <= B) -> ((A / C) <= (B / C)) ? ... which is still valid for  
> integer arithmetic.
Sorry for a mistake, it should have been ((A <= B) and (A >= 0) and (C >  
0)) -> ((A / C) <= (B / C)), to keep it simple and just to talk about  
what's relevant here.


-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Yannick Duchêne (Hibou57)]

Another example, as much strange to me.


    procedure Limit
      (X     : in out Integer;
       Lower : in     Integer;
       Upper : in     Integer)
    --# pre    Lower < Upper;
    --# post  ((X~ < Lower) -> (X = Lower)) and
    --#       ((X~ > Upper) -> (X = Upper)) and
    --#       (X in Lower .. Upper);

    -- ....


       Limit (Local_Data, Lowest, Highest);
       Part := Local_Data - Lowest;
       Whole := Highest - Lowest;
       --# assert Part >= 0;
       --# assert Local_Data <= Highest;

    -- ....

The simplifier cannot prove “Local_Data <= Highest”, although the post  
condition of Limit states “X in Lower .. Upper” so that it should know  
“Local_Data in Lowest .. Highest” and then “Local_Data <= Highest”.

While perhaps I'm not using it the good way (as a beginner, this may be a  
possible case).

-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Phil Clayton]

On May 15, 5:41 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
>
>        --# assert ((Part * 100) <= (Whole * 100)) ->
>        --#        (((Part * 100) / Whole) <= ((Whole * 100) / Whole));
>
> It was not able to prove it. Do I miss something or does it simply means  
> the simplifier does not know about a rule which seems basic to me, that is  
> (A <= B) -> ((A / C) <= (B / C)) ? ... which is still valid for integer  
> arithmetic.

This isn't valid for all values of A, B and C: consider C = -1.  It
would be sufficient to know 0 < C, so perhaps sufficient information
needs to be propagated to show 0 < Whole ?

Phil C.

Re: SPARK

[Yannick Duchêne (Hibou57)]

Oh, something interesting:


    procedure Limit
      (X     : in out Integer;
       Lower : in     Integer;
       Upper : in     Integer)
    --# pre    Lower < Upper;
    --# post  ((X~ < Lower) -> (X = Lower)) and
    --#       ((X~ > Upper) -> (X = Upper)) and
    --#       (X in Lower .. Upper);

    -- .....


       Limit (Local_Data, Lowest, Highest);
       --# assert Local_Data <= Highest;  -- (1)
       Part := Local_Data - Lowest;
       Whole := Highest - Lowest;
       --# assert Part >= 0;              -- (2)
       --# assert Local_Data <= Highest;  -- (3)

    -- .....


If (2) is removed, it can prove (1) and (3). If (2) is there, it fails to  
prove (3), while nothing changes Local_Data in the path from (1) to (3),  
and so (3) should be as much provable as (1).

When (2) is there, it seems to forget about the previously proved  
hypothesis (1) or about hypotheses which make (1) provable.

Will have to better understand how this “thing” thinks.

-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Yannick Duchêne (Hibou57)]

> This isn't valid for all values of A, B and C: consider C = -1.  It
> would be sufficient to know 0 < C, so perhaps sufficient information
> needs to be propagated to show 0 < Whole ?
>
> Phil C.
Yes, you are right, that's why I had previously apologized for this error  
and corrected it in a reply to the erroneous message.

Your exercises are interesting BTW.


-- 
There is even better than a pragma Assert: an --# assert

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Sat, 15 May 2010 21:08:05 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Oh, something interesting:
>
>
>     procedure Limit
>       (X     : in out Integer;
>        Lower : in     Integer;
>        Upper : in     Integer)
>     --# pre    Lower < Upper;
>     --# post  ((X~ < Lower) -> (X = Lower)) and
>     --#       ((X~ > Upper) -> (X = Upper)) and
>     --#       (X in Lower .. Upper);
>
>     -- .....
>
>
>        Limit (Local_Data, Lowest, Highest);
>        --# assert Local_Data <= Highest;  -- (1)
>        Part := Local_Data - Lowest;
>        Whole := Highest - Lowest;
>        --# assert Part >= 0;              -- (2)
>        --# assert Local_Data <= Highest;  -- (3)
>
>     -- .....
>
>
> If (2) is removed, it can prove (1) and (3). If (2) is there, it fails  
> to prove (3), while nothing changes Local_Data in the path from (1) to  
> (3), and so (3) should be as much provable as (1).

If “assert” is replaced by “check” then it can prove (3) even if (2) is  
there. So that


      procedure Limit
        (X     : in out Integer;
         Lower : in     Integer;
         Upper : in     Integer)
      --# pre    Lower < Upper;
      --# post  ((X~ < Lower) -> (X = Lower)) and
      --#       ((X~ > Upper) -> (X = Upper)) and
      --#       (X in Lower .. Upper);

      -- .....


         Limit (Local_Data, Lowest, Highest);
         --# check Local_Data <= Highest;  -- (1)
         Part := Local_Data - Lowest;
         Whole := Highest - Lowest;
         --# check Part >= 0;              -- (2)
         --# check Local_Data <= Highest;  -- (3)

      -- .....

is OK.

So let's talk about “assert” vs “check”.

[Generation of VCs for SPARK Programs (2.2)] says:
> each assert or check statement in the code is located at a point in
> between two executable statements, in general, ie it is associated
> with a point on the arc of the flowchart of the subprogram which
> passes between the two statements it appears between. Each such
> assertion specifies a relation between program variables which must
> hold at that precise point, whenever execution reaches it. Assert
> statements generate a cut point on the flowchart of the subprogram,
> check statements do not.

What does “cut point” means precisely ? Is it related or similar to the  
unfortunately too much famous Prolog's cut ? This seems to be the next  
question to be answered, and a focus to care about for peoples learning  
SPARK.

Is that this “cut point” which makes Simplifier to forget about previous  
hypotheses when “assert” is used ? (if that's really similar to Prolog's  
cut, then indeed, it likely to make the prover loose memory)

About one of the most worthy thing with proving : what's the better way to  
give hints to the prover ? Is it “assert” or “check” ? This example  
suggest the best way is “check”. Is this example representative of most  
cases or a just a special case ?


--
There is even better than a pragma Assert: an --# assert (or a --#  
check.... question pending)

Re: SPARK

[Phil Clayton]

On May 15, 8:12 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Yes, you are right, that's why I had previously apologized for this error  
> and corrected it in a reply to the erroneous message.

Yes, I hadn't updated the web page to see your latest message.


> Your exercises are interesting BTW.

They're not mine - I'm a different Phil!  An unfortunate overloading
issue here...

Phil C.

Re: SPARK

[Yannick Duchêne (Hibou57)]

Ok, from some branch of this thread, you may have learned a question have  
raised about which one of “assert” or “check” should be used to write  
in-text proofs where the Simplifier could not prove it it/his/her self.

The answer to this is so much important that I give the answer to it from  
the root of this thread, instead of from the latter leaf.

So it is : Use Check, not Assert.

Here is a concrete example of what you can do with Check and which does  
not work with Assert. The example is detailed, I mean, exposes detailed  
proofs, over what may have been sufficient. This is because I like  
explicit and expressive things, and this was also to be sure nobody could  
miss a single step of the proof and nobody could have any doubt about the  
usefulness of such a approach in software conception. That's also the  
reason why the exercise upon which this is based, was a bit modified (like  
using two intermediate variables instead of subexpressions.. I do that  
oftenly on my side).

Here is :


    procedure Limit
      (X     : in out Integer;
       Lower : in     Integer;
       Upper : in     Integer)
    --# pre    Lower < Upper;
    --# post  ((X~ < Lower) -> (X = Lower)) and
    --#       ((X~ > Upper) -> (X = Upper)) and
    --#       (X in Lower .. Upper);
    is
    begin
       if X < Lower then
          X := Lower;
       elsif X > Upper then
          X := Upper;
       end if;
    end Limit;

    function Percent_Of_Range
      (Data    : Integer;
       Lowest  : Integer;
       Highest : Integer) return Percent_Type
    --# pre    (Lowest < Highest) and
    --#        ((Highest - Lowest) <= Integer'Last) and
    --#        (((Highest - Lowest) * 100) <= Integer'Last);
    is
       Local_Data : Integer;
       Part       : Integer;
       Whole      : Integer;
    begin
       Local_Data := Data;
       -- Local copy of Data to be allowed to modify it. We only need
       -- a modified version locally, the caller does not need this.

       Limit
         (X     => Local_Data, -- in out.
          Lower => Lowest,     -- in
          Upper => Highest);   -- in.

       Part  := Local_Data - Lowest;
       Whole := Highest - Lowest;

       -- We are to prove that ((Part * 100) / Whole) is in 0 .. 100.

       -- (1) Prove that Part >= 0.
       --# check Local_Data in Lowest .. Highest;
       --# check Local_Data >= Lowest;
       --# check (Local_Data - Lowest) >= 0;
       --# check Part >= 0;

       -- Given (1), it's obvious that (Part * 100) >= 0.

       -- (2) Prove that Whole is > 0.
       --# check Lowest < Highest;
       --# check Highest > Lowest;
       --# check (Highest - Lowest) > 0;
       --# check Whole > 0;

       -- Given (2), it's obvious that ((Part * 100) / Whole) is valid.
       -- Given (1) and (2), it's obvious that ((Part * 100) / Whole) >= 0.

       -- (3) Prove that (Whole >= Part). This is required for (4) which is
       --    to come.
       --# check Local_Data in Lowest .. Highest;
       --# check Highest >= Local_Data;
       --# check (Highest - Lowest) >= (Local_Data - Lowest);
       --# check Whole >= Part;

       -- (4) Prove that ((Part * 100) / Whole) is less or equal to 100.
       --# check Part <= Whole;
       --# check (Part * 100) <= (Whole * 100);
       --# check ((Part * 100) / Whole) <= ((Whole * 100) / Whole);
       --# check ((Part * 100) / Whole) <= 100;

       -- (5) Prove that the subexpression (Part * 100) will not
       --     commit an overflow.
       --# check (((Highest - Lowest) * 100) <= Integer'Last);
       --# check (Whole * 100) <= Integer'Last;
       --# check Part <= Whole;
       --# check (Part * 100) <= Integer'Last;

       -- Given (1), we know ((Part * 100) / Whole) >= 0.
       -- Given (4), we know ((Part * 100) / Whole) <= 100.
       -- Given (5), we we know (Part * 100) will not commit an overflow.
       -- Given (1) and (2) and(5), the following statement is then proved  
to
       -- be valid and meaningful.

       return Percent_Type ((Part * 100) / Whole);

    end Percent_Of_Range;

A working example of a step by step proof of every things required to be  
proven.

Waaw... I like it so much, I love it. This is the way I was thinking  
software should be built for so long ! I was waiting for such a thing for  
about 14 years you know !

I use to learn about VDM when I was younger, hire books about it in  
libraries, use to think about creating my own implementation of VDM, but  
failed to find the language specification (and was frightened about the  
idea to setup my own language in this area).

And now, I see SPARK can do nearly the same.

Well, although wonderful, that's still not perfect : why is there a  
Checker (which I didn't used here) and why no provision to write in-text  
what is done with the Checker ? That's what I was attempting to do here.  
It works, but I miss something like explicit “from (1) and (2) infer ....  
” etc. I cannot give names or numbers to Check clauses and cannot  
explicitly refer to these. I cannot nor explicitly refer to precondition  
in inferences (like in (5), where the reference to a precondition is  
implicit, not explicit).

Is there some provision for such a thing ?

Yes, I may wish too much... that's not perfect, while still wonderful. Do  
you feel too ? :)


-- 
There is even better than a pragma Assert: an --# assert (or a --#  
check... question pending)

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Sun, 16 May 2010 00:48:33 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Ok, from some branch of this thread, you may have learned a question  
> have raised about which one of “assert” or “check” should be used to  
> write in-text proofs where the Simplifier could not prove it it/his/her  
> self.
>
> The answer to this is so much important that I give the answer to it  
> from the root of this thread, instead of from the latter leaf.
>
> So it is : Use Check, not Assert.
> [...]

Part 6 of Phil's document says:

> For both check and assert, there is a VC generated that has
> the current program state as hypotheses and the <Boolean
> expression> as the conclusion.
I've meet something different (see previous messages in this thread), or  
at least, the current state is not represented with the same set of  
hypotheses.


> For code that does not contain any loops, there is
> (in principle) never any need for either of these
> annotations since they cannot make unprovable VCs
> into provable VCs.
Sorry, I can't buy that at all. I could make VCs provable, and this was  
otherwise not provable by the simplifier, using Check clauses.

Sorry friend, I'm not dreaming : this really happened.

-- 
There is even better than a pragma Assert: a SPARK --# check.

Wanted: if you know about some though in the area of comparisons between  
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.

Re: SPARK

[Yannick Duchêne (Hibou57)]

> Sorry, I can't buy that at all. I could make VCs provable, and this was  
> otherwise not provable by the simplifier, using Check clauses.
>
> Sorry friend, I'm not dreaming : this really happened.
No, OK, I'm wrong : miss-understood the meaning of unprovable in this  
context.

You're OK.

-- 
There is even better than a pragma Assert: a SPARK --# check.

Wanted: if you know about some though in the area of comparisons between  
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.

Re: SPARK

[Yannick Duchêne (Hibou57)]

Request for confirmation.

In Praxis's documentations, there is a file named Checker_Rules.pdf, title  
is “SPADE Proof Checker Rules Manual”, which list Checker's built-in  
rules. I do not see any reason why the Examiner/Simplifier would have a  
different rules set than the Checker, so I suppose this rules set is also  
the one used by the Examiner/Simplifier. I would just want to be sure :  
someone can confirm ?

If it is, this may explain why I meet some troubles proving one thing with  
real arithmetic (yes, I know real arithmetic is not safe and I must care,  
but this is just an exercise...)

-- 
There is even better than a pragma Assert: a SPARK --# check.

Wanted: if you know about some though in the area of comparisons between  
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.

Re: SPARK

[Peter C. Chapin]

Yannick Duchêne (Hibou57) wrote:

> Is that this “cut point” which makes Simplifier to forget about previous  
> hypotheses when “assert” is used ? (if that's really similar to Prolog's  
> cut, then indeed, it likely to make the prover loose memory)
> 
> About one of the most worthy thing with proving : what's the better way to  
> give hints to the prover ? Is it “assert” or “check” ? This example  
> suggest the best way is “check”. Is this example representative of most  
> cases or a just a special case ?

My understanding is that assert prevents the simplifier from using previous
material as hypotheses in following verification conditions---as you noticed
in your experiments. John Barnes talks about this in his book a little.
Mostly I think assert is intended for use in loops. Without it, SPARK needs
to consider each loop iteration as a spearate path which is clearly a problem
(since loops iterate a dynamic number of times). The assert "cuts" the loop
and reduces the problem to just

1. The path into the loop for the first time to the assert.
2. The path around the loop from assert to assert.
3. The path from the assert to whatever follows the loop.

It is necessary, I think, for SPARK to forget about previous "stuff" when
handling the assert since otherwise it would have to consider all the
previous loop iterations.

The check annotation asks SPARK to prove the check and then it can *add* that
information to the hypotheses of the following verification conditions rather
than start from scratch.

So to summarize perhaps a good rule might be to use assert to express loop
invariants and check for everything else. I welcome other comments on this.
I'm learning as well.

Peter

Re: SPARK

[Phil Thornley]

On 15 May, 21:23, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[big snip :-]

> What does “cut point” means precisely ? Is it related or similar to the  
> unfortunately too much famous Prolog's cut ? This seems to be the next  
> question to be answered, and a focus to care about for peoples learning  
> SPARK.

There may be multiple paths to any point (before/after/between
executeable statements).  For the purposes of VC generation, a "cut
point" is a point in the code that terminates all the paths that reach
it and there is a single path starting at that point.

The hypotheses of VCs include the local state that has been defined
along a path, and each path to a point will have different versions of
these hypotheses.

Therefore the hypotheses that are generated in VCs that follow a cut
point cannot include any of the hypotheses that have been included in
the VCs before the cut point - unless they are included in the
assertion at the cut point and therefore proved to be true for every
path that reaches that cut point.


> About one of the most worthy thing with proving : what's the better way to  
> give hints to the prover ? Is it “assert” or “check” ? This example  
> suggest the best way is “check”. Is this example representative of most  
> cases or a just a special case ?

You should always use 'check' when giving the Simplifier a hint - then
you don't lose any of the local state information.

Another key point to understand is that the Simplifier does not prove
all provable VCs (so when the tutorials ask you to "make all VCs
provable" don't expect to get all the VCs proved by the Simplifier.)

There are (at least) three ways to deal with these (other than
changing the code itself).
1) Give the Simplifier 'hints' by adding check annotations.
2) Use the Proof Checker to prove the VCs left after simplfication.
3) Give the Simplifier more rules to use ('user rules').

My experience is that trying 1) can get very frustrating as the
Simplifier sometimes seems to be extremely stupid.
2) works OK but isn't practical for any software under development as
the proof scripts that are created (and are needed each time the VCs
are generated) are extremely fragile to minor changes in the software.
The current recommendation is to use 3) - create user rules as
appropriate.  These are easy to write and usually work as expected.
(But they are a very powerful mechanism, so are correspondingly
dangerous - it is quite easy to create unsound user rules.)

(If you are working through the tutorials in sequence then user rules
are in section 11 - the next to the last).

Cheers,

Phil

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Sun, 16 May 2010 20:13:27 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> My understanding is that assert prevents the simplifier from using  
> previous
> material as hypotheses in following verification conditions---as you  
> noticed
> in your experiments. John Barnes talks about this in his book a little.
> Mostly I think assert is intended for use in loops. Without it, SPARK  
> needs
> to consider each loop iteration as a spearate path
Here is the word, as you said, this cut the path. That's what I've learned  
later too. This starts a new path, with a new hypotheses set, and indeed,  
forget about all previous.

Now we know why it is so.

> [...]
> So to summarize perhaps a good rule might be to use assert to express  
> loop
> invariants and check for everything else. I welcome other comments on  
> this.
It seems all is there.

> I'm learning as well.
Great! Cheers


-- 
There is even better than a pragma Assert: a SPARK --# check.

Wanted: if you know about some though in the area of comparisons between  
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Sun, 16 May 2010 20:17:49 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> [...]
> Therefore the hypotheses that are generated in VCs that follow a cut
> point cannot include any of the hypotheses that have been included in
> the VCs before the cut point - [...]
Otherwise this would not be a cut-point any more, indeed, and starting  
with a new state, is not a side effect, it's the purpose.

> Another key point to understand is that the Simplifier does not prove
> all provable VCs (so when the tutorials ask you to "make all VCs
> provable" don't expect to get all the VCs proved by the Simplifier.)
Unfortunately, I wanted to prove every things (cheese)

TBH, I did not work on all, just some and just had a quick overview on  
others.

> There are (at least) three ways to deal with these (other than
> changing the code itself).
Sorry for that Er Professor, I've modified it a bit (re-cheese).

> 1) Give the Simplifier 'hints' by adding check annotations.
> 2) Use the Proof Checker to prove the VCs left after simplfication.
As said in another message, this was exactly the purpose : I wanted to  
prove without relying on the Checker, in order to have all proofs in the  
text. It seems to be possible, as long as one is explicit enough.

> 3) Give the Simplifier more rules to use ('user rules').
I would better like add a very few rule in the whole system, better than  
adding some rules here and there, all being package specific.

> My experience is that trying 1) can get very frustrating as the
> Simplifier sometimes seems to be extremely stupid.
That's an important matter. On an other thread, on the french c.l.a (where  
I’ve talked about the same), I was afraid some people may think SPARK is  
not working properly and is unusable for that reason. That's why I  
insisted a lot on the Check clause and to not be afraid to detail proofs  
as much as needed.

> 2) works OK but isn't practical for any software under development as
> the proof scripts that are created (and are needed each time the VCs
> are generated) are extremely fragile to minor changes in the software.
> The current recommendation is to use 3) - create user rules as
> appropriate.  These are easy to write and usually work as expected.
> (But they are a very powerful mechanism, so are correspondingly
> dangerous - it is quite easy to create unsound user rules.)
I would prefer the choice #3, which seems more logical to me. Just that  
this may be better to add these rules system wide better than on a package  
basis. If I'm not wrong, there is provision for that also.

The requirement for a rule to be sound, is indeed important. There may be  
some rule of thumb in that area, like check all special cases, all special  
ranges. As an example, before adding a rule on real, one may carefully  
check the rule is valid for multiple combinations of special values and  
bounds and range on each items appearing in the rule, like 0, 1, -1, 0 ..  
1, 0 .. -1, > 1, < -1, and so on. The same with set, there are special  
values as well : empty set/sequence, one element set/sequence, more than  
one, a set included in an other, etc.

In that area, I was wondering how built-in rules were  choose : from a  
well know set of scientist ? Empirically ? By expansion during SPARK's  
life ? Others ?

I was wondering about it, because I could not find one rule which seems  
important to me, and which does not seems to be part of the predefined set  
(well, there are actually +500 rules, however, may be some useful rules  
are still missing).

> (If you are working through the tutorials in sequence then user rules
> are in section 11 - the next to the last).
Yes, I've seen it, and I've also read Part 6, which is about the  
difference between Check and Assert (I've it later after the question you  
were answering).

Have a nice day (Peter as well, obviously)

Yannick D.

-- 
There is even better than a pragma Assert: a SPARK --# check.

Wanted: if you know about some though in the area of comparisons between  
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Sun, 16 May 2010 07:28:16 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Request for confirmation.
>
> In Praxis's documentations, there is a file named Checker_Rules.pdf,  
> title is “SPADE Proof Checker Rules Manual”, which list Checker's  
> built-in rules. I do not see any reason why the Examiner/Simplifier  
> would have a different rules set than the Checker, so I suppose this  
> rules set is also the one used by the Examiner/Simplifier. I would just  
> want to be sure : someone can confirm ?
>
> If it is, this may explain why I meet some troubles proving one thing  
> with real arithmetic (yes, I know real arithmetic is not safe and I must  
> care, but this is just an exercise...)

About adding rules.

The Praxis document named Checker_Rules.pdf says

> The tool Buildchlib is no longer shipped with the Checker
> following the release of version 2.05. The use of
> user-defined rule files is still permitted, through the
> consult command. For further information contact
> Praxis High Integrity Systems.
So there is no way to add a rule system-wide as I was expecting.

Attempting to change the content of an *.RUL file in the lib/checker/rules  
directory, has no effect at all. The rules seems really compiled inside  
Simplifier and Checker.

Here are the rules I was to add in NUMINEQS.RUL:

    inequals(122):  X/Y<1     may_be_deduced_from [ X>=0, Y>0, Y>X ].
    inequals(123):  X/Y<1     may_be_deduced_from [ X<=0, Y<0, Y<X ].
    inequals(124):  X/Y>(-1)  may_be_deduced_from [ X>=0, Y<0, (-Y)>X ].
    inequals(125):  X/Y>(-1)  may_be_deduced_from [ X<=0, Y>0, Y>(-X) ].

It works only if added in an .RLU file.

Note: writing something like ...

    inequals(124):  X/Y>(-1)  may_be_deduced_from [ X>=0, Y<0,  
abs(Y)>abs(X) ].

... although parsed correctly, will turns into a rule which may not be  
applied by Simplifier. It seems rules must be given in the most  
straightforward way. This may explain why ARITH.RUL contains such a thing:

    arith(1):    X*1             may_be_replaced_by X.
    arith(2):    1*X             may_be_replaced_by X.

Commutativity seems not expected to be automatically applied or attempted.

About the rules I was to add, I tried something like:

    inequals(122):  [ X/Y>=0, X/Y<1 ]    may_be_deduced_from [ X>=0, Y>0,  
Y>X ].

This is at least parsed without syntax error message, but not applied.

I've noticed Simplifier seems to read an .RUL file it is belongs to a  
directory where it is reading .VCG files (I don't why it do that). I've  
noticed that while I was playing a bit with it :p

Will have to search for another way to add rules system-wide, if possible.


Have a nice day



-- 
There is even better than a pragma Assert: a SPARK --# check.

Wanted: if you know about some though in the area of comparisons between  
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.

Re: SPARK

[Phil Thornley]

On 18 May, 19:01, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> I've noticed Simplifier seems to read an .RUL file it is belongs to a  
> directory where it is reading .VCG files (I don't why it do that). I've  
> noticed that while I was playing a bit with it :p
>
> Will have to search for another way to add rules system-wide, if possible.

Yannick,

I don't think that the toolset provides what you are looking for*.

The only recognised way to supply additional rules to the Simplifier
are as user rules - the full details about this are in Section 7 of
the Simplifier user manual.  This section also describes how the user
rules are applied.

It is unfortunate that user rules are less effective than the rules
built into the Simplifier as they are only used once the normal
Simplifier strategies have failed to prove a conclusion (see the
introduction of Section 3).

For example an inference rule will only be used if it *directly*
proves a conclusion.
Section 7.2.1: "In order for the Simplifier to be able to make use of
the rule, it must find an instance of the rule by pattern-matching it
against the current VC (for inference rules, this essentially means
against the undischarged conclusions of the VC)"

Cheers,

Phil

* Except that, of course, the full source of the Simplifier is
available, and there is nothing to stop you making changes to it!

Re: SPARK

[Simon Wright]

Phil Thornley <phil.jpthornley@googlemail.com> writes:

> * Except that, of course, the full source of the Simplifier is
> available, and there is nothing to stop you making changes to it!

I believe you need the non-free (ie, quite expensive) SICSTUS Prolog
system to build the tools from source (there is SICSTUS-special code
which doesn't work under GNU Prolog).

The GPL SPARK 8.1.1 binary release doesn't run well under Mac OS X Snow
Leopard (problems with exception handling in 64-bit executables).

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Wed, 19 May 2010 22:38:07 +0200, Simon Wright <simon@pushface.org> a  
écrit:

> Phil Thornley <phil.jpthornley@googlemail.com> writes:
>
>> * Except that, of course, the full source of the Simplifier is
>> available, and there is nothing to stop you making changes to it!
>
> I believe you need the non-free (ie, quite expensive)
Question on side: Why is it always either free or either expansive ? Why  
not multiple levels between both of these extremities ?

> SICSTUS Prolog
> system to build the tools from source (there is SICSTUS-special code
> which doesn't work under GNU Prolog).
You may be true, as I remember an old topic (about two one years ago and a  
half), of someone getting into trouble trying to build SPARK with his  
favorite Prolog compiler.

> The GPL SPARK 8.1.1 binary release doesn't run well under Mac OS X Snow
> Leopard (problems with exception handling in 64-bit executables).
Where does the SPARK executable makes use of exceptions ? I have read  
something asserting the SPARK system is it-self checked to be runtime  
exceptions free. Perhaps this is in an external dependency part.

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Wed, 19 May 2010 10:09:33 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> For example an inference rule will only be used if it *directly*
> proves a conclusion.
> Section 7.2.1: "In order for the Simplifier to be able to make use of
> the rule, it must find an instance of the rule by pattern-matching it
> against the current VC (for inference rules, this essentially means
> against the undischarged conclusions of the VC)"
Thanks for the detail Phil.

> * Except that, of course, the full source of the Simplifier is
> available, and there is nothing to stop you making changes to it!
Simon has tell about a limit in this area. I see another, which is the  
biggest to me : this would be a kind of forking, and a fork is not any  
more something common. This would be a valid way for my own use only,  
which could not be shared any more ; someone else could not check  
something from me using his/her own SPARK installation. I use to be  
interested is some specifications of some other languages of the like,  
which I've never found, and gave up with the idea (of the probably too  
much big work) to attempt to create one, for this exact reason : this  
would be specific to me, to what I use. In this area, it is mandatory to  
have standards, otherwise, this is not as much interesting.

This is not only about checking for validity, this is also about  
expressing why it is so to others in way hey can trust and read.

Re: SPARK

[Simon Wright]

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

>> The GPL SPARK 8.1.1 binary release doesn't run well under Mac OS X Snow
>> Leopard (problems with exception handling in 64-bit executables).
> Where does the SPARK executable makes use of exceptions ? I have read
> something asserting the SPARK system is it-self checked to be runtime
> exceptions free. Perhaps this is in an external dependency part.

Yes; the traceback is

#0  0x00007fff82610886 in __kill ()
#1  0x00007fff826b0eae in abort ()
#2  0x00000001000837ce in uw_init_context_1 ()
#3  0x00000001000838e8 in _Unwind_Backtrace ()
#4  0x00000001000c8279 in __gnat_backtrace ()
#5  0x00000001000c42dd in system__traceback__call_chain ()
#6  0x0000000100088259 in ada__exceptions__call_chain ()
#7  0x0000000100087a61 in ada__exceptions__exception_propagation__propagate_exceptionXn ()
#8  0x0000000100088548 in __gnat_raise_nodefer_with_msg ()
#9  0x00000001000885aa in __gnat_raise_exception ()
#10 0x00000001000b5b87 in system__file_io__open ()
#11 0x000000010009744e in ada__text_io__open ()
#12 0x0000000100023f2f in spark_io__open ()
#13 0x000000010002b7be in sparkmake__openorcreatefile.1909 ()
#14 0x000000010002c083 in _ada_sparkmake ()

so I probaby had some missing file. If the SPARK system itself s
excetion-free, and the RTS makes no use of exceptions internally, maybe
this is worth pursuing .. adds to the difficulties, though.

Re: SPARK

[Yannick Duchêne (Hibou57)]

Le Thu, 20 May 2010 08:21:43 +0200, Simon Wright <simon@pushface.org> a  
écrit:
> Yes; the traceback is
>
> #0  0x00007fff82610886 in __kill ()
> #1  0x00007fff826b0eae in abort ()
> #2  0x00000001000837ce in uw_init_context_1 ()
> #3  0x00000001000838e8 in _Unwind_Backtrace ()
> #4  0x00000001000c8279 in __gnat_backtrace ()
> #5  0x00000001000c42dd in system__traceback__call_chain ()
> #6  0x0000000100088259 in ada__exceptions__call_chain ()
> #7  0x0000000100087a61 in  
> ada__exceptions__exception_propagation__propagate_exceptionXn ()
> #8  0x0000000100088548 in __gnat_raise_nodefer_with_msg ()
> #9  0x00000001000885aa in __gnat_raise_exception ()
> #10 0x00000001000b5b87 in system__file_io__open ()
> #11 0x000000010009744e in ada__text_io__open ()
> #12 0x0000000100023f2f in spark_io__open ()
> #13 0x000000010002b7be in sparkmake__openorcreatefile.1909 ()
> #14 0x000000010002c083 in _ada_sparkmake ()
>
> so I probaby had some missing file. If the SPARK system itself s
> excetion-free, and the RTS makes no use of exceptions internally, maybe
> this is worth pursuing .. adds to the difficulties, though.
SPARK_IO is indeed implemented on top of Ada.Text_IO, which is not under  
control of the SPARK application.

Still wonder why Text_IO fails here, and surprisingly right at startup.  
Requires investigations.

Did you submit this issue to Praxis ? Mac is somewhat popular, pretty sure  
they will be interested in the case.

Re: SPARK

[Simon Wright]

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

> Still wonder why Text_IO fails here, and surprisingly right at
> startup. Requires investigations.

The section that leads to the problem is

      SPARK_IO.Open (File         => Id,
                     Mode_Of_File => Mode,
                     Name_Length  => File.Length,
                     Name_Of_File => Str (File),
                     Form_Of_File => "",
                     Status       => Status);

      if Status = SPARK_IO.Name_Error then
         SPARK_IO.Create (File         => Id,
                          Name_Length  => File.Length,
                          Name_Of_File => Str (File),
                          Form_Of_File => "",
                          Status       => Status);
      end if;

and you can see why exceptions are involved 'under the hood'!

The progress messages from sparkmake were enough to allow me to create
the files concerned (foo.idx, foo.smf) using touch after which sparkmake
was able to update them.

One hopes that GNAT GPL 2010 will run on Snow Leopard! (and of course on
Leopard for those who felt no need to update).