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
|
