From: JP Thornley <jpt@diphi.demon.co.uk>
Subject: Re: SPARK and static unit checking?
Date: Sun, 13 Apr 2008 20:39:34 +0100
Date: 2008-04-13T20:39:34+01:00 [thread overview]
Message-ID: <O1nEKjD2FmAIJwBH@diphi.demon.co.uk> (raw)
In-Reply-To: af9b42f7-b24c-4ca5-8a49-1ea9c15e1f37@y21g2000hsf.googlegroups.com
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
next prev parent reply other threads:[~2008-04-13 19:39 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2008-04-11 9:59 SPARK and static unit checking? Jacob Sparre Andersen
2008-04-13 19:39 ` JP Thornley [this message]
2008-04-14 11:21 ` Jacob Sparre Andersen
2008-04-14 14:57 ` roderick.chapman
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox