SPARK left/right shift.

SPARK left/right shift.

[xorque]

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.

Re: SPARK left/right shift.

[Rod Chapman]

On Jul 21, 10:07 am, 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

Re: SPARK left/right shift.

[Rod Chapman]

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

Re: SPARK left/right shift.

[xorque]

Rod Chapman wrote:
> OK - it's done as follows...

Looks good.

Thanks very much!

Re: SPARK left/right shift.

[Rod Chapman]

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

Re: SPARK left/right shift.

[xorque]

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.

Re: SPARK left/right shift.

[Georg Bauhaus]

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.

Re: SPARK left/right shift.

[Jean-Pierre Rosen]

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

Re: SPARK left/right shift.

[xorque]

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