Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrew Sutton (asutton.list_at_[hidden])
Date: 2012-10-05 16:28:57

> Zero breaks the postconditions of division.  So?

Not always. Dividing by 0.0 for floating point types is a valid
operation resulting in inf. But that only applies to a IEEE floating
point types. Perform the same computation with rational number and you
might get an assertion or exception. But you might not. It depends on
your choice of implementation.

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.

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.