Re: SPARK and static unit checking?

[roderick.chapman@googlemail.com]

SPARK has a few general princles regarding the arithmetic
operators.

1) They are always "monotonic" meaning they take and return the same
type - the binary operators, for example, always have the signature
  (Left, Right : in T) return T

2) There is no re-declaration, renaming, or user-defined overloading
of the
operators, so "+" _always_ means "arithmetic addition" (which might
be signed integer, modular integer, floating, or fixed, of course...)

3) You can't change the base-name of an operator via a renaming,
which,
as Bob Duff pointed out in another thread, is a dreadful thing to do
anyway.

You can define functions with identifiers for names if you can put
up with having to write "My_Plus (A, B)" instead of "A + B" for
instance.

- Rod Chapman, SPARK Team