SPARK and static unit checking?

SPARK and static unit checking?

[Jacob Sparre Andersen]

I have found a rather annoying (but in some ways very reasonable) rule
in SPARK:

   You are not allowed to (re)declare operators for a type.

This prevents me from using my standard trick for static unit type
checking:

   type Length is private;
   function "+" (L, R : Length) return Length; -- not SPARK
   ...
   Meter : constant Length;

   type Area is private;
   function "*" (L, R : Length) return Area; -- not SPARK
   ...

I have an idea for a (clumsy) solution:  Generate two packages with
the same types (name-wise).  The one as above, the other simply as:

   type Length is new Float;
   type Area is new Float;

Then I can use the liberal version with the SPARK tools, and swap the
restrictive in for the proper compilation.

Any proposals for an elegant solution?

Jacob
--
[ I left my signature generator at home. ]

Re: SPARK and static unit checking?

[JP Thornley]

In article 
<af9b42f7-b24c-4ca5-8a49-1ea9c15e1f37@y21g2000hsf.googlegroups.com>, 
Jacob Sparre Andersen <jspa@nykredit.dk> writes
>I have found a rather annoying (but in some ways very reasonable) rule
>in SPARK:
>
>   You are not allowed to (re)declare operators for a type.
>
>This prevents me from using my standard trick for static unit type
>checking:
>
>   type Length is private;
>   function "+" (L, R : Length) return Length; -- not SPARK
>   ...
>   Meter : constant Length;
>
>   type Area is private;
>   function "*" (L, R : Length) return Area; -- not SPARK
>   ...
>
>I have an idea for a (clumsy) solution:  Generate two packages with
>the same types (name-wise).  The one as above, the other simply as:
>
>   type Length is new Float;
>   type Area is new Float;
>
>Then I can use the liberal version with the SPARK tools, and swap the
>restrictive in for the proper compilation.

Ummmm, sorry no - derived types aren't allowed either (except for 
extending tagged record types).

>
>Any proposals for an elegant solution?

The nearest you can get to derived types is simply:

    type Length is digits 6;

but this will require type conversions that are not required by the 
"proper" version (and which will be required by the derived types as 
well).

I guess the only way is an unconstrained subtype:

    subtype Length is Float;

(hardly elegant, but ...)

Phil Thornley

-- 
JP Thornley

Re: SPARK and static unit checking?

[Jacob Sparre Andersen]

JP Thornley wrote:
> Jacob Sparre Andersen writes

> >   type Length is new Float;
> >   type Area is new Float;
>
> >Then I can use the liberal version with the SPARK tools, and swap the
> >restrictive in for the proper compilation.
>
> Ummmm, sorry no - derived types aren't allowed either (except for
> extending tagged record types).

[...]

> I guess the only way is an unconstrained subtype:
>
>     subtype Length is Float;

This was what I was thinking when I wrote "type Length is new".  With
derived types, I wouldn't be allowed to multiply Length with Length to
get Area.

The main question still remains.

Jacob
--
[I left my signature generator at home]

Re: SPARK and static unit checking?

[roderick.chapman]

SPARK has a few general princles regarding the arithmetic
operators.

1) They are always "monotonic" meaning they take and return the same
type - the binary operators, for example, always have the signature
  (Left, Right : in T) return T

2) There is no re-declaration, renaming, or user-defined overloading
of the
operators, so "+" _always_ means "arithmetic addition" (which might
be signed integer, modular integer, floating, or fixed, of course...)

3) You can't change the base-name of an operator via a renaming,
which,
as Bob Duff pointed out in another thread, is a dreadful thing to do
anyway.

You can define functions with identifiers for names if you can put
up with having to write "My_Plus (A, B)" instead of "A + B" for
instance.

- Rod Chapman, SPARK Team