Talk About Network



Register and Login
Nick
Password
Register create new account Sign up is FREE and you can post replies, new topics, bookmark posts and more!
Recover lost password


Programming > Ada > SPARK and stati...
Latest [ Topics | Posts ] Archive Post A New Topic Post a Reply
<< Topic < Post Post 1 of 4 Topic 5650 of 5697
Post > Topic >>

SPARK and static unit checking?

by Jacob Sparre Andersen <jspa@[EMAIL PROTECTED] > Apr 11, 2008 at 02:59 AM

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. ]




 4 Posts in Topic:
SPARK and static unit checking?
Jacob Sparre Andersen <  2008-04-11 02:59:20 
Re: SPARK and static unit checking?
JP Thornley <jpt@[EMAI  2008-04-13 20:39:34 
Re: SPARK and static unit checking?
Jacob Sparre Andersen <  2008-04-14 04:21:56 
Re: SPARK and static unit checking?
roderick.chapman@[EMAIL P  2008-04-14 07:57:49 

Post A Reply:
  Go here to Signup

AddThis Feed Button


About - Advertising - Contact - Frequently Asked Questions - Privacy Policy - Terms of Use - Signup

Contact
tan12V112 Wed May 14 10:56:00 CDT 2008.