From: Lutz Donnerhacke <lutz@iks-jena.de>
Subject: Re: [Spark] Using defered constants
Date: Wed, 23 Apr 2003 10:52:58 +0000 (UTC)
Date: 2003-04-23T10:52:58+00:00 [thread overview]
Message-ID: <slrnbacs4a.op.lutz@taranis.iks-jena.de> (raw)
In-Reply-To: 3EA65CA6.5010705@praxis-cs.co.uk
* Peter Amey wrote:
> Lutz's question has caused me to reconsider all this and the next release
> of the Examiner will relax these rules so that after the point that Ada
> requires that the deferred constant to be complete it can be used even if
> the SPARK Examiner has not seen it (because it is hidden).
Thank you very much.
> The worst consequence for the Examiner will be the ability to construct
> programs with hidden pakcage private parts that will examine cleanly but
> not compile because soemthing in the hidden part makes them illegal Ada;
> at least this is "safe".
Of course. You can't check hidden areas. If you would do so, you would not
need the argument of #hide, because then you can determine the closure of
the hidden region yourself.
> As with all these things, it is feedback from active users that drive
> things forward!
I'm not an active user. I'm just playing with Spark and Ada.
Back to the original problem. A simple workaround is to replace the constant
by a parameterless (inlined) function.
package t is
type x is private;
function cx return x;
procedure copy(o : out x; i : Integer);
--# derives o from i;
private
--# hide t;
type x is new Integer;
end t;
package body t is
function cx return x is
--# hide cx;
begin
return 0;
end cx;
procedure doupdate(o : in out x; i : Integer)
--# derives o from i, o;
is
--# hide doupdate;
begin
o := o + x(i);
end doupdate;
procedure copy(o : out x; i : Integer) is
begin
o := cx;
doupdate(o, i);
end copy;
end t;
prev parent reply other threads:[~2003-04-23 10:52 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-04-15 13:18 [Spark] Using defered constants Lutz Donnerhacke
2003-04-16 13:01 ` Rod Chapman
2003-04-16 13:37 ` Lutz Donnerhacke
2003-04-16 15:05 ` Hyman Rosen
2003-04-16 15:15 ` Lutz Donnerhacke
2003-04-16 15:27 ` Vinzent Hoefler
2003-04-23 9:28 ` Peter Amey
2003-04-23 10:52 ` Lutz Donnerhacke [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox