f



SPARK left/right shift.

Hi.

What's the "correct" way to get access to left/right shift operations
for modular types in SPARK? I see from the Checker manual that
the proof language is capable of modelling them but then I also see
that the Interfaces package isn't predefined.
0
xorquewasp (64)
7/21/2009 9:07:40 AM
comp.lang.ada 8774 articles. 2 followers. Post Follow

8 Replies
979 Views

Similar Articles

[PageSpeed] 9

On Jul 21, 10:07=A0am, xorque <xorquew...@googlemail.com> wrote:
> Hi.
>
> What's the "correct" way to get access to left/right shift operations
> for modular types in SPARK?

The standard shift/rotate functions in Interfaces
are overloaded, so not legal SPARK.  The way round this is
to declare a "shadow" package that de-overloads them for SPARK.
I'll post an example of how to do it in a minute...
 - Rod
0
7/21/2009 9:21:38 AM
OK - it's done as follows.  We create a SPARK "shadow" specification
of
package Interfaces and a new package SPARK_Interfaces for which there
is an Ada version (for the compiler) and a shadow version (for the
Examiner.)

1) Add the following to your Examiner index file:

interfaces spec is in interfaces.shs
spark_interfaces spec is in spark_interfaces.shs

2) interfaces.shs contains

package Interfaces
is
   type Unsigned_32 is mod 2**32;
   -- ... and similarly for other Unsigned_XX types
end Interfaces;

3) spark_interfaces.shs contains

with Interfaces;
--# inherit Interfaces;
package SPARK_Interfaces
is
   function Rotate_Left_32
     (Value  : Interfaces.Unsigned_32;
      Amount : Natural) return Interfaces.Unsigned_32;

end SPARK_Interfaces;

(note this removes the overloading, and declares the function so it's
legal SPARK)

4) spark_interfaces.ads contains

with Interfaces;
package SPARK_Interfaces
is
   function Rotate_Left_32
     (Value  : Interfaces.Unsigned_32;
      Amount : Natural) return Interfaces.Unsigned_32 renames
Interfaces.Rotate_Left;

end SPARK_Interfaces;

(note this _renames_ the original function from Interfaces, so you
still
get the efficiency of the Intrinsic version.)

OK?
 - Rod

0
7/21/2009 9:31:32 AM
Rod Chapman wrote:
> OK - it's done as follows...

Looks good.

Thanks very much!
0
xorquewasp (64)
7/21/2009 9:38:19 AM
xorque,
 If it's not a dumb question: what exactly are you trying to
implement with SPARK?  It seems rather ambitious - you've
been pushing the boundaries a fair bit....
 - Rod Chapman, SPARK Team
0
7/21/2009 9:54:49 AM
Rod Chapman wrote:
> xorque,
>  If it's not a dumb question: what exactly are you trying to
> implement with SPARK?  It seems rather ambitious - you've
> been pushing the boundaries a fair bit....

Currently, a UTF-8 encoder/decoder.

Quite a few questions I've posted on here have been related
to "toy" projects testing what can be done sanely with this
degree of verification in Ada. I've rarely been disappointed.

I'm not currently writing anything that could be described
as "high-integrity" but I try to use SPARK wherever possible
as I do care deeply about software quality.
0
xorquewasp (64)
7/21/2009 10:00:18 AM
xorque schrieb:

> I'm not currently writing anything that could be described
> as "high-integrity" but I try to use SPARK wherever possible
> as I do care deeply about software quality.

Can I second this?  In writing a double buffer properly,
in particular when varying length characters need to be
handled, SPARK is really helpful, if only to sort out
and document the author's assumptions, omissions, and errors.

Same for a live topsorted structure that is waiting on
my shelf to be finished.
0
7/21/2009 10:40:29 AM
xorque a �crit :
> Rod Chapman wrote:
>> xorque,
>>  If it's not a dumb question: what exactly are you trying to
>> implement with SPARK?  It seems rather ambitious - you've
>> been pushing the boundaries a fair bit....
> 
> Currently, a UTF-8 encoder/decoder.
> 
FYI:
Rather than inventing your own interface, there is currently a proposal
for coding/decoding functions, see AI05-0137.


-- 
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr
0
rosen (784)
7/21/2009 10:46:02 AM
> Rather than inventing your own interface, there is currently a proposal
> for coding/decoding functions, see AI05-0137.

Unfortunately, in it's current state, that interface isn't possible to
implement in SPARK directly (without a non-SPARK wrapper)
It uses exceptions, returns unconstrained arrays, etc.
0
xorquewasp (64)
7/21/2009 11:33:47 AM
Reply: