Prev: very important science....
Next: Ada & gdb (was: for S'Image use Func??)
From: Dmitry A. Kazakov on 12 May 2010 11:37
On Wed, 12 May 2010 10:41:03 +0200, stefan-lucks(a)see-the.signature wrote:

> 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 ...

Any program is partially correct, if otherwise has not been observed. I
fail to see how Eiffel is different from C or Assembler in that respect.

The point is that run-time checks contribute nothing to correctness either
partial or not. Because a partially incorrect program remains partially
incorrect independently on whether you check that or not: SPARK makes
*some* incorrect programs invalid. Eiffel does not. That is the difference.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
From: Yannick Duchêne (Hibou57) on 12 May 2010 12:06
Le Wed, 12 May 2010 17:37:44 +0200, Dmitry A. Kazakov
<mailbox(a)dmitry-kazakov.de> a écrit:
> Any program is partially correct, if otherwise has not been observed. I
> fail to see how Eiffel is different from C or Assembler in that respect.
If Eiffel was the same as C or assembly, why would Meyer have created it
and why people seeking for safety would be interested in this one ?

OK, the latter assertion is not proof of anything, and I may just be
talking about people who are wrong.

Go further : look at Eiffel's syntax and semantic associated to each
syntactic elements and compare that to what's provided with C (by the way,
there exist formal specifications for C as well, I mean ACSL previously
presented) or assembly. Can't you see something different ?

There is at least, and this is not subjective, two areas in which it
differs : expression and runtime-check.

Well, I've noted you do not like runtime-check because it is not [formal]
proof of anything, but no one said it is formal proof, this is just better
to catch error the sooner and understand why this was an error. This is
already the purpose of exceptions, and Eiffel's formalism helps in that
area... because it comes with a formalization.

About expression now, although understandability of a source does not
provide proof, this help to at least make partial assertions and discover
what's wrong. Obviously, static checker does not even need input which are
human readable : does this means we do not need human-readable as a
feature ?

A C or assembly designed application is unlikely to raise a run-time
exception when it detect an erroneous runtime condition. It will just
raise exception (or signals) when CPU will be in a critical states as
request for data in an non-existing memory page, as an example. Detecting
error at runtime in the program state itself, at an higher level, is
better than this critical kind of CPU level critical state. It is best to
face an error like “this class invariant was violated” than “this access
to this memory address failed”. The purpose of Eiffel is to help to catch
errors at the higher level as possible, thus at a level which is nearer to
human or proper application functionalities concern. In that way, this is
a step toward abstraction and formal specification.

This is not, this is a step toward.

Eiffel's not SPARK, there is no doubt about it, and that was previously
stated, even by Eiffel advocators.


However, to say “C, assembly and Eiffel are all the same and none provided
better proof an application may at least run partially good” is a lot said
(it is by the way as much true that jocks and teasing kept apart, C is not
the same as assembly)

And like Pascal said : “Eiffel is far more easier than SPARK” (you cannot
request every one to know SPARK, and you help them when you provide them
something like Eiffel).

Given all that : SPARK is largely known as not being able to handle some
complex applications, which are yet of every day use (like a web browser).
If SPARK cannot handle the whole of these applications, what can we do ?
Eiffel's approach is a suggested one... This does not statically check
statically, this do it at runtime instead, ... still better than no
abstraction and formalization at all.

--
pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 12 May 2010 12:49
Le Wed, 12 May 2010 17:59:21 +0200, Phil Thornley
<phil.jpthornley(a)googlemail.com> a écrit:
> Sorry, Yannick, but you are wrong.
>
> Recursion between subprograms in different packages is prohibited by
> the rule that mutual inheritance between packages is not allowed.
That's one of that severe limitations so (noted, as I'm learning).

> Recursion between subprograms in a single package (including self-
> recursion) is prohibited by the rule that a subprogram cannot be
> called until all of its body has been declared. I don't think this is
> mentioned in the SPARK language description, but if you violate this
> rule you get semantic error 163:
An attempt to give an answer : I had to drop recursivity in a JavaScript
application, because this was a long process and JavaScript has no support
at all for multi-tasking (except with some tricks relying on pop-up
windows... which unfortunately browsers blocks). So I had to rely on
timer, bounded execution chunk (kind of cooperative multitasking as it was
with Windows 3.1) and had to re-implement recursivity on top of an array
used as a stack. The “process” was reloading its previous state from
variables each time it was resuming, and as there was obviously no way to
restore the stack pointer (JavaScript is not C or assembly you know), I
had to re-implement the stack this way.

I suppose this kind of recursivity would be OK.

May be this help analysis after all ?

And there are recursivities which can be dropped, like the one of
binary-search (a kind of final recursivity, and that is a common
optimization in functional languages to drop these)

> I haven't seen the latest SPARK version yet (still waiting for the GPL
> version) but I would be very surprised if this has changed since the
> last version.
>
> Cheers,
>
> Phil
The one I've installed yesterday is version 8.1.1. Not version 9 Mark L
talked about, however, this one seems to already have support for generics.

--
pragma Asset ? Is that true ? Waaww... great
From: stefan-lucks on 12 May 2010 14:10
On Wed, 12 May 2010, Dmitry A. Kazakov wrote:

> Any program is partially correct, if otherwise has not been observed. I
> fail to see how Eiffel is different from C or Assembler in that respect.

In C, if I try to compute the factorial of a (natural) number, I'll always
get an answer (assuming a decent program, which can be written by a
first-year computer science student, and a normal C-compiler). The answer
may be right or wrong. If the input is too large, the answer actually is
wrong (our first-year student stores the result in an int variable, and
100! is too large). But I still get an answer, even if it is wrong.

In Eiffel, I'll either get an answer, or the program will tell that at
some point of time when computing, say, the factorial of 100, a certain
exception has been raised. (I didn't try out Eiffel, but that is what I
would expect.) But if I get an answer, I can be sure it is the right one.
That is partial correctness.

In SPARK, the examiner (or the simplifier or the proof checker) will tell
me that my program is only correct if I specify a certain precondition
(e.g., if the input is less than some upper bound). So in SPARK, I can be
sure that I'll get the right answer, and SPARK forces me to specify the
proper preconditions to get the right answer. Except that even a proper
SPARK program might run in an infinite loop ...

In any case, there is a huge difference between SPARK and Eiffel, but also
between Eiffel and C.

> The point is that run-time checks contribute nothing to correctness either
> partial or not. Because a partially incorrect program remains partially
> incorrect independently on whether you check that or not:

Technically, any program of the form

{Any Precondition}
Statements;
if not Postcondition then
raise Program_Error;
end if;
{Postcondition}

is partially correct, even if "Statements;" are semantic nonsense (as long
as the whole thing compiles at all), regardless of "{Any Precondition}".

Perhaps you don't like raising an exception?

OK, we can stick with the original approach from Hoare from 1969, who
didn't know (or didn't care) about exceptions. The following program is
partially correct, regardless of the "Statements;" and "{Any
Precondition}":

{Any Precondition}
Statements;
while not Postcondition loop
null;
end loop;
{Postcondition}

Actually, the second program could be written in SPARK. It would pass all
the static verification performed by the SPARK toolset chain, without
leaving any unproven verification conditions. Still, when running the
program I can only trust that if I get a result, it satisfies my
precondition -- but I can't be sure it satisfies my precondition.

More natural -- but not necessarily better -- is the following program:

{Any Precondition}
while not Postcondition loop
Statements;
end loop;
{Postcondition}

Same problem: partial correctness is trivial, regardless of "Statements;".


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! ------

From: Dmitry A. Kazakov on 12 May 2010 13:24
On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote:

> Well, I've noted you do not like runtime-check because it is not [formal]
> proof of anything, but no one said it is formal proof, this is just better
> to catch error the sooner and understand why this was an error.

Yes, it is better but that is not the point. Which is there is no
substantial difference between Eiffel precondition and C's if statement
beyond syntax sugar, and that if-statement is less misleading.

> About expression now, although understandability of a source does not
> provide proof, this help to at least make partial assertions and discover
> what's wrong.

No more than an appropriately placed if-statement, tracing call, debugging
break point etc.

> It is best to
> face an error like “this class invariant was violated” than “this access
> to this memory address failed”.

The text used in error message is up to the programmer. My objection is not
that what Eiffel offers is useless. The objection is that it has nothing to
do with contracts (in its normal meaning) or with design by. These are no
more than *debugging* tools. Using the terms pre-, postcondition, invariant
is also misleading.

> And like Pascal said : “Eiffel is far more easier than SPARK” (you cannot
> request every one to know SPARK, and you help them when you provide them
> something like Eiffel).

Yes, but you do not want to prove everything, which is impossible anyway.
What Ada lacks is better contracts specified by the programmer only when he
wishes to. E,g, exception contracts, statements about purity of a function,
upper bound of stack use etc.

IMO, Ada does not need Eiffel-like pre- postconditions, assertions etc.
They add nothing to safety and thus to Ada. It would be enough to introduce

raise when <condition>;

and close the theme. (Yes I heard the argument that one can use them in
declarations. I don't think that is a good idea. I don't like exceptions
from declarations.)

Ada had dynamic constraints long before Eiffel. If one wished to extend
this feature, it is welcome. Just do not call it "error check", when you
use the subtype Positive. Tie it to subtypes.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Prev: very important science....
Next: Ada & gdb (was: for S'Image use Func??)