Prev: More Ada in Cryptography.
Next: What Ada can do for Cryptography.
From: Simon Wright on 30 Jun 2010 01:08
"Randy Brukardt" <randy(a)rrsoftware.com> writes:

> This is exactly why I'm not much interested in SPARK itself: because
> it forces programs back into the style that I originally learned for
> Fortran IV in 1976: no dynamic allocation, no dynamic calls, no
> exceptions -- no interest! I'm interested in what SPARK brings to the
> table in proof capabilities, but I see no reason to give up 3/4rds of
> Ada to get it.

Complete agreement here!
From: stefan-lucks on 30 Jun 2010 04:17
On Tue, 29 Jun 2010, Randy Brukardt wrote:

> Returning to the dark ages of programming (that is BE - Before Exceptions)
> and reintroducing all of the problems of early C code just because of
> inadequate tools seems like a horrible step backwards to me.

I agree that error returns in code that isn't statically checked is a
first-class flight into the world of severe errors and bugs.

But for SPARK, if a subprogram can return an error code and you forget to
handle the error code, SPARK will remind you -- your program will not pass
the static verification. So the kind of errors introduced by error returns
can easily be avoided in SPARK.

So long

Stefan

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

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