A question has arisen concerning arithmetic on primary types. I have a
strong opinion, but that doesn't make me right.
The question may be summarized by example. Should the addition operator
+: int32 x int32 -> int32
be defined as performing modular arithmetic, or should it be defined as
performing a run-time bounds check and possibly an exception throw?
It is clear that we need both in certain cases, and a parallel set of
operators for modular arithmetic (+%, -%, etc.) has been proposed.
Obviously we will need names for the checking versions as well. In honor
of their proposer, I am contemplating (markm+, markm-, etc.), but I will
get over it.
The only question here is: what should the default behavior for '+' be?
One bit of possibly relevant empirical information: Ada defines these
operators to check for overflow. The Spark/ADA people have been
relatively successful at proving theorems of the form
(defthm no-overflows
(not (throws arithmetic-overflow (eval {(main)}))))
[sorry about the wacky syntax]. Note that if this theorem can be
discharged, the checks can be entirely removed by the compiler. More
locally, they can be removed by the compiler in all of those specific
cases where they can be shown not to occur.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
