From: Jacob Sparre Andersen <jspa@nykredit.dk>
Subject: Re: SPARK and static unit checking?
Date: Mon, 14 Apr 2008 04:21:56 -0700 (PDT)
Date: 2008-04-14T04:21:56-07:00 [thread overview]
Message-ID: <f6625d23-9ff0-417d-9d87-890cf52ec045@a22g2000hsc.googlegroups.com> (raw)
In-Reply-To: O1nEKjD2FmAIJwBH@diphi.demon.co.uk
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]
next prev parent reply other threads:[~2008-04-14 11:21 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
2008-04-14 11:21 ` Jacob Sparre Andersen [this message]
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