João Ferreira

Programming is one of the most difficult branches of applied mathematics; the poorer mathematicians had better remain pure mathematicians.

It was Edsger W. Dijkstra, the famous computer scientist, who wrote these words in his note named “How do we tell truths that might hurt?“. I am sure that many people didn’t like to read them, and didn’t understand what he meant.

Although it is not my intention to discuss his words, I want to present a simple example that demonstrates how mathematics can be used to program better and to make you more confident about your own programs.

This post includes a fair amount of mathematical definitions and concepts, but they should not be difficult to understand. After the mathematical discussion, I present an example using the Perl programming language (it also applies to languages like C or Java).

The Problem

The problem I am going to deal with, involves the ceiling and floor functions. If you don’t remember, the floor of a real number is (usually) written as and it is defined as the greatest integer that is at most . Similarly, the ceiling of a real number is written as and it is defined as the smallest integer that is at least .

The goal is to implement the ceiling function supposing that our programming language only provides the floor function to round numbers. Formally, given a real , we want to calculate an expression such that:

The ceiling and floor functions

As I said before, the floor of a real number is the greatest integer that is at most . Formally, we capture this notion in the following definition:

For all real , is an integer such that, for all integers ,

This very compact and elegant definition allows us to derive some properties very quickly. If, for instance, we instantiate to be , we get:

Since the left side of the equivalence is true, the right side is also true. We thus have our first property:

Please note that since is an integer by definition, we can only replace it by integer values. That is why we can replace it by , which is an integer, but we can’t instantiate it to be because is a real number. However, we can replace by , since all integers are also reals. Replacing by , we get:

which simplifies to

Now, instantianting to in (0), we can also conclude that

Finally, from (1) and (2), we conclude that

We already knew this property: the floor of an integer number is .

We can do a very similar analysis for the ceiling function. We’ve seen that the ceiling of a real is the smallest integer that is at least . So, formally, we have:

For all real , is an integer such that, for all integers ,

Note that we can apply the contrapositive rule (that’s when we negate both sides) to this definition. Doing that, we get the equivalent definition:

For all real , is an integer such that, for all integers ,

I leave as an exercise to prove the dual properties of the ones we’ve seen for the floor function.

Indirect equality and the solution to the problem

Ok, so now that we have seen the formal definitions of the ceiling and floor functions, we can proceed. Note that these definitions have the aproppriate shape to use the proof technique named Indirect Equality. Briefly, the rule of Indirect Equality claims that two numbers and are equal if, for all numbers of the same type as and , the following holds:

Recall that we want to calculate an expression , such that, for a given real :

To use indirect equality, we will prove, for all , the following:

The detailed proof is as follows:

We have thus proved that:

Note that we still have a problem: our floor expression still involves an application of the ceiling function! However, since

we can easily determine the value of by a simple case analysis. If is an integer, then , else . Hence,

An example in Perl

An example of a language that does not provide a native function ceiling is Perl. The only native function related with rounding numbers (as far as I know) is the function int. This function is a mixture of the floor and ceiling function: for positive numbers it behaves as the floor function and for negative numbers it behaves as the ceiling function. This means that to solve the problem in Perl, we just have to worry about positive arguments!

Therefore, from our previous analysis, we can write a correct implementation of the ceiling function as follows:

sub correct_ceil {
  my $r = shift;
  my $frac = $r - int($r);
  if($frac<=0) {
    return int($r);
  } else {
    return 1+int($r);
  }
}

And that’s it! We have a real proof that this function is correct! Although the problem is simple, it is very common to make mistakes. As an example, I found the following wrong ceiling implementation in a programming forum:


# ceil() funtion to use instead of loading in
# the POSIX module each time
{
local ($amount) = @_;
$floor = int($amount);
$ceil = int($amount + 0.5);
if ($ceil == $floor)
{
$ceil++;
}
return $ceil;
}


Clearly, this function does not work for integer arguments! I just hope it is not being used anywhere

Note: in Perl you can import the module Posix and use the function ceil, but our goal was to write the ceiling function knowing that the floor function is defined.

Conclusions

The main goal of this post was to show how mathematical arguments can be used to give us confidence in our own programs. I’m aware that, although the ceiling and floor functions are widely used (in financial applications, for instance), this example could be presented in a different way. The most obvious drawback is that the main proof is quite long; it could be shortened, but I would have to omit some intermediate steps.

On the positive side, once we adopt the definitions given, most part of the proofs involving the ceiling and floor functions become similar, and thus systematic. This allows us to reuse the proof techniques over and over again.

I hope you have enjoyed the post and I’d be glad to get some comments!

A much better solution by Rob Mayoff

Rob Mayoff proposed a much better solution (see comments) to this problem! A proof of his solution can be:

Therefore,

.

Thanks Rob!

Related Articles:

• On Programming and Mathematical Methodology -- Part II
• On Programming and Mathematical Methodology