From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 border1.nntp.ams3.giganews.com!border1.nntp.ams2.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!eternal-september.org!feeder.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: The future of Spark . Spark 2014 : a wreckage
Date: Mon, 08 Jul 2013 20:24:54 +0100
Organization: A noiseless patient Spider
Message-ID: <lyvc4kyhvd.fsf@pushface.org>
References: <d84b2eb2-eab3-4dec-917c-0498473c1e93@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: mx05.eternal-september.org;
 posting-host="a849a84efccf4ec3e3fdf530b5c53bc9";
 logging-data="31711"; mail-complaints-to="abuse@eternal-september.org";
 posting-account="U2FsdGVkX19VEFPEHenppFsCRkutszOW7kEQLL10B5Y="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (darwin)
Cancel-Lock: sha1:uw6tfDAZ+iQY8AjKe/S2oz0L52A=
 sha1:WYtpyKj5H9jRyszh+1AE8uJFZRk=
X-Original-Bytes: 3112
Xref: number.nntp.dca.giganews.com comp.lang.ada:182340
Date: 2013-07-08T20:24:54+01:00
List-Id: <comp.lang.ada>

vincent.diemunsch@gmail.com writes:

> Same specification in Spark 2014 :
>    procedure Swap
>       with Global  => (In_Out => (X, Y)),
>            Depends => (X => Y,   -- to be read as "X depends on Y"
>                        Y => X);  -- to be read as "Y depends on X"
>
> How are we supposed to guess that "X => Y" means X depends on Y, if
> the arrow goes from X to Y ? In the literature, Flow analysis use
> always Information Flow where arrows follows the real move of
> information. See for instance "SPARK the proven approach of High
> Integrity Software" from John Barn page 311 or the "Dragon Book"
> (Compilers : principles, techniques and tools).

Maybe, but a UML dependency would be read the way that you have quoted.
I don't expect users would guess, I expect they'd RTFM.

> - the syntax makes a complete confusion between a precondition and a
> test : Preconditions are SPECIFICATIONS that insures that the runtime
> tests that the Ada compiler puts in the code will pass. What's the use
> of testing at the entry of a procedure what will be tested in the
> procedure ? Doing the test twice won't impove correctness ! That is
> why proconditions and postconditions must stay as comments.

I assume that after one has done a successful proof of correctness with
SPARK 2014 one will build with a configuration that says that assertions
and predicates are to be ignored (ARM 11.4.2). I suspect that for many
real-time systems you'd need to do this to get timely operation anyway;
nice if the compiler could ensure the Note, "Normally, the boolean
expression in a pragma Assert should not call functions that have
significant side effects when the result of the expression is True, so
that the particular assertion policy in effect will not affect normal
operation of the program.", but that's probably equivalent to the
halting problem.

I wonder whether the same consideration should apply to predicates?

> Expressions functions break the Ada Specification

Expression functions are *in* the Ada Specification! (assuming you mean
the ARM?)