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 $x$ is (usually) written as $\lfloor{}x\rfloor$ and it is defined as the greatest integer that is at most $x$. Similarly, the ceiling of a real number $x$ is written as $\lceil{}x\rceil$ and it is defined as the smallest integer that is at least $x$.
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 $x$, we want to calculate an expression $e$ such that:
\[
\lceil{}x\rceil = \lfloor{}e\rfloor ~~.
\]
The ceiling and floor functions
As I said before, the floor of a real number $x$ is the greatest integer that is at most $x$. Formally, we capture this notion in the following definition:
For all real $x$, $\lfloor{}x\rfloor$ is an integer such that, for all integers $n$,
\[
n \leq{} \lfloor{}x\rfloor ~\equiv~ n \leq{} x ~~.
\]
This very compact and elegant definition allows us to derive some properties very quickly. If, for instance, we instantiate $n$ to be $\lfloor{}x\rfloor$, we get:
\[
\lfloor{}x\rfloor \leq{} \lfloor{}x\rfloor ~\equiv~ \lfloor{}x\rfloor \leq{} x ~~.
\]
Since the left side of the equivalence is true, the right side is also true. We thus have our first property:
$\mleq{(0)}{\lfloor{}x\rfloor \leq{} x ~~.}$
Please note that since $n$ is an integer by definition, we can only replace it by integer values. That is why we can replace it by $\lfloor{}x\rfloor$, which is an integer, but we can’t instantiate it to be $x$ because $x$ is a real number. However, we can replace $x$ by $n$, since all integers are also reals. Replacing $x$ by $n$, we get:
\[
n \leq{} \lfloor{}n\rfloor ~\equiv~ n \leq{} n ~~.
\]
which simplifies to
$\mleq{(1)}{n \leq{} \lfloor{}n\rfloor ~~.}$
Now, instantianting $x$ to $n$ in (0), we can also conclude that
\[
\lfloor{}n\rfloor \leq{} n ~~.
\]
Finally, from (1) and (2), we conclude that
\[
n = \lfloor{}n\rfloor
\]
We already knew this property: the floor of an integer number $n$ is $n$.
We can do a very similar analysis for the ceiling function. We’ve seen that the ceiling of a real $x$ is the smallest integer that is at least $x$. So, formally, we have:
For all real $x$, $\lceil{}x\rceil$ is an integer such that, for all integers $n$,
\[
\lceil{}x\rceil{\leq}n~~{\equiv}~~x{\leq}n ~~.
\]
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 $x$, $\lceil{}x\rceil$ is an integer such that, for all integers $n$,
\[
n{\lt}\lceil{}x\rceil~~{\equiv}~~n{\lt}x ~~.
\]
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 $x$ and $y$ are equal if, for all numbers $n$ of the same type as $x$ and $y$, the following holds:
\[
n{\leq}x~~{\equiv}~~n{\leq}y ~~.
\]
Recall that we want to calculate an expression $e$, such that, for a given real $x$:
\[
\lceil{}x\rceil = \lfloor{}e\rfloor ~~.
\]
To use indirect equality, we will prove, for all $n$, the following:
\[
\beginproof
\pexp{n {\leq} {\lceil x \rceil} }
\hint{=}{hint why the step is valid}
\pexp{n {\leq} {\lfloor e \rfloor} ~~.}
\endproof
\]
The detailed proof is as follows:
\[
\beginproof
\pexp{n \leq {\lceil{x}\rceil}}
\hint{=}{integer inequality}
\pexp{n{}1 \lt {\lceil{x}\rceil}}
\hint{=}{contrapositive of ceiling}
\pexp{n{}1 \lt x}
\hintf{=}{$x=\fapp{int}{x}+\fapp{frac}{x}$, where $\fapp{int}{x}$ is the integer part}
\hintl{of $x$ and $\fapp{frac}{x}$ is the fractional part}
\pexp{n{}1 \lt \fapp{int}{x}{+}\fapp{frac}{x}}
\hint{=}{monotonicity: we subtract $\fapp{int}{x}$ from both sides}
\pexp{n{}1{}\fapp{int}{x} \lt \fapp{frac}{x}}
\hint{=}{contrapositive of ceiling}
\pexp{n{}1{}\fapp{int}{x} \lt \lceil \fapp{frac}{x} \rceil}
\hint{=}{monotonicity: we add $\fapp{int}{x}$ to both sides}
\pexp{n{}1 \lt \fapp{int}{x} + \lceil \fapp{frac}{x} \rceil}
\hint{=}{integer inequality}
\pexp{n \leq \fapp{int}{x} + \lceil \fapp{frac}{x} \rceil}
\hint{=}{definition of floor}
\pexp{n \leq \lfloor \fapp{int}{x} + \lceil \fapp{frac}{x} \rceil \rfloor}
\endproof
\]
We have thus proved that:
\[
{\lceil{x}\rceil} = \lfloor \fapp{int}{x} + \lceil \fapp{frac}{x} \rceil ~~.
\]
Note that we still have a problem: our floor expression still involves an application of the ceiling function! However, since
\[
0{\leq}\fapp{frac}{x}{\lt}1 ~~,
\]
we can easily determine the value of $\lceil\fapp{frac}{x}\rceil$ by a simple case analysis. If $x$ is an integer, then $\lceil\fapp{frac}{x}\rceil = 0$, else $\lceil\fapp{frac}{x}\rceil = 1$. Hence,
\[
\if
\beginguards
\gf{\text{$x$ is an integer}}{\lceil{x}\rceil=\lfloor\fapp{int}{x}\rfloor=x;}
\gb{\text{$x$ is not an integer}}{\lceil{x}\rceil=\lfloor\fapp{int}{x}{+}1\rfloor=\fapp{int}{x}{+}1;}
\endguards
\fi
\]
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:
\[
\beginproof
\pexp{n \leq {\lceil{x}\rceil}}
\hint{=}{integer inequality}
\pexp{n{}1 \lt {\lceil{x}\rceil}}
\hint{=}{contrapositive of ceiling}
\pexp{n{}1 \lt x}
\hint{=}{multiply both sides by $1$}
\pexp{n{+}1 \gt x}
\hint{=}{contrapositive of floor}
\pexp{n{+}1 \gt \lfloor{x}\rfloor}
\hint{=}{integer inequality}
\pexp{n \geq \lfloor{x}\rfloor}
\hint{=}{multiply both sides by $1$}
\pexp{n \leq \lfloor{x}\rfloor ~~.}
\endproof
\]
Therefore,
\[
\lceil{x}\rceil = \lfloor{x}\rfloor ~~.
\]
Thanks Rob!
There’s a simpler (IMHO) definition of ceil(x) in terms of floor(x):
For every integer n, n = floor(y). (eq. 2)
By algebra, n = y. (eq. 3)
Substitute eqs. 2 and 3 into eq. 1: for every integer n, n >= floor(y) iff n >= y. (eq. 4)
If predicate p(n) is true for all integers n, then p(n) is also true for all integers n since both n and n are integers. So replace n with n in eq. 4.
For every integer n, n >= floor(y) iff n >= y.
For every integer n, n >= ceil(y) iff n >= y. (def’n of ceil)
Therefore ceil(y) = floor(y).
In perl:
sub ceil {
return ($_[0]
My previous comment got completely hosed because the blog software threw away every lessthansymbol and all following characters until the next greaterthan symbol. Oh well. The point is that ceil(x) = floor(x).
Thanks Rob! I’ve added the proof for your solution to the post. I don’t understand something in your argument, though. In equation 3, you say that n = y. But n is a natural and y is a real. And then you use this for equation 4. I believe the solution is correct, but I don’t understand your proof.
Regarding the lessthan in comments, I’ll try to fix it. Sorry about that!
Pingback: How to be more confident about your own programs an example using  Outdoor Ceiling Fans
Pingback: How to be more confident about your own programs an example using  debt solutions