SPARK : third example for Roesetta - reviewers welcome
Yannick Duchêne (Hibou57)
Here is about the third example for Rosetta Code ()
In order to avoid silly error which have bad consequence on SPARK
reputation, as for the first two ones, I assume this may be better to
submit it to interested reviewer.
Now I choosed the one about dicho-search (binary-search).
http://rosettacode.org/wiki/Binary_search
I found this one interesting because 1) it has both a recursive and an
iterative version (the one I prefer) and as SPARK does not support
recursion, I felt this was funny to still be able to overcome this
limitation here with iterative form and show an example of this. 2) This
was the opportunity to post an example with loop assertion, which is a
main topic in SPARK. 3) Last but not least, this task was many order of
magnitude easier than the one to prove A * B will not overflow (see
previous topic in this area).
Here is the one I came to, with questions also for this one :
(for users of GoogleGroups, hope there will not be too much line wrapping,
do not remember the line width there)
with SPARK_IO;
--# inherit SPARK_IO;
--# main_program;
procedure Program
--# global in out
--# SPARK_IO.Outputs;
--# derives
--# SPARK_IO.Outputs from
--# SPARK_IO.Outputs;
is
package Binary_Searchs is
subtype Item_Type is Integer; -- From specs.
subtype Index_Type is Integer range 1 .. 100; -- Arbitrary limits.
type Array_Type is array (Index_Type range <>) of Item_Type;
procedure Search
(Source : in Array_Type;
Item : in Item_Type;
Success : out Boolean;
Position : out Index_Type);
--# derives
--# Success, Position from
--# Source, Item;
--# post
--# (Success -> (Source (Position) = Item)) and
--# ((Source'Length = 0) -> (Success = False));
-- If Success is False, nothing can be said about Position.
end Binary_Searchs;
subtype Index_Type is Binary_Searchs.Index_Type range 1 .. 5;
-- Needed to defined constrained Array_Type.
subtype Array_Type is Binary_Searchs.Array_Type (Index_Type);
-- Needed to pass an array literal to Run_Search (later defined).
-- SPARK does not allow an unconstrained type mark for that purpose.
package body Binary_Searchs is
procedure Search
(Source : in Array_Type;
Item : in Item_Type;
Success : out Boolean;
Position : out Index_Type)
is
Lower : Index_Type; -- Lower bound of Subrange.
Upper : Index_Type; -- Upper bound of Subrange.
Middle : Index_Type; -- Position where Item is tested for.
Terminated : Boolean;
begin
Success := False;
-- Default status updated on success.
Position := Index_Type'First;
-- Default value (required to not a have a data flow error).
if Source'Length > 0 then
Lower := Source'First;
Upper := Source'Last;
Terminated := False;
while not Terminated loop
Middle := (Lower + Upper) / 2;
--# assert
--# (Lower >= Source'First) and -- See below.
--# (Upper <= Source'Last) and -- See below.
--# (Middle >= Lower) and -- Prove Middle in
Source'Range.
--# (Middle <= Upper) and -- Prove Middle in
Source'Range.
--# (Success = False); -- For postcondition.
if Item < Source (Middle) then
if Middle = Lower then
-- No lower subrange.
Terminated := True;
else
--# check Middle > Lower;
-- For the two following proofs.
--# check Middle - 1 >= Lower;
--# check Lower + Middle - 1 >= Lower * 2;
--# check (Lower + Middle - 1) / 2 >= Lower;
-- For "Middle >= Lower" in loop assertion.
--# check Lower < Middle;
--# check Lower + Middle - 1 <= (Middle - 1) * 2;
--# check (Lower + Middle - 1) / 2 <= (Middle - 1);
-- For "Middle <= Upper" in loop assertion.
Upper := Middle - 1;
-- Switch to lower half subrange.
end if;
elsif Item > Source (Middle) then
if Middle = Upper then
-- No upper subrange.
Terminated := True;
else
--# check Middle < Upper;
--# check Upper >= Middle + 1;
--# check Middle + 1 + Upper >= (Middle + 1) * 2;
--# check (Middle + 1 + Upper) / 2 >= (Middle + 1);
-- For "Middle >= Lower" in loop assertion.
--# check Middle + 1 <= Upper;
--# check Middle + 1 + Upper <= Upper * 2;
--# check (Middle + 1 + Upper) / 2 <= Upper;
-- For "Middle <= Upper" in loop assertion.
Lower := Middle + 1;
-- Switch to upper half subrange.
end if;
else
-- Found.
Success := True;
Position := Middle;
Terminated := True;
end if;
end loop;
end if;
end Search;
end Binary_Searchs;
procedure Run_Search
(Source : in Binary_Searchs.Array_Type;
Item : in Binary_Searchs.Item_Type)
--# global in out
--# SPARK_IO.Outputs;
--# derives
--# SPARK_IO.Outputs from
--# SPARK_IO.Outputs, Source, Item;
is
Success : Boolean;
Position : Binary_Searchs.Index_Type;
begin
SPARK_IO.Put_String
(File => SPARK_IO.Standard_Output,
Item => "Searching for ",
Stop => 0);
SPARK_IO.Put_Integer
(File => SPARK_IO.Standard_Output,
Item => Item,
Width => 3,
Base => 10);
SPARK_IO.Put_String
(File => SPARK_IO.Standard_Output,
Item => " in (",
Stop => 0);
-- Open list.
for Source_Index in
Binary_Searchs.Index_Type range Source'Range
loop
--# assert True;
-- No need for an assertion on anything.
SPARK_IO.Put_Integer
(File => SPARK_IO.Standard_Output,
Item => Source_Index,
Width => 3,
Base => 10);
end loop;
SPARK_IO.Put_String
(File => SPARK_IO.Standard_Output,
Item => "): ",
Stop => 0);
-- Close list.
Binary_Searchs.Search
(Source => Source, -- in
Item => Item, -- in
Success => Success, -- out
Position => Position); -- out
case Success is
when True =>
SPARK_IO.Put_String
(File => SPARK_IO.Standard_Output,
Item => "found as #",
Stop => 0);
SPARK_IO.Put_Integer
(File => SPARK_IO.Standard_Output,
Item => Position,
Width => 0, -- Zero, to stick to the sibling '#' sign.
Base => 10);
SPARK_IO.Put_Line
(File => SPARK_IO.Standard_Output,
Item => ".",
Stop => 0);
when False =>
SPARK_IO.Put_Line
(File => SPARK_IO.Standard_Output,
Item => "not found.",
Stop => 0);
end case;
end Run_Search;
begin
SPARK_IO.New_Line (File => SPARK_IO.Standard_Output, Spacing => 1);
Run_Search (Source => Array_Type'(0, 1, 2, 3, 4), Item => 3);
Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 3);
Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 0);
Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 6);
Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 1);
Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 5);
Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 2);
end Program;
Time for questions :
* The test part, that is Run_Search and body of Program takes up to half
of all of the source. Should I remove it or not ?
* In the loop inside of Search there are Check annotations which was not
strictly needed but which I still left for more expressiveness. Is that OK
? Not too much ?
* To keep it simple so far, I have dropped a precondition which I
initially started with and which was requiring the array to be sorted.
This only impact semantic, not runtime check, as any way, the subrange
width always decrease, so that the loop always terminates. Should I or
should I not get it back ?
* I also though about an indirect way to prove the loop always terminates
(although this is not a feature supported by SPARK, there are indirect
ways to achieve this). I though this would look like too much obfuscated
if I add it. Do you agree this would be a bad idea or on the opposite do
you feel this would be an opportunity to show something interesting ?
* If Success (as return by Search) is False then Position is not
guaranteed to mean anything, simply because in such a circumstance, no
postcondition about it applies. I did this way, because I do not know a
way to explicitly state “This is undefined”. Do you know a better way to
express it ? (I could have used a discriminated type for that purpose, but
SPARK disallow this... as you know).
Oops, as last question: I did not understood why, once a time, POGS
returns me two reports for the same single Run_Test procedure, one which
was saying OK and one which was saying False. As there can be only one SIV
file in a given directory, this seemed strange to me. How did he get to
these two different reports at the same time about a single procedure ? Do
you know this issue ? I removed all files, this had been sufficient to
solve the trick.
Yannick Duchêne (Hibou57)
<yannick...@yahoo.fr> a écrit:
As I've posted it here, I was something which was missing:
Success -> (Position in Source'Range)
I am not sure the existing postcondition
Success -> (Source (Position) = Item))
can implies this.
Jeffrey Carter
>
> package Binary_Searchs is
The plural of "search" is "searches".
--
Jeff Carter
"To Err is human, to really screw up, you need C++!"
Stéphane Richard
63
--- news://freenews.netfront.net/ - complaints: ne...@netfront.net ---
Yannick Duchêne (Hibou57)
<spam.jrc...@spam.not.acm.org> a écrit:
> On 08/14/2010 11:17 PM, Yannick Duchêne (Hibou57) wrote:
>>
>> package Binary_Searchs is
>
> The plural of "search" is "searches".
Oh, thanks Jeffrey. SearchEs (will correct it in my source before I post
it to the wiki)
Phil Thornley
On 15 Aug, 07:17, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Here is about the third example for Rosetta Code ()
Some comments first:
> Position := Index_Type'First;
> -- Default value (required to not a have a data flow error).
It's bad practice to put in an unnecessary assignment to get rid of a
flow error. It is much better to structure the code to avoid the flow
error. (They can hide genuine flow errors.) In this case you can get
rid of this one by not defining the variable Middle and using Position
instead - since Position is simply assigned to Middle once a value is
found.
> for Source_Index in
> Binary_Searchs.Index_Type range Source'Range
> loop
> --# assert True;
> -- No need for an assertion on anything.
If you don't need an assertion then don't put one in. If you want to
get rid of the warning about the default assertion then just put
'default_loop_assertions' into your warning file.
> SPARK_IO.Put_Integer
> (File => SPARK_IO.Standard_Output,
> Item => Source_Index,
This line just prints the index - should be Item =>
Source(Source_Index),
> case Success is
> when True =>
A case statement for a Boolean is just a waste of typing. Also I
don't think 'Success' is a good name for this variable as the program
always 'succeeds'. 'Found' would be a more descriptive name and is
more clearly a Boolean term.
> begin
> SPARK_IO.New_Line (File => SPARK_IO.Standard_Output, Spacing => 1);
> Run_Search (Source => Array_Type'(0, 1, 2, 3, 4), Item => 3);
> Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 3);
> Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 0);
> Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 6);
> Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 1);
> Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 5);
> Run_Search (Source => Array_Type'(1, 2, 3, 4, 5), Item => 2);
You might have noticed that error if these tests had been a bit more
diverse!
> * The test part, that is Run_Search and body of Program takes up to half
> of all of the source. Should I remove it or not ?
I don't think so - it seems to be a good idea to provide runable
programs where appropriate.
> * In the loop inside of Search there are Check annotations which was not
> strictly needed but which I still left for more expressiveness. Is that OK
> ? Not too much ?
I prefer user rules to large numbers of check annotations, but YMMV.
> * To keep it simple so far, I have dropped a precondition which I
> initially started with and which was requiring the array to be sorted.
> This only impact semantic, not runtime check, as any way, the subrange
> width always decrease, so that the loop always terminates. Should I or
> should I not get it back ?
See my version below (which requires this precondition).
> * I also though about an indirect way to prove the loop always terminates
> (although this is not a feature supported by SPARK, there are indirect
> ways to achieve this). I though this would look like too much obfuscated
> if I add it. Do you agree this would be a bad idea or on the opposite do
> you feel this would be an opportunity to show something interesting ?
No - keep is as simple as possible (but not simpler...).
> * If Success (as return by Search) is False then Position is not
> guaranteed to mean anything, simply because in such a circumstance, no
> postcondition about it applies. I did this way, because I do not know a
> way to explicitly state “This is undefined”. Do you know a better way to
> express it ? (I could have used a discriminated type for that purpose, but
> SPARK disallow this... as you know).
Strengthening the postcondition is a good idea, and one I've followed
up on, see below...
>
> Oops, as last question: I did not understood why, once a time, POGS
> returns me two reports for the same single Run_Test procedure, one which
> was saying OK and one which
I think you might get this if you get a syntax error from the Examiner
when generating VCs.
I decided that it would more interesting to strengthen the post-
condition to say that 'not Success' means that no element in Source is
equal to Item.
Since this can't be proved without using user rules, I got rid of the
checks for the 'div' calculations and added two rules for these as
well.
I had to introduce a precondition that the Source array is ordered,
otherwise the rules wouldn't work.
(This leaves an unproven VC in Run_Search, but I don't think this is a
big issue.)
This is getting a bit too big to post, so the code and user rules are
in http://www.sparksure.com/resources/Rosetta_Binary_Search.txt
Cheers,
Phil
Yannick Duchêne (Hibou57)
<phil.jp...@gmail.com> a écrit:
>
>> Position := Index_Type'First;
>> -- Default value (required to not a have a data flow error).
> It's bad practice to put in an unnecessary assignment to get rid of a
> flow error. It is much better to structure the code to avoid the flow
> error. (They can hide genuine flow errors.) In this case you can get
> rid of this one by not defining the variable Middle and using Position
> instead - since Position is simply assigned to Middle once a value is
> found.
may be for two bad reasons (will have to be checked) : first may be I did
useless "optimization" (do not know how good compilers handle this), and
then, I though this may be better if ever the context may have some kind
of tasking. About the latter, I will have to check if weither or not an
out value is supposed to be updated only when the method exit or is
possibly updated outside while the method is running.
>> for Source_Index in
>> Binary_Searchs.Index_Type range Source'Range
>> loop
>> --# assert True;
>> -- No need for an assertion on anything.
> If you don't need an assertion then don't put one in. If you want to
> get rid of the warning about the default assertion then just put
> 'default_loop_assertions' into your warning file.
I was wondering about reader which may try the example as-is. As was
"afraid" to think someone may try it and see that "unexpected" message
from the Examiner. Or may be there is a place some kind of more
useful-looking assertion here instead of a dummy one ?
OTH, while I thinking about your comment, I cannot avoid this though:
after all, if a loop assertion is really missing, this inevitably ends up
into undischarged Validation Conditions. So in some sense, this warning is
useless, because 1) when it is meaningful, it is redundant with later
reports of undischarged VC 2) if this does not ends into undischarged VC,
this is not meaningful. So, this is either not meaningful either
redundant. May be this is disabled by default in the Examiner's builtin
options ?
... I still wonder about readers who may get this warning without this.
But for Real Use, I agree with you, the idea of disabling this warning is
indeed good.
>> SPARK_IO.Put_Integer
>> (File => SPARK_IO.Standard_Output,
>> Item => Source_Index,
> This line just prints the index - should be Item =>
> Source(Source_Index),
Don't mind for this one Phil, this was a transient modification which
occurs at the same time I was posting this here (I did both thing at the
time and did not notice I was posting an error). The one at Rosetta do
Source (Source_Index); it was corrected in the afternoon (local time, lol).
>> case Success is
>> when True =>
> A case statement for a Boolean is just a waste of typing. Also I
> don't think 'Success' is a good name for this variable as the program
> always 'succeeds'. 'Found' would be a more descriptive name and is
> more clearly a Boolean term.
Mmmh, your informal argument makes me think this may be matter of taste
this one, both for case and name. However, will think about it. Well, you
may be right for Success vs Found ; will change it ; except for Case
Statement which I do not wish to change for the time. I have reasons for
that, but don't want to argue about it here (to not obfuscate the topic,
... will just say, to keep it simple, I don't enjoy the “else” branches of
"if-then" constructs... I call it “the mute branch”).
>> * The test part, that is Run_Search and body of Program takes up to
>> half of all of the source. Should I remove it or not ?
> I don't think so - it seems to be a good idea to provide runable
> programs where appropriate.
OK. As there was a doubt in my mind about it, I added a comment suggesting
to focus only on the relevant part. So I may remove it. Will have this in
mind for future example.
>> * In the loop inside of Search there are Check annotations which was
>> not strictly needed but which I still left for more expressiveness. Is
>> that OK ? Not too much ?
> I prefer user rules to large numbers of check annotations, but YMMV.
I don't want to introduce user rules at Rosetta, because don't think this
is the place for such none-straight-way things.
About Real Use, this is another topic.
>> * To keep it simple so far, I have dropped a precondition which I
>> initially started with and which was requiring the array to be sorted.
>> This only impact semantic, not runtime check, as any way, the subrange
>> width always decrease, so that the loop always terminates. Should I or
>> should I not get it back ?
> See my version below (which requires this precondition).
OK. Will see right after (I reply as I read)
>> * I also though about an indirect way to prove the loop always
>> terminates
>> (although this is not a feature supported by SPARK, there are indirect
>> ways to achieve this). I though this would look like too much obfuscated
>> if I add it. Do you agree this would be a bad idea or on the opposite do
>> you feel this would be an opportunity to show something interesting ?
> No - keep is as simple as possible (but not simpler...).
>> * If Success (as return by Search) is False then Position is not
>> guaranteed to mean anything, simply because in such a circumstance, no
>> postcondition about it applies. I did this way, because I do not know a
>> way to explicitly state “This is undefined”. Do you know a better way
>> to express it ? (I could have used a discriminated type for that
>> purpose, but SPARK disallow this... as you know).
> Strengthening the postcondition is a good idea, and one I've followed
> up on, see below...
>> Oops, as last question: I did not understood why, once a time, POGS
>> returns me two reports for the same single Run_Test procedure, one
>> which was saying OK and one which
> I think you might get this if you get a syntax error from the Examiner
> when generating VCs.
And this could end into two SIV files in the same folder for the same
procedure ?
> I decided that it would more interesting to strengthen the post-
> condition to say that 'not Success' means that no element in Source is
> equal to Item.
May be I see. This suggest the most typical or expected result is Found,
instead of not Found, and so you are focusing on the consequence of not
Found, which are more likely to need care.
> Since this can't be proved without using user rules, I got rid of the
> checks for the 'div' calculations and added two rules for these as
> well.
>
> I had to introduce a precondition that the Source array is ordered,
> otherwise the rules wouldn't work.
> (This leaves an unproven VC in Run_Search, but I don't think this is a
> big issue.)
>
> This is getting a bit too big to post, so the code and user rules are
> in http://www.sparksure.com/resources/Rosetta_Binary_Search.txt
OK. The cool stuff to read is there :)
I enjoy your contribution, with the one of Jeffrey too. I was pleased.
Well, well, now time to read your version. "See" you soon.
--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
Yannick Duchêne (Hibou57)
> condition to say that 'not Success' means that no element in Source is
> equal to Item.
After I have read this, it is more clear :
> --# post (Found -> (Source (Position) = Item)) and
> --# (not Found ->
> --# (for all I in Index_Type range Source'First .. Source'Last
> --# => (Source(I) /= Item)));
This is indeed a more strong/strengthened postcondition than mine. To talk
with a word I like : this is more expressive.
> --# assert not Terminated and
> --# Lower >= Source'First and
> --# Upper <= Source'Last and
> --# Position >= Lower and
> --# Position <= Upper and
> --# not Found and
> --# (Lower > Source'First -> Source(Lower - 1) < Item) and
> --# (Upper < Source'Last -> Source(Upper + 1) > Item);
Interesting to study: you could move all in the loop assertion.
(I am still going on with reading)
Jacob Sparre Andersen
> http://rosettacode.org/wiki/Binary_search
> subtype Item_Type is Integer; -- From specs.
No need to introduce a subtype here. Just use "Integer" as the element
type, or introduce a new type with explicit ranges (just to show how
easy it is).
> subtype Index_Type is Integer range 1 .. 100; -- Arbitrary limits.
Is there really any need to make this a subtype of Integer? Shouldn't
it rather be a completely independent type:
type Index_Type is range 1 .. 100;
> procedure Search
> (Source : in Array_Type;
> Item : in Item_Type;
> Success : out Boolean;
> Position : out Index_Type);
> --# derives
> --# Success, Position from
> --# Source, Item;
> --# post
> --# (Success -> (Source (Position) = Item)) and
> --# ((Source'Length = 0) -> (Success = False));
> -- If Success is False, nothing can be said about Position.
Shouldn't the preconditions include that Source is ordered? (How do you
write that in SPARK?)
The procedure Search should be placed in a package of its own (in theory
it is reusable), and the demonstration program should be a library level
procedure. There is no reason to make the example code more complicated
than that.
Greetings,
Jacob
--
"... but it was, on the other hand, very good at being a slow
and dim-witted pupil."
"I had no idea they were supposed to be in short supply"
Yannick Duchêne (Hibou57)
> else
> -- Switch to lower half subrange.
> Upper := Position - 1;
> Position := (Lower + Upper) / 2; -- <<<
> end if;
>-- [...]
>else
> -- For "Middle <= Upper" in loop assertion.
> -- Switch to upper half subrange.
> Lower := Position + 1;
> Position := (Lower + Upper) / 2; -- <<<
> end if;
Interesting to note: you moved “Position := (Lower + Upper) / 2;” inside
logical branch, I suppose to ease prove, as the instruction is right in a
context which makes its validity more obvious. This is indeed better than
the idea of the factorization I used.
This topic makes me think about the latter about the Middle variable
turned into a direct use of Position. May be I did "automatic useless
optimization" here.
That is funny, because it happens I do the same (that is why I suppose I
was not so good here due to a kind of "inappropriate automation").
Phil Thornley
wrote:
[...]
> I don't want to introduce user rules at Rosetta, because don't think this
> is the place for such none-straight-way things.
I agree that introducing different combinations of files to Rosetta
for different examples could be quite confusing for the casual browser
of the site.
Perhaps we need two different languages: SPARK and SPARK+Proof where
the SPARK examples just include the (now normal) proof of absence of
run-time error and the +Proof versions include partial proofs of
correctness.
Would that be a problem for the Rosetta code site?
What do others think?
Cheers,
Phil
Yannick Duchêne (Hibou57)
Le Sun, 15 Aug 2010 22:04:26 +0200, Jacob Sparre Andersen <spa...@nbi.dk>
a écrit:
>> http://rosettacode.org/wiki/Binary_search
>
>> subtype Item_Type is Integer; -- From specs.
>
> No need to introduce a subtype here. Just use "Integer" as the element
> type, or introduce a new type with explicit ranges (just to show how
> easy it is).
The idea was to give a proper name expressing a purpose (I like to start
to name thing).
Well, your idea of "show how easy it is" could be balanced. However, I
have not clear idea about it. Would be nice to know how it is perceived.
On the other hand, if the purpose of the sorted list is to be general
purpose or even more, precisely to sort Integer, namely, this could be
indeed an option.
May be Phil or Jeffrey will have something to state here.
>> subtype Index_Type is Integer range 1 .. 100; -- Arbitrary limits.
>
> Is there really any need to make this a subtype of Integer? Shouldn't
> it rather be a completely independent type:
>
> type Index_Type is range 1 .. 100;
This was rightly to simplify thing (I say "rightly", because you moved it
in front above). This was avoiding the need to
have some conversion to Integer.
> Shouldn't the preconditions include that Source is ordered?
That was a topic indeed. Phil and I talked about it in this same thread. I
first had the idea to express it, but later removed it.
> (How do you write that in SPARK?)
I did it this way (before I removed it):
--# pre
--# (Source'Length = 0) or else
--# (for all I in Index_Type range Source'First .. Source'Last - 1
--# => (Source (I) <= Source (I + 1)));
-- The array must be either empty or sorted from lower to higher.
Phil did it another way (using an abstract function, if that is the good
word, i am not sure about the proper way to name it).
> The procedure Search should be placed in a package of its own (in theory
> it is reusable), and the demonstration program should be a library level
> procedure. There is no reason to make the example code more complicated
> than that.
Yes, that was silly after all. I will split it into proper spec, body and
program, this is indeed strongly advised to expose a good example. You are
right. I did it this way because I always write test program in a single
file (and thus declaring package spec and body in the declarative part of
the main procedure). Will change it later when I will be finished with
reading Phil's version of the implementation and specs.
Yannick Duchêne (Hibou57)
<phil.jp...@gmail.com> a écrit:
> in http://www.sparksure.com/resources/Rosetta_Binary_Search.txt
I saw something wrong in this version. But I will expose it later, as I
want to run some experiencing before. I will merge some of the things
you've introduced, but only what will produce a version with no
undischarged VC and no user rules (may be feasible) and will do the
structural update Sparre suggested. Looking at it for tonight and will do
the update at Rosetta tomorrow.
Jeffrey Carter
>
> --# pre
> --# (Source'Length = 0) or else
> --# (for all I in Index_Type range Source'First .. Source'Last - 1
> --# => (Source (I) <= Source (I + 1)));
> -- The array must be either empty or sorted from lower to higher.
Is this correct? Consider the case where Source'Length = 1. In that case, the
range in the "for all" is null; does that evaluate to True? If not, then it
needs to be
Source'Length < 2 or else (for all ...)
Even if it is correct as written, it may be misleading to non-Ada readers (whom
we want to impress on Rosetta) who might think it implies an out-of-range access.
--
Jeff Carter
"Son of a window-dresser."
Monty Python & the Holy Grail
12
Jeffrey Carter
>
>> * In the loop inside of Search there are Check annotations which was not
>> strictly needed but which I still left for more expressiveness. Is that OK
>> ? Not too much ?
> I prefer user rules to large numbers of check annotations, but YMMV.
The large number of Check annotations seems to my untrained eye an unusual way
to use SPARK. As a comparison, the Tokeneer "core" code is 34769 LOC and
contains 27 Check annotations, a much lower ratio of Check/LOC. Is this a good
way to present SPARK on Rosetta?
Yannick Duchêne (Hibou57)
<spam.jrc...@spam.not.acm.org> a écrit:
>> --# pre
>> --# (Source'Length = 0) or else
>> --# (for all I in Index_Type range Source'First .. Source'Last - 1
>> --# => (Source (I) <= Source (I + 1)));
>> -- The array must be either empty or sorted from lower to higher.
>
> Is this correct?
No, indeed, this is not. For the reason you noticed. I removed it too much
soon to have an opportunity to see it. This is not a matter of “correct as
written”, this is logically incorrect.
Yannick Duchêne (Hibou57)
<yannick...@yahoo.fr> a écrit:
> I saw something wrong in this version.
in SPARK. But I don't really enjoy the lack of a test for the empty array
case, as a SPARK program is always a valid Ada program, and may be
compiled ignoring any SPARK error as well. This is perfectly possible to
compile this passing Search an empty array. I would prefer SPARK allow
empty array, and thus end into the creation of more robust units.
So whatever SPARK says about it, I will get back the test for the empty
array case.
Yannick Duchêne (Hibou57)
<spam.jrc...@spam.not.acm.org> a écrit:
> The large number of Check annotations seems to my untrained eye an
> unusual way to use SPARK. As a comparison, the Tokeneer "core" code is
> 34769 LOC and contains 27 Check annotations, a much lower ratio of
> Check/LOC. Is this a good way to present SPARK on Rosetta?
hide it in user rules. The reason why I do not like it, is because you do
not see the proofs any more (or great part of it are missing), this is not
any more part of the source. Proofs should come with the implementation. I
cannot dissociate both.
May be a matter if personality also.
> Is this a good way to present SPARK on Rosetta?
Rightly, at this place, this is moreover a special case: better to show
what annotations are than to hide it. People aware of SPARK may guess
implicit parts... other users will not. So better show it explicitly (as
long as the target is to explain what formal validation means with
interpretable examples).
At least, I feel it this way. Tell about your comments.
Phil Thornley
wrote:
> On 08/15/2010 01:19 PM, Yannick Duchêne (Hibou57) wrote:
>
> > --# pre
> > --# (Source'Length = 0) or else
> > --# (for all I in Index_Type range Source'First .. Source'Last - 1
> > --# => (Source (I) <= Source (I + 1)));
> > -- The array must be either empty or sorted from lower to higher.
>
> Is this correct? Consider the case where Source'Length = 1. In that case, the
> range in the "for all" is null; does that evaluate to True? If not, then it
> needs to be
>
> Source'Length < 2 or else (for all ...)
That's the correct way of saying that the array is ordered, and it
works fine for an array of Length 1 (or less).
The translation of that expression to FDL (the language SPARK uses for
all it's proof work) will be something like:
for_all(i_ : integer, source__first <= i_ and i_ <= source__last - 1
-> (element(source, [i_]) <= element(source, [i_ + 1]))) .
If source__first = source__last then the LHS of the implication is
False, and the implication itself is True.
> Even if it is correct as written, it may be misleading to non-Ada readers (whom
> we want to impress on Rosetta) who might think it implies an out-of-range access.
That's why I used the proof function 'Ordered' in my version of the
code. To the casual reader it should look OK, and when you want to
get more formal then you define Ordered as exactly that expression
above.
Cheers,
Phil
Phil Thornley
wrote:
> On 08/15/2010 11:42 AM, Phil Thornley wrote:
>
>
>
> >> * In the loop inside of Search there are Check annotations which was not
> >> strictly needed but which I still left for more expressiveness. Is that OK
> >> ? Not too much ?
> > I prefer user rules to large numbers of check annotations, but YMMV.
>
> The large number of Check annotations seems to my untrained eye an unusual way
> to use SPARK. As a comparison, the Tokeneer "core" code is 34769 LOC and
> contains 27 Check annotations, a much lower ratio of Check/LOC. Is this a good
> way to present SPARK on Rosetta?
It is certainly unusual (I worked on the proofs for a program of
150,000 lines and there was just 1 check annotation), and I agree that
it may put readers off.
I think that it is just about acceptable if it avoids creating *any*
user rules (because adding these rules to the source might also put
people off).
However it is likely that most other examples won't have this problem
- integer division (which causes the problems here) is an area where
the Simplifier needs a lot of help either by check annotations or user
rules.
If Yannick wants to keep them then perhaps he could add some comments
to the program description saying that this use of check annotations
is unusual.
Cheers,
Phil
Phil Thornley
wrote:
> There is no Magic here, what you do not have in Check annotations, you
> hide it in user rules. The reason why I do not like it, is because you do
> not see the proofs any more (or great part of it are missing), this is not
> any more part of the source. Proofs should come with the implementation. I
> cannot dissociate both.
User rules are as formal or as informal as you choose to make them.
In my version of this example I have some user rules with informal
justifications - eg:
/*---------------------------------------------------------
-- Rule 1:
-- Justification:
-- X + Y >= 2*X, so (X + Y) div 2 >= X.
---------------------------------------------------------*/
binary_search_rule(1): (X + Y) div 2 >= X
may_be_deduced_from
[ X <= Y,
X >= 1,
Y >= 1] .
/*---------------------------------------------------------
-- Rule 2:
-- Justification:
-- X + Y <= 2*Y, so (X + Y) div 2 <= Y.
---------------------------------------------------------*/
binary_search_rule(2): (X + Y) div 2 <= Y
may_be_deduced_from
[ X <= Y,
X >= 1,
Y >= 1] .
if you need more formality then first define a couple of integer
variables x and y in a .fdl file:
title procedure search_rules:
var x, y : integer;
end;
then prove the following VC using the Proof Checker:
search_rules_1.
H1: x <= y .
H2: x >= 1 .
H3: y >= 1 .
->
C1: (x + y) div 2 >= x .
C2: (x + y) div 2 <= y .
The only manual step in this is the translation of the rule to the VC
- and so long as you use the same names with just the case changed (X -
> x) and layout the VC similarly to the rule this step is very easy to
validate manually.
Cheers,
Phil
Phil Thornley
wrote:
> Le Sun, 15 Aug 2010 22:57:21 +0200, Yannick Duchêne (Hibou57)
>
> Half false alarm, half True alarm: there is not way to have an empty array
> in SPARK. But I don't really enjoy the lack of a test for the empty array
> case, as a SPARK program is always a valid Ada program, and may be
> compiled ignoring any SPARK error as well. This is perfectly possible to
> compile this passing Search an empty array. I would prefer SPARK allow
> empty array, and thus end into the creation of more robust units.
>
> So whatever SPARK says about it, I will get back the test for the empty
> array case.
But if you put that test back in you are going to get flow errors for
the added path - because Position will be exported but no value will
be assigned to it.
There's an interesting general point here - the 'SPARK' assumption is
that the complete program is SPARK, so an empty array can't happen (it
would require a index subtype with 'First > 'Last, which is a semantic
error).
However, if we start to see individual packages being put into the
public domain then the calling program could well be just Ada, so an
empty array becomes a possibility.
My personal view is against changing the code of SPARK operations to
handle non-SPARK constructs, because it will cause all sorts of
problems (like the flow error in this case).
For the examples in Rosetta Code we should just state that assumption
in the accompanying text, since these code samples are for
demonstrating language features rather than providing a source code
library.
But there is still a problem in the real world. Perhaps what is needed
is an 'Ada to SPARK' interface to check for violations. One
possiblity would be for the SPARK operation to become internal to the
package and the body of the visible operation to check that the array
is non-null and only call the internal operation if it's OK (the code
of that operation will probably have to be hidden from the Examiner).
Cheers,
Phil
Stephen Leake
The user rules are part of the SPARK source. The file names may not end
in .ad?, but they are still source.
Is there a way to get the Rosetta website to make that clear?
--
-- Stephe
Phil Thornley
wrote:
[...]
>
> The user rules are part of the SPARK source. The file names may not end
> in .ad?, but they are still source.
>
> Is there a way to get the Rosetta website to make that clear?
It appears to be very simple (although I haven't tried to do anything
yet). The entry for a language consists of blocks (of text in any
format, although it does keyword colouring for known languages) that
can be called 'source' interspersed with any other text that can
explain the contents of the 'source' blocks.
So there's no problem adding user rules, just the question of whether
that is a good idea or not.
Cheers,
Phil
Jacob Sparre Andersen
> Yannick Duchęne wrote:
>> I don't want to introduce user rules at Rosetta, because don't think
>> this is the place for such none-straight-way things.
>
> I agree that introducing different combinations of files to Rosetta
> for different examples could be quite confusing for the casual browser
> of the site.
Yes.
But if user rules is The Right Way(tm) to solve a problem, then user
rules should be included.
> Perhaps we need two different languages: SPARK and SPARK+Proof where
> the SPARK examples just include the (now normal) proof of absence of
> run-time error and the +Proof versions include partial proofs of
> correctness.
I don't think so, but we should put instructions for compiling a SPARK
program with user rules somewhere (easily findable) on the Rosetta code
site.
Greetings,
Jacob
--
"This page inadvertently left blank."
Yannick Duchêne (Hibou57)
<phil.jp...@gmail.com> a écrit:
> But if you put that test back in you are going to get flow errors for
> the added path - because Position will be exported but no value will
> be assigned to it.
> For the examples in Rosetta Code we should just state that assumption
> in the accompanying text, since these code samples are for
> demonstrating language features rather than providing a source code
> library.
Good point for that case! Thanks
In the real world now: I understand your point about what a SPARK program
is really. But do you see a reason why SPARK should disallow defensive
programming ? (forget about the suggestion to handle empty array in SPARK,
this was silly, but defensive programming may not be)
Yannick Duchêne (Hibou57)
<phil.jp...@gmail.com> a écrit:
> It appears to be very simple (although I haven't tried to do anything
> yet). The entry for a language consists of blocks (of text in any
> format, although it does keyword colouring for known languages) that
> can be called 'source' interspersed with any other text that can
> explain the contents of the 'source' blocks.
>
> So there's no problem adding user rules, just the question of whether
> that is a good idea or not.
files would make it look more like a tool than a language, or at least not
as easy to track as any other language. Separation of spec and body in one
common thing, adding a third file while examples show proofs can also
appears in source as well, would be strange (sometime here, sometime
there). Moreover, don't forget that SPARK and its annotation are a
language, and Praxis Examiner/Simplifier are a particular implementation
of SPARK. The only one at the time, I know, but still a particular
implementation. User rules are by the way not even described in the SPARK
LRM.
Just to compare, I did not saw any kind of external resource files at this
wiki.
If at least if this could be located in the same directory as the
source... but this have to be located at some place which depends on some
SPARK configuration.
Yannick Duchêne (Hibou57)
<phil.jp...@gmail.com> a écrit:
> It is certainly unusual (I worked on the proofs for a program of
> 150,000 lines and there was just 1 check annotation), and I agree that
> it may put readers off.
other hand, look at the SPARK introduction at WikiPedia, it talks about
check/assert annotations, no where it talks about user rules. The SPARK
LRM talks about annotations, no of very few about user rules. Whenever you
see an introduction about SPARK, it is said to be an Ada subset with
annotations. And indeed, notations are there.
Do you see the point ?
May there are two very different way to work with SPARK so. This will not
ease things...
Would be difficult to explain (and to me to) that what is so much focused
on, just appears in very cases. So why annotations and so much spots on it
?
Mark Lorenzen
<yannick_duch...@yahoo.fr> wrote:
ks
>
> In the real world now: I understand your point about what a SPARK program
> is really. But do you see a reason why SPARK should disallow defensive
> programming ? (forget about the suggestion to handle empty array in SPARK,
> this was silly, but defensive programming may not be)
Defensive programming can cause problems when trying to obtain 100%
test coverage. This is of course especially true, when the defensive
parts cover situations "that can never occur". How do you trigger
these situations? Using preconditions (or e.g. more restricted ranges)
as has already been suggested, can eliminate a surprising number of
cases where defensive programming would typically be used in non-SPARK
code.
- Mark L
Phil Thornley
wrote:
[...]
> > The procedure Search should be placed in a package of its own (in theory
> > it is reusable), and the demonstration program should be a library level
> > procedure. There is no reason to make the example code more complicated
> > than that.
>
> Yes, that was silly after all. I will split it into proper spec, body and
> program, this is indeed strongly advised to expose a good example.
I don't think that further discussion about the best way to code this
example is going to achieve much.
So, Yannick, if you do this split of the package and the main (test)
program into two separate units then I will add the alternative
implementation of the package. It will need some careful explanations
of what it all means but that seems to be the best way forward at
present.
Then once I've put something up we can get opinions on how to proceed
further.
Cheers,
Phil
Peter C. Chapin
> My personal opinion about user rules kept apart, my fear is that
> external files would make it look more like a tool than a language, or
> at least not as easy to track as any other language.
In many respects SPARK is not like other languages. The nature of what
it's trying to do is such that these extra supporting files are
sometimes necessary. My feeling is that you should demonstrate
reasonable SPARK style. If it is felt that user rules are appropriate in
this case, then so be it. If the reader of the Rosetta site is put off
by the extra complexity, perhaps they would be more interested in the
Python examples. :)
(No disrespect to Python intended)
Peter
Yannick Duchêne (Hibou57)
écrit:
> In many respects SPARK is not like other languages.
> The nature of what
> it's trying to do is such that these extra supporting files are
> sometimes necessary. My feeling is that you should demonstrate
> reasonable SPARK style. If it is felt that user rules are appropriate in
> this case, then so be it. If the reader of the Rosetta site is put off
> by the extra complexity, perhaps they would be more interested in the
> Python examples. :)
That's not only about users of Rosetta which would be supposed not clever
enough to understand it, that's about usability any one else (at least
some ones else). You cannot make the assumption that if someone feel this
is somewhat scattered, then this one is just not versed enough to
understand how good it is.
What I wanted to underline is this:
1) Why to present SPARK as an annotated subset of Ada if it is not the way
it is to be used ? (either all these documents about it should be revised
or this point reviewed... the latter being unlikely to occur I feel).
2) If the user rule files are of a so big importance (Phil talked about
tens of thousands of lines of Ada source with a single check annotation),
so why to move them at the place where "builded" files belongs ? (just
like if Ada package was to be put in the object/exe build directory). Is
it the intended location of what is supposed to be a language source ?
3) User rules are written in another other totally different language. So
a third unavoidable language comes into the place. This is not tiny affair.
Excuse me, but with due respect to you and Phil, I see no way to turn this
into anything clear.
May be this is an effect of SPARK to few widely used (Ada being sadly
already few than others, that's even more true with SPARK) which may have
turned into the lack of some practical consideration. Sure these points
are not there to help or to make people feel this is an Ada derived
language with formal capabilities added. Why not promote Windows resource
files as C derived language sources so ? And to present things one way,
while this is another way, do you feel that is clear or (even honest) ?
« Je tombe des nues » as says a french expression.
For the time, unless some news comes in the place, I will end with this
conclusion: SPARK's not a language, that's Praxis's tool. So why speak
about it as a language, while a language is something which is clearly not
use or managed this way as a tool ?
By the way, if this is really a Praxis's tool as I suppose now, do I have
to understand there will be always one single implementation of SPARK and
a single provider in this area ?
That is important too, and another difference with what a language is, how
it is used and how it lives.
P.S. I have not updated the example unlike I said I will do today, because
my mind is totally unclear about the topic now. Just you reply makes me
think I had to tell my though. If you or Phil want to change it, feel free
and just do. I probably will not before I will have a back-clear idea of
all of this.
P.P.S Forgive for the hard intonation of my reply, this is just that SPARK
is an important topic for me, the kind of thing I was dreaming about for
long (from the start when I first discovered MS QBasic in Windows 3.1), so
this trickery does not really make feel at rest.
Peter C. Chapin
> That's not only about users of Rosetta which would be supposed not
> clever enough to understand it, that's about usability any one else (at
> least some ones else). You cannot make the assumption that if someone
> feel this is somewhat scattered, then this one is just not versed enough
> to understand how good it is.
I didn't mean to imply that Rosetta users (or Python users) are
unintelligent. If my comment came across that way, I apologize. My point
was that a person who places a high value in conciseness in programming
language design (such as many advocates of dynamic languages) is
probably not going to be very impressed with SPARK no matter what you
do. Adding an extra rules file (or not) isn't going to matter to such a
person.
> For the time, unless some news comes in the place, I will end with this
> conclusion: SPARK's not a language, that's Praxis's tool.
When people ask me what SPARK is about I tell them it's an annotated
subset of Ada together with a tool set that can be used for deep static
analysis of that annotated language. It seems to me that SPARK is both a
language and a tool.
Perhaps this gets back to a question Phil raised: does it make sense on
Rosetta to differentiate between SPARK and SPARK+proofs?
In principle the issue comes up with other languages too. C is not much
use without a C compiler (a tool). It is true that you can write a C
program in isolation. However, the legality of the program is enforced
by a tool. If a SPARK compiler existed as a single program that took
SPARK source to object code, it would combine the functionality of, at
least, the Examiner and a partial Ada compiler. I suppose it could also
contain the functionality of the simplifier as well. Would that make all
of that functionality part of the SPARK language? If you created an Ada
compiler that split semantic analysis into a separate executable would
that make the semantic checks "just a tool?"
I suppose to really distinguish between language and tool you need to
examine the specification of SPARK. Just as the Ada standard defines the
Ada language the SPARK "standard" would define the SPARK language. Any
additional features would be added by tools.
> By the way, if this is really a Praxis's tool as I suppose now, do I
> have to understand there will be always one single implementation of
> SPARK and a single provider in this area ?
That's an interesting question.
Oracle is suing Google over Google's use of Java in Android. I suppose
this is the nasty quagmire one gets into whenever one starts using
proprietary languages. Thankfully Ada has an international standard so
the Ada community can avoid some of that. However, there is no
international standard for SPARK. At least not as far as I know. Will it
become the Java of the formal methods community?
Peter
Stephen Leake
Of course it is; the point of the web site is to demonstrate how to
solve problems in various languages. The SPARK language includes user
rules; the problem is not solved without them.
I thought the question was whether to use user rules in a non-Ada file,
or Checks as SPARK annotations in an Ada file. Either way, they are an
important part of the solution.
--
-- Stephe
Jacob Sparre Andersen
> Peter C. Chapin wrote:
>> The nature of what it's trying to do is such that these extra
>> supporting files are sometimes necessary. My feeling is that you
>> should demonstrate reasonable SPARK style.
Agreed.
But Yannick is correct that it is a problem, if we need to include
compiler specific files in our examples.
I decided not to include a GNAT project file with my "Fork" example for
Ada, since that's a compiler specific file. But this means that new
users may find it difficult to get the example to work. Should I rather
include compiler specific files and instructions on how to compile the
program examples?
> 1) Why to present SPARK as an annotated subset of Ada if it is not the
> way it is to be used ? (either all these documents about it should be
> revised or this point reviewed... the latter being unlikely to occur I
> feel).
The problem is that the compiler you are using isn't intelligent enough
to compile your programs without some assistance. Whether that
assistance is a project file with compiler and linker flags, or hints on
how to prove some hypotheses.
> 2) If the user rule files are of a so big importance (Phil talked
> about tens of thousands of lines of Ada source with a single check
> annotation), so why to move them at the place where "builded" files
> belongs ? (just like if Ada package was to be put in the object/exe
> build directory). Is it the intended location of what is supposed to
> be a language source ?
User rules is a kind of compiler configuration. I generally keep
compiler configuration files as a part individual of projects (like
source text).
> 3) User rules are written in another other totally different
> language. So a third unavoidable language comes into the place. This
> is not tiny affair.
Just like GNAT project files.
> For the time, unless some news comes in the place, I will end with
> this conclusion: SPARK's not a language, that's Praxis's tool.
I would say that it is a programming language with only one existing
compiler. I am quite sure that Praxis would be happy (but also a bit
annoyed ;-) if the market was big enough that another company found it
worth creating a competing SPARK compiler.
If I decided to compete with Praxis, I would probably make the abilities
of the theorem prover an area where I would try to make a difference.
Another difference could be integration of the complete compiler tool
chain.
> By the way, if this is really a Praxis's tool as I suppose now, do I
> have to understand there will be always one single implementation of
> SPARK and a single provider in this area ?
I can't see anything but resources (i.e. commercial viability)
preventing the existence of a competing SPARK compiler. Since the
Praxis implementation of SPARK is distributed under the GNU GPL, you can
always start by forking that implementation.
Greetings,
Jacob
--
"It ain't rocket science!"
Phil Thornley
> On 2010-08-16 18:38, Yannick Duchêne (Hibou57) wrote:
>
> > For the time, unless some news comes in the place, I will end with this
> > conclusion: SPARK's not a language, that's Praxis's tool.
>
> When people ask me what SPARK is about I tell them it's an annotated
> subset of Ada together with a tool set that can be used for deep static
> analysis of that annotated language. It seems to me that SPARK is both a
> language and a tool.
>
> Perhaps this gets back to a question Phil raised: does it make sense on
> Rosetta to differentiate between SPARK and SPARK+proofs?
not a good idea - using SPARK is much more of a continuum of
approaches.
[Which is a Very Good Thing(TM) - new users can start by ignoring
proof completely. Then start proving that the code is type safe
without having to even think about formal specifications - and
complete their type safety proofs ranging from the completely informal
(proof by review) up to the completely formal (check annotations,
where they work, and the Proof Checker otherwise). Then move into the
formal spec world of contracts expressed through pre and post
conditions.]
I'm going to try and come up with an explanation of SPARK for Rosetta
Code that covers all the ground, but is as succinct as possible (so no-
one should be holding their breath for that). I'll link out to
detailed descriptions where possible.
[...]
> > By the way, if this is really a Praxis's tool as I suppose now, do I
> > have to understand there will be always one single implementation of
> > SPARK and a single provider in this area ?
>
> That's an interesting question.
>
> Oracle is suing Google over Google's use of Java in Android. I suppose
> this is the nasty quagmire one gets into whenever one starts using
> proprietary languages. Thankfully Ada has an international standard so
> the Ada community can avoid some of that. However, there is no
> international standard for SPARK. At least not as far as I know.
That was one of the first questions that the Annex H Rapporteur Group
looked at when it was formed following the publication of the Ada95
standard. Should the Group define a 'safe subset' for Ada and, if so,
should that subset be SPARK? The Group fairly quickly decided against
defining a standard subset so the question about SPARK never arose.
The tools are now GPL'ed, but the documentation is all copyright
Altran-Praxis and the SPARK LRM is also Crown Copyright (probably
after some early funding from the UK MoD). I don't know enough about
these issues to say what effect that has on restricting other
organisations' ability to develop new versions of the language and
tools.
> ... Will it become the Java of the formal methods community?
Not until Altran-Praxis start making a great deal more money out of it
than they do at present.
Cheers,
Phil
Peter C. Chapin
> I've thought about that one a bit more and decided that it's probably
> not a good idea - using SPARK is much more of a continuum of
> approaches.
I've noticed this as well and I agree that it is a good thing. Sometimes
I use SPARK to try an prove quite a bit. Sometimes I just try to prove
freedom from run time errors. Sometimes I just use the flow analysis and
stop there. All of these options get followed at different places in the
same program depending on time, effort required, criticality, etc.
I suppose it's the same with any kind of analysis tool and it's
reflective of the tool-like nature of SPARK.
>> However, there is no
>> international standard for SPARK. At least not as far as I know.
>
> That was one of the first questions that the Annex H Rapporteur Group
> looked at when it was formed following the publication of the Ada95
> standard. Should the Group define a 'safe subset' for Ada and, if so,
> should that subset be SPARK? The Group fairly quickly decided against
> defining a standard subset so the question about SPARK never arose.
That's interesting to know.
I can see why the group did not want standardize a safe subset. After
all many different subsets could be imagined and what constitutes "safe"
is going to depend on the application and on the analysis technology
available. As I understand it SPARK has evolved as analysis techniques
have improved. It will probably continue to do so. Other, similar
systems with slightly different needs could potentially exist using
different subsets as well.
>> ... Will it become the Java of the formal methods community?
>
> Not until Altran-Praxis start making a great deal more money out of it
> than they do at present.
I'm not really worried about it. Still it would be great if interest in
SPARK or SPARK-like systems became so widespread that people did start
worrying about it!
Peter
Simon Wright
> I can't see anything but resources (i.e. commercial viability)
> preventing the existence of a competing SPARK compiler. Since the
> Praxis implementation of SPARK is distributed under the GNU GPL, you
> can always start by forking that implementation.
Following on from discussions in another thread, I propose the name
SPlint for this fork.
Phil Thornley
> I'm going to try and come up with an explanation of SPARK for Rosetta
> Code that covers all the ground, but is as succinct as possible (so no-
> one should be holding their breath for that). I'll link out to
> detailed descriptions where possible.
OK - I discovered that Rosetta Code has Encyclopedia pages, that can
be used for any topic that doesn't fit in anywhere else. So I've
written a very short bit for the 'Category:SPARK' page which is what
is linked to by the language name. This page will contain links to
the Altran-Praxis home page and to their page about SPARK.
Then I've written a longer 'SPARK tools' page to go in the
Encyclopedia, to be linked from the category text, that describes the
Examiner and the Simplifier.
Then a 'SPARK Proof' page, also for the Encyclopedia and to be linked
from the SPARK tools page, that describes how verification conditions
are processed and discharged. (So readers won't see all the horrible
confusing options about proof until they've followed three separate
links and so are likely to be a bit more interested than the casual
browser).
The proof page briefly lists the different ways that an unproven but
provable VC can be dealt with (which is where all the problems have
cropped up), so if the code examples reference back to this when they
need to it should help to reduce the confusion in the reader faced by
multiple different types of artefact.
My first draft is in http://www.sparksure.com/resources/Rosetta_Text.txt.
Cheers,
Phil
Peter C. Chapin
> Following on from discussions in another thread, I propose the name
> SPlint for this fork.
Splint is the name of a C analysis tool. See http://www.splint.org/
Peter
Simon Wright
Oh well.
Dmitry A. Kazakov
articles. I think that SPARK is immensely important for Rosetta Code. I
would say, it is even more important than Ada itself, because it shows an
attitude to software developing absolutely different to ones represented by
other programming languages.
On Tue, 17 Aug 2010 12:53:18 -0700 (PDT), Phil Thornley wrote:
> OK - I discovered that Rosetta Code has Encyclopedia pages, that can
> be used for any topic that doesn't fit in anywhere else. So I've
> written a very short bit for the 'Category:SPARK' page which is what
> is linked to by the language name.
Integrate it here, please:
http://rosettacode.org/wiki/SPARK
> This page will contain links to
> the Altran-Praxis home page and to their page about SPARK.
Here is the standard place for this:
http://rosettacode.org/wiki/Category:SPARK_Implementations
Rosetta generated this page automatically.
> Then I've written a longer 'SPARK tools' page to go in the
> Encyclopedia, to be linked from the category text, that describes the
> Examiner and the Simplifier.
Could you also write a short encyclopedia article about proofs and link to
SPARK specific pages from there?
I would also suggest Rosetta Maintainers a new category (we should invent a
good clear name for it, e.g. "static analysis", "DbC", "provability") to
add it to this:
http://rosettacode.org/wiki/Language_Comparison_Table
BTW, it already contains SPARK (this happens automatically), feel free to
augment it.
P.S. Rosetta is living and very liberal, it is appropriate to contribute
not yet all-complete and polished material there. As someone said on other
occasion, please submit early!
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
Phil Thornley
wrote:
[...]
> On Tue, 17 Aug 2010 12:53:18 -0700 (PDT), Phil Thornley wrote:
> > OK - I discovered that Rosetta Code has Encyclopedia pages, that can
> > be used for any topic that doesn't fit in anywhere else. So I've
> > written a very short bit for the 'Category:SPARK' page which is what
> > is linked to by the language name.
>
> Integrate it here, please:
>
> http://rosettacode.org/wiki/SPARK
> > This page will contain links to
> > the Altran-Praxis home page and to their page about SPARK.
>
> Here is the standard place for this:
>
> http://rosettacode.org/wiki/Category:SPARK_Implementations
OK - I'll use this
> > Then I've written a longer 'SPARK tools' page to go in the
> > Encyclopedia, to be linked from the category text, that describes the
> > Examiner and the Simplifier.
Maybe I don't need these - I've just discovered the Wiki page about
SPARK:
http://en.wikipedia.org/wiki/SPARK_(programming_language)
> Could you also write a short encyclopedia article about proofs and link to
> SPARK specific pages from there?
I've also just discovered the Wiki page about static analysis - which
should do for this purpose:
http://en.wikipedia.org/wiki/Static_code_analysis
> I would also suggest Rosetta Maintainers a new category (we should invent a
> good clear name for it, e.g. "static analysis", "DbC", "provability") to
> add it to this:
>
> http://rosettacode.org/wiki/Language_Comparison_Table
>
Seem's a good idea - how about "statically analysable".
Cheers,
Phil
Dmitry A. Kazakov
It is too vague. In some sense any language is, after all there exist
static analysis tool for C. SPARK is obviously more than that, but it is
tricky to formulate the difference.
Jacob Sparre Andersen
> Phil Thornley wrote:
>> Dmitry A. Kazakov wrote:
>>> I would also suggest Rosetta Maintainers a new category (we should
>>> invent a good clear name for it, e.g. "static analysis", "DbC",
>>> "provability") to add it to this:
>>>
>>> http://rosettacode.org/wiki/Language_Comparison_Table
>>>
>> Seem's a good idea - how about "statically analysable".
>
> It is too vague. In some sense any language is, after all there exist
> static analysis tool for C. SPARK is obviously more than that, but it
> is tricky to formulate the difference.
Maybe we should simply introduce several categories.
+ Provable free of exceptions (run-time errors?)
+ Finite memory use.
+ Free of unreachable code.
+ ...?
I'm not quite sure exactly which categories I would formulate. Maybe
somebody from Spark-Team at Praxis can help us with some good
suggestions.
Greetings,
Jacob
--
"if a person can't communicate,
the very least he can do is to shut up!"
Phil Thornley
> On 17 Aug, 23:15, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
> [...]> On Tue, 17 Aug 2010 12:53:18 -0700 (PDT), Phil Thornley wrote:
> > > OK - I discovered that Rosetta Code has Encyclopedia pages, that can
> > > be used for any topic that doesn't fit in anywhere else. So I've
> > > written a very short bit for the 'Category:SPARK' page which is what
> > > is linked to by the language name.
>
> > Integrate it here, please:
>
> >http://rosettacode.org/wiki/SPARK
>
> Yes - will do.
> > > This page will contain links to
> > > the Altran-Praxis home page and to their page about SPARK.
>
> > Here is the standard place for this:
>
> >http://rosettacode.org/wiki/Category:SPARK_Implementations
>
> OK - I'll use this
Now done.
> > > Then I've written a longer 'SPARK tools' page to go in the
> > > Encyclopedia, to be linked from the category text, that describes the
> > > Examiner and the Simplifier.
>
> Maybe I don't need these - I've just discovered the Wiki page about
> SPARK:http://en.wikipedia.org/wiki/SPARK_(programming_language)
>
> > Could you also write a short encyclopedia article about proofs and link to
> > SPARK specific pages from there?
>
> I've also just discovered the Wiki page about static analysis - which
> should do for this purpose:http://en.wikipedia.org/wiki/Static_code_analysis
I've ended up referencing the SPARK Wiki page to get a description of
the language and tools, but added an encyclopedia page about the SPARK
proof process. (I want this there so that the tasks can reference it
when describing how they are proved.)
I've updated the Binary Search example to show both versions of the
package.
I've also edited the other two examples to get syntax colouring
working for them.
Please have a look at all of these and make any further improvements
you thing approriate.
Cheers,
Phil
Phil Thornley
> Dmitry A. Kazakov wrote:
> > Phil Thornley wrote:
> >> Dmitry A. Kazakov wrote:
> >>> I would also suggest Rosetta Maintainers a new category (we should
> >>> invent a good clear name for it, e.g. "static analysis", "DbC",
> >>> "provability") to add it to this:
>
> >>>http://rosettacode.org/wiki/Language_Comparison_Table
>
> >> Seem's a good idea - how about "statically analysable".
>
> > It is too vague. In some sense any language is, after all there exist
> > static analysis tool for C. SPARK is obviously more than that, but it
> > is tricky to formulate the difference.
>
> Maybe we should simply introduce several categories.
>
> + Provable free of exceptions (run-time errors?)
> + Finite memory use.
> + Free of unreachable code.
> + ...?
>
> I'm not quite sure exactly which categories I would formulate. Maybe
> somebody from Spark-Team at Praxis can help us with some good
> suggestions.
mean then there's no chance of other language users understanding what
we mean by it and using it correctly.
Phil
Phil Thornley
> Yannick Duchêne wrote:
[...]
> > subtype Index_Type is Integer range 1 .. 100; -- Arbitrary limits.
>
> Is there really any need to make this a subtype of Integer? Shouldn't
> it rather be a completely independent type:
I've left this as a subtype of Integer in the updated version on
Rosetta Code. The main reason is that an independent type would need
a base type assertion adding - which will just be noise to a casual
browser with only a small benefit gained.
(IMHO of course - and it's a Wiki, so ...)
Cheers,
Phil
J-P. Rosen
> On 19 Aug, 07:19, Jacob Sparre Andersen <spa...@nbi.dk> wrote:
>>>> Seem's a good idea - how about "statically analysable".
>>
[...]
> I suspect that if we can't come up with an obvious phrase for what we
> mean then there's no chance of other language users understanding what
> we mean by it and using it correctly.
>
What about "supports formal analysis" ?
--
---------------------------------------------------------
J-P. Rosen (ro...@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr
Dmitry A. Kazakov
> Le 20/08/2010 10:40, Phil Thornley a écrit :
>> On 19 Aug, 07:19, Jacob Sparre Andersen <spa...@nbi.dk> wrote:
>
>>>>> Seem's a good idea - how about "statically analysable".
>>>
> [...]
>> I suspect that if we can't come up with an obvious phrase for what we
>> mean then there's no chance of other language users understanding what
>> we mean by it and using it correctly.
>>
> What about "supports formal analysis" ?
That provokes the question - analysis of what?
J-P. Rosen
>> What about "supports formal analysis" ?
>
> That provokes the question - analysis of what?
>
If you mean: what kind of outcome from the analysis, I think it is
better to leave it open. We don't want a special category for Spark
where only Spark would get a mark.
The important parts here is "supports" (as opposed to "allows"), i.e.
the language includes features intended only for formal analysis,
without any effect on the generated code.
I guess Eiffel would qualify too.
Dmitry A. Kazakov
> Le 20/08/2010 11:23, Dmitry A. Kazakov a écrit :
>>> What about "supports formal analysis" ?
>>
>> That provokes the question - analysis of what?
>>
> Of the code, for sure ;-)
Doesn't C has code? Can't it be analyzed formally?
> If you mean: what kind of outcome from the analysis, I think it is
> better to leave it open. We don't want a special category for Spark
> where only Spark would get a mark.
Why not. I think that the category should indicate that the language
promotes static formal analysis as a necessary and integral part of
software design.
> The important parts here is "supports" (as opposed to "allows"), i.e.
> the language includes features intended only for formal analysis,
> without any effect on the generated code.
>
> I guess Eiffel would qualify too.
Only because the keyword "static" was lost. Dynamic formal analysis is
certainly possible and useful too, but it relates to the language in the
same way morbid anatomy does to therapy.
BTW, "without any effect on the generated code" would disqualify Eiffel
anyway.
J-P. Rosen
> On Fri, 20 Aug 2010 11:55:43 +0200, J-P. Rosen wrote:
>
>> Le 20/08/2010 11:23, Dmitry A. Kazakov a écrit :
>>>> What about "supports formal analysis" ?
>>>
>>> That provokes the question - analysis of what?
>>>
>> Of the code, for sure ;-)
>
> Doesn't C has code?
> Can't it be analyzed formally?
No. As soon as you have address arithmetic, no semantic can be
guaranteed. Well, it depends on what you call "formally" TBH.
[...]
>> The important parts here is "supports" (as opposed to "allows"), i.e.
>> the language includes features intended only for formal analysis,
>> without any effect on the generated code.
>>
>> I guess Eiffel would qualify too.
>
> Only because the keyword "static" was lost. Dynamic formal analysis is
> certainly possible and useful too, but it relates to the language in the
> same way morbid anatomy does to therapy.
>
> BTW, "without any effect on the generated code" would disqualify Eiffel
> anyway.
>
I thought about that after I sent the message. I really meant "without
any semantic effect on the generated code (in the absence of violations)"
Dmitry A. Kazakov
> Le 20/08/2010 12:24, Dmitry A. Kazakov a écrit :
>> Can't it be analyzed formally?
> No. As soon as you have address arithmetic, no semantic can be
> guaranteed. Well, it depends on what you call "formally" TBH.
But the definition does not hint what kind of properties have to be
analyzed (and when).
> [...]
>>> The important parts here is "supports" (as opposed to "allows"), i.e.
>>> the language includes features intended only for formal analysis,
>>> without any effect on the generated code.
>>>
>>> I guess Eiffel would qualify too.
>>
>> Only because the keyword "static" was lost. Dynamic formal analysis is
>> certainly possible and useful too, but it relates to the language in the
>> same way morbid anatomy does to therapy.
>>
>> BTW, "without any effect on the generated code" would disqualify Eiffel
>> anyway.
>>
> I thought about that after I sent the message. I really meant "without
> any semantic effect on the generated code (in the absence of violations)"
You mean the case when the code "supporting analysis" is dead code! What
kind of "support" is to include unreachable code? If it supports anybody,
then memory chips vendors. Then a dynamically typed language with its
"message not understood" would qualify for the same reasons as Eiffel.
J-P. Rosen
>> No. As soon as you have address arithmetic, no semantic can be
>> guaranteed. Well, it depends on what you call "formally" TBH.
>
> But the definition does not hint what kind of properties have to be
> analyzed (and when).
whether "static" should be put in, but I think it is important to keep
"formal".
> You mean the case when the code "supporting analysis" is dead code! What
> kind of "support" is to include unreachable code?
Of course. Spark's annotation have no effect on correct programs.
> If it supports anybody,
> then memory chips vendors. Then a dynamically typed language with its
> "message not understood" would qualify for the same reasons as Eiffel.
>
Anybody can argue about what "formal verification" means, but the same
is true of "strongly typed". Even in C, there are cases of code that
does not compile because of type mismatches...
It would make no sense to introduce a category "has Spark annotations".
We need something broader. And a minimum of honesty is needed when
checking the box. The only issue is to make sure that the casual reader
understands that it means: "has special features directed specifically
to analysis". Could be "has assertions", but that seems too restrictive
to me. So please, if you have a better idea, I'd be delighted to hear
about it.
Dmitry A. Kazakov
> Le 20/08/2010 14:25, Dmitry A. Kazakov a écrit :
>>> No. As soon as you have address arithmetic, no semantic can be
>>> guaranteed. Well, it depends on what you call "formally" TBH.
>>
>> But the definition does not hint what kind of properties have to be
>> analyzed (and when).
> It's on purpose. A category should be broad enough. We can discuss
> whether "static" should be put in, but I think it is important to keep
> "formal".
Yes
1. Formal in the sense that there is a specification.
2. Static, that verification happens before run time.
>> You mean the case when the code "supporting analysis" is dead code! What
>> kind of "support" is to include unreachable code?
> Of course. Spark's annotation have no effect on correct programs.
They do, because correctness itself depends on the annotation. If you
change the annotation, the program may become incorrect. Dead code does not
have this property.
> It would make no sense to introduce a category "has Spark annotations".
Yes.
> We need something broader. And a minimum of honesty is needed when
> checking the box. The only issue is to make sure that the casual reader
> understands that it means: "has special features directed specifically
> to analysis". Could be "has assertions", but that seems too restrictive
> to me. So please, if you have a better idea, I'd be delighted to hear
> about it.
I thought about a specific approach to programming, as it was proposed by
Dijkstra, with designing both the program and a proof that certain
properties of the program hold. SPARK's annotations support this approach.
This is not specific to SPARK.
(see below)
3ed38f7f-372d-422e...@x21g2000yqa.googlegroups.com, "Phil
Thornley" <phil.jp...@gmail.com> wrote:
Proof-oriented?
--
Bill Findlay
<surname><forename> chez blueyonder.co.uk
J-P. Rosen
> I thought about a specific approach to programming, as it was proposed by
> Dijkstra, with designing both the program and a proof that certain
> properties of the program hold. SPARK's annotations support this approach.
> This is not specific to SPARK.
>
extent, and also Ada with Pre/Post condition.
Now, do you have a name for it?
Dmitry A. Kazakov
> Le 20/08/2010 16:05, Dmitry A. Kazakov a écrit :
>> I thought about a specific approach to programming, as it was proposed by
>> Dijkstra, with designing both the program and a proof that certain
>> properties of the program hold. SPARK's annotations support this approach.
>> This is not specific to SPARK.
>>
> Good - and I still think that Eiffel could claim that to a certain
> extent, and also Ada with Pre/Post condition.
Not to me.
> Now, do you have a name for it?
No. Maybe by analogy to TDD (test-driven design):
proof-driven design support
Dmitry A. Kazakov
I like it!
Jacob Sparre Andersen
> On Fri, 20 Aug 2010 16:34:56 +0100, (see below) wrote:
>> Proof-oriented?
>
> I like it!
Yes. That sounds right.
It might also be worth considering a category ("contract-oriented",
"design by contract"?) which catches all languages with checked pre- and
post-conditions.
Greetings,
Jacob
--
Ada - the programming language still ahead of its time.
Dmitry A. Kazakov
> It might also be worth considering a category ("contract-oriented",
> "design by contract"?) which catches all languages with checked pre- and
> post-conditions.
Any strongly typed language is contract-oriented. (It is interesting to
speculate whether contracts unrelated to types and subtypes may exist.)
As for checked pre- and post-conditions they rather are debug-oriented,
partially, TDD and, to lesser extent, defensive programming.