* SPARK and static unit checking?
@ 2008-04-11 9:59 Jacob Sparre Andersen
2008-04-13 19:39 ` JP Thornley
0 siblings, 1 reply; 4+ messages in thread
From: Jacob Sparre Andersen @ 2008-04-11 9:59 UTC (permalink / raw)
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. ]
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: SPARK and static unit checking?
2008-04-11 9:59 SPARK and static unit checking? Jacob Sparre Andersen
@ 2008-04-13 19:39 ` JP Thornley
2008-04-14 11:21 ` Jacob Sparre Andersen
0 siblings, 1 reply; 4+ messages in thread
From: JP Thornley @ 2008-04-13 19:39 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: SPARK and static unit checking?
2008-04-13 19:39 ` JP Thornley
@ 2008-04-14 11:21 ` Jacob Sparre Andersen
2008-04-14 14:57 ` roderick.chapman
0 siblings, 1 reply; 4+ messages in thread
From: Jacob Sparre Andersen @ 2008-04-14 11:21 UTC (permalink / raw)
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]
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: SPARK and static unit checking?
2008-04-14 11:21 ` Jacob Sparre Andersen
@ 2008-04-14 14:57 ` roderick.chapman
0 siblings, 0 replies; 4+ messages in thread
From: roderick.chapman @ 2008-04-14 14:57 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2008-04-14 14:57 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2008-04-11 9:59 SPARK and static unit checking? Jacob Sparre Andersen
2008-04-13 19:39 ` JP Thornley
2008-04-14 11:21 ` Jacob Sparre Andersen
2008-04-14 14:57 ` roderick.chapman
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox