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