Quick: how do you sort three numbers in ascending order?

Here is an excerpt from the first page returned by Google.

```
! -------------------------------------------------------
! This program reads in three INTEGERs and displays them
! in ascending order.
! -------------------------------------------------------
PROGRAM Order
IMPLICIT NONE
INTEGER :: a, b, c
READ(*,*) a, b, c
IF (a < b) THEN ! a < b here
IF (a < c) THEN ! a < c : a the smallest
IF (b < c) THEN ! b < c : a < b < c
WRITE(*,*) a, b, c
ELSE ! c <= b : a < c <= b
WRITE(*,*) a, c, b
END IF
ELSE ! a >= c : c <= a < b
WRITE(*,*) c, a, b
END IF
ELSE ! b <= a here
IF (b < c) THEN ! b < c : b the smallest
IF (a < c) THEN ! a < c : b <= a < c
WRITE(*,*) b, a, c
ELSE ! a >= c : b < c <= a
WRITE(*,*) b, c, a
END IF
ELSE ! c <= b : c <= b <= a
WRITE(*,*) c, b, a
END IF
END IF
END PROGRAM Order
```

```
int a, b, c;
#define swap(x, y) do {int tmp; tmp = x; x = y; y = tmp; } while (0)
if (b < a) swap(b, a);
if (c < b) swap(c, b);
if (b < a) swap(b, a);
```

```
if (b < a) swap(b, a);
if (c < b) swap(c, b);
if (d < c) swap(d, c);
if (b < a) swap(b, a);
if (c < b) swap(c, b);
if (b < a) swap(b, a);
```

Nevertheless, there's still one more question: How do we come up with the above solutions, and how do we know they are correct?

The answer is also simple, and it is called *abstract interepretation*.
We simply write a program that performs the
bubble sort
algorithm
(this is how the above code snippets work),
but we substitute the loop's innermost statement with a print statement.
Here is the code:

```
main()
{
int i, j;
const int n = 4;
for (i = 0; i < n - 1; i++)
for (j = 0; j < n - 1 - i; j++)
printf("if (%c < %c) swap(%c, %c);\n",
'a' + j + 1, 'a' + j, 'a' + j + 1, 'a' + j);
}
```

Read and post comments, or share through

Navigation

Tagged as

Recent posts

Was Knuth Really Framed by Jon Bentley?
(2020-02-25)

Convert file I/O into pipe I/O with /dev/fd (2019-12-14)

Pia Betton on Service Design (2019-12-05)

How to monitor MySQL / MariaDB query progress (2019-11-03)

So, you're chairing a conference session? (2019-05-29)

Java Stream Methods and Unix Pipeline Commands: A Dictionary (2018-11-27)

Debugging had to be discovered! (2018-11-16)

How I slashed a SQL query runtime from 380 hours to 12 with two Unix commands (2018-08-05)

How to Perform Set Operations on Terabyte Files (2018-04-03)

The Shoemaker's Children Go Barefoot (2018-02-10)

Convert file I/O into pipe I/O with /dev/fd (2019-12-14)

Pia Betton on Service Design (2019-12-05)

How to monitor MySQL / MariaDB query progress (2019-11-03)

So, you're chairing a conference session? (2019-05-29)

Java Stream Methods and Unix Pipeline Commands: A Dictionary (2018-11-27)

Debugging had to be discovered! (2018-11-16)

How I slashed a SQL query runtime from 380 hours to 12 with two Unix commands (2018-08-05)

How to Perform Set Operations on Terabyte Files (2018-04-03)

The Shoemaker's Children Go Barefoot (2018-02-10)

Last modified: Thursday, November 17, 2005 10:01 am

Unless otherwise expressly stated, all original material on this page created by Diomidis Spinellis is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.