From: Yannick Duchêne (Hibou57) on
Le Tue, 11 May 2010 21:45:45 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene(a)yahoo.fr> a écrit:
> This limitation (generics) may not be always true, as it seems there are
> some plans to change it : AdaCore and Praxis are working toward this.
> Interested parties may have a look at this quick presentation :
> http://mpri.master.univ-paris7.fr/stages-2010/20091104-154948/sujet-containers.pdf

Hey Folks! I'm dreaming!

I've just installed the last version of SPARK, started to play a bit with
its basic principles on a test package, then, just to see what will
happened, turned the package into a generic. And you know what ? Yes, you
guess : the SPARK examiner did not returned any error about it and just
displayed the message

About to call SetPackageIsGeneric P
ThePackage P
IS GENERIC

I though it has simply drop the whole text, so I've introduced an error on
purpose in the package, and it has complained about the error (a missing
annotation for a procedure declaration), which is the proof that it did
not drop the package text.

Nice, looks promising.

Well, that's just the examiner, that's not all the stuff (which I still
need to learn)... anyway, I like that.

Hope you will try too

I will open a later thread about some SPARK stuffs (for questions, as I'm
just beginning with it).

P.S. Do not know what implies this “About to call SetPackageIsGeneric P”,
just hope I do not have to bother for the time.

--
pragma Asset ? Is that true ? Waaww... great
From: stefan-lucks on
On Tue, 11 May 2010, Dmitry A. Kazakov wrote:

> On Tue, 11 May 2010 18:05:42 +0200, Yannick Duch�ne (Hibou57) wrote:
>
> > While they can be compared in some way, there is indeed a big difference :
> > Eiffel is runtime oriented, SPARK is static analysis oriented.
>
> A proof of correctness cannot be run-time. Incorrectness need no proof.

Actually, there is a difference between partial and total correctness. A
program is partially correct, if it produces the correct result in the
case it produces any result. A partially correct program may run
infinitely or abort with an exception, but when it does
neither, you get the specified result. A totally correct program is
partially correct *and* terminates in finite time *and* doesn't abort with
an unhandled exception. So Eiffel programs seen to be partially correct,
but lack any proof of total correctness. Which is OK for some
applications. I would expect the autopilot of an airplane to be totally
correct -- partial correctness wouldn't be too helpful. But there are
plenty of applications, where a partially correct program would be a huge
improvement over all the software we are currently using ...

BTW, SPARK also only provides partial correctness, but no total
correctness. While SPARK allows to prove that no exception is raised (*),
it lacks the option to specify (and verify, of course) variants for
WHILE-loops (**). Eiffel supports such
invariants.

So long

Stefan

P.S.: I have worked a bit with SPARK, and I am currently trying to
improve my knowledge about it. While I do prefer static analysis
over Eiffels dynamic checking at run time, I still think Eiffel's
approach has its place. The constraints of SPARK as a programming
language are severe. (For me, the worst is the prohibition of
recursive subprograms.)

------
(*) Actually, as much as I understand SPARK, it doesn't allow to prove
that the absence of Storage_Error. For that purpose, one needs an
additional compiler-specific tool.

(**) I just read that the most recent version of SPARK is able to deal
with generics. Great! Maybe, SPARK has also recently learned how to
specify and prove loop variants?


--
------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------
Stefan dot Lucks at uni minus weimar dot de
------ I love the taste of Cryptanalysis in the morning! ------
From: Mark Lorenzen on
On 12 Maj, 01:44, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr>
wrote:
> Hey Folks! I'm dreaming!
>
> I've just installed the last version of SPARK, started to play a bit with  
> its basic principles on a test package, then, just to see what will  
> happened, turned the package into a generic. And you know what ? Yes, you  
> guess : the SPARK examiner did not returned any error about it and just  
> displayed the message
>
>     About to call SetPackageIsGeneric P
>     ThePackage P
>     IS GENERIC
>
> I though it has simply drop the whole text, so I've introduced an error on  
> purpose in the package, and it has complained about the error (a missing  
> annotation for a procedure declaration), which is the proof that it did  
> not drop the package text.
>
> Nice, looks promising.

The planned support for generics was announced at the "Introducing
SPARK 9.0" webinar, see http://www.adacore.com/home/products/gnatpro/webinars/
and click "Introducing SPARK 9.0". The announcement is at 25:30 to
26:50.

- Mark L
From: Yannick Duchêne (Hibou57) on
Le Wed, 12 May 2010 10:41:03 +0200, <stefan-lucks(a)see-the.signature> a
écrit:
> it lacks the option to specify (and verify, of course) variants for
> WHILE-loops (**). Eiffel supports such
> invariants.
I was to ask you if you were really sure, ... you've already requested for
more comments in the P.S., so may not give me an answer.
Well, you may also see a loop as an abstraction surrounded by pre and post
and requires the previous state in some the same as the new one after each
iteration (just a beginner's two cents idea)

> P.S.: I have worked a bit with SPARK, and I am currently trying to
> improve my knowledge about it. While I do prefer static analysis
> over Eiffels dynamic checking at run time, I still think Eiffel's
> approach has its place. The constraints of SPARK as a programming
> language are severe. (For me, the worst is the prohibition of
> recursive subprograms.)
I'm just starting with SPARK, so I may be wrong : it seems to me recursion
is allowed if the stack usage is bounded (keep in mind I may be wrong).

--
pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on
Le Wed, 12 May 2010 14:12:31 +0200, Mark Lorenzen
<mark.lorenzen(a)gmail.com> a écrit:
> The planned support for generics was announced at the "Introducing
> SPARK 9.0" webinar, see
> http://www.adacore.com/home/products/gnatpro/webinars/
> and click "Introducing SPARK 9.0". The announcement is at 25:30 to
> 26:50.
>
> - Mark L
I've posted a planned to support generic previously I've discovered
support seems to be already there.
Your link (interesting) shows it recent.
Thanks for the news.

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