Eric Northup wrote: >... > >>The static type >>checker would catch any usage violating this. Then for >>wrap around, aka a ring, ring+, ring- etc. Then for >>exceptions on overflow or underflow, have bounded+, >>bounded-, etc. >> > >I doubt that a static check is possible in the general >case. I suspect it will end up being the halting problem. >For some cases, a proof can be constructed that overflow >never occurs, and thus need not be checked at runtime. >But what about the others? I want our type-checker to >terminate! > > > My reasoning for preferring 'throw-exception'-style >operators is that programmers who were not considering >problems of overflow will be reminded when it gets the >exception. Programmers who _were_ considering overflow >have explicitly marked their intention by using the >wrap-around version of the operators. > But, getting a run-time exception is a little too late. The product was shipped, and the software (aircraft controller?) crashed. And, if there is a proof obligation to show that the exception will never occur, we are back to the same halting problem.
Probably, the best solution in the case of non_mod_+ and non_mod_- is that if the compiler (to be understood as compiler-prover combination) is unable to trivially (for large values of trivially, which is decidable) show that the expression is guaranteed not to overflow, then it is a compile time error, and the programmer should choose the mod_+ and mod_- operators instead. >... > >But I don't care >too strongly as long as both forms can be read unambiguously >and typed without contributing to repetitive-stress >injuries. > I second your opinion. Swaroop. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
