on Fri Oct 05 2012, Andrew Sutton <asutton.list-AT-gmail.com> wrote:
Zero breaks the postconditions of division. So?
Not always. Dividing by 0.0 for floating point types is a valid operation resulting in inf.
Yes, I'm talking about ints.
One of the goals of looking at semantics in this way is to help programmers document and better characterize the requirements of their algorithms. An algorithm that computes generically over Fields necessarily excludes NaN as an input and must guard against division by 0. An algorithm that computes over, say, ExtendedReals may allow division by 0, but also excludes NaN. A generic algorithm designed specifically for floating point types allows division by 0 and NaN as inputs.
Right.
The point isn't to change the meaning of existing programs by excluding certain values or expressions. Axioms should present a consistent logical framework that precisely but generally describe the semantics our existing programs. This is not easily done.
I agree; it is not. -- Dave Abrahams BoostPro Computing Software Development Training http://www.boostpro.com Clang/LLVM/EDG Compilers C++ Boost