From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,5aa1f17e1cbe0afb X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!postnews.google.com!a22g2000hsc.googlegroups.com!not-for-mail From: Jacob Sparre Andersen Newsgroups: comp.lang.ada Subject: Re: SPARK and static unit checking? Date: Mon, 14 Apr 2008 04:21:56 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: NNTP-Posting-Host: 195.249.127.231 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1208172222 2620 127.0.0.1 (14 Apr 2008 11:23:42 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 14 Apr 2008 11:23:42 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: a22g2000hsc.googlegroups.com; posting-host=195.249.127.231; posting-account=UqUC7goAAAAaIopcWPSUmIYxkLwIeB6X User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.1; SV1; .NET CLR 1.1.4322; .NET CLR 2.0.50727; InfoPath.1; .NET CLR 3.0.04506.648; .NET CLR 3.5.21022),gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:20932 Date: 2008-04-14T04:21:56-07:00 List-Id: JP Thornley wrote: > Jacob Sparre Andersen writes > > =A0 type Length is new Float; > > =A0 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: > > =A0 =A0 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]