Re: pre- and post-conditions

mathewji <itoneymathew@gmail.com> writes:


  Good. Now write (this addresses all readers of this post,
  not just mathewji) a function

long long average( long long j, long long k );

  precondition: LLONG_MIN <= j, k <= LLONG_MAX

  postcondition: average( j, k ) is the smallest (nearest to
  minus infinity) of all the long long values that are closest
  to the mathematical value of (j+k)/2.

  The function should be coded in such a way that the
  postcondition is true under every C implementation.

  For example:

average( LLONG_MAX, LLONG_MAX ) == LLONG_MAX
average( LLONG_MAX - 1, LLONG_MAX - 1 ) == LLONG_MAX - 1
average( LLONG_MIN, LLONG_MIN ) == LLONG_MIN
average( LLONG_MIN, LLONG_MAX ) == should usually be a value near 0
average( LLONG_MAX, LLONG_MIN ) == should usually be a value near 0
average( j, j ) = j
average( 2, 3 ) = 2
average( -2, -3 ) = -3
average( 2, 4 ) = 3
average( -2, -4 ) = -3

  (The implementation written can choose another means to choose a
  value: For example, instead of ?smallest? above, also the
  ?largest? value might be chosen, so that average( 2, 3 ) is 3.
  This choice has to be documented.)

                ~~~~~~~~~~~~~~

  Extra points are given when floating-point types are not used
  in the implementation. The following program prints ?0? here:

#include <stdio.h>
#include <limits.h>
int main( void )
{ printf( "%g\n", ( double )LLONG_MAX - ( double )( LLONG_MAX - 5 )); }

  which shows that double can't represent all the long long
  values anyways. And this

#include <stdio.h>
#include <limits.h>
int main( void )
{ printf( "%Lg\n", ( long double )LLONG_MAX - ( long double )( LLONG_MAX - 5 )); }

  prints ?1.13305e-317? here. But it is possible that my C
  implementation is buggy with regard to some floating point
  calculations as I observed before. I just tested it with
  another compiler, and it printed ?0? for the first program
  and ?5? for the second.

  I don't know whether there is a portable guarantee that all
  long long values can be represented in a long double, but I
  doubt that there is such a guarantee.