Less Bugs by using Formal Logic

If you are a Software Developer, chances are you had to debug code at some point in your professional career. This is an article on how to minimise debugging effort by avoiding creating common bugs in software development in the first place.

Boundary Value Error

Chances also are that you have run into a particular breed of common software bugs - one that is called a boundary value error.

Example in Python

Consider the following simple example of such an error in Python:

Now if you call that function to find out if a percentage is in your favor or not, imagine what happens if you call it with

odds_checker(50)

The function would print nothing. Image such a bug in more complex functions with lists and arrays, they would be hard to spot and they are easy to make.

To fix above error, we would have to define a third elif clause which caters for the value 50. Alternatively we would define whether 50 is in favor or against odds and adjust the greater or smaller than sign to incorporate an equality operator, resulting in <= or >=.

Formal Logic

Computer Scientists do mitigate the introduction of such errors by using formal logic, going back to George Boole's The Laws of Thought and even Aristotle.

Connective Meaning Alternative term
and Conjunction
or Disjunction
¬ not Negation
if … then Implication

Table 1.1 - Four logical connectives

Unlike in everyday language the binary and unary operators from above table are given precise definitions in propositional logic. A proposition expresses a truth value, which is either true or false. This can be expressed through truth tables.

Propositional logic does matter in computational thinking, because by applying formal logic to algorithms, you can add precision to their specification, reducing the probability for errors in their implmenentation.

Understanding Propositional Logic

Imagine a sentence, a proposition or an argument. An argument is above all interferable. Interference is achieved if there is no interpratation of the argument for which the premises are true, but the conlcusion is false. Or with the words of Peter Wyss (2013) from the University of Oxford:

Arguments are valid if they do not produce falsehoods from true premises

A Proposition can be expressed as a natural sentence, in philosophy a proposition even has to be expressed that way.

Proposition

A parent promises its child that if she eats her vegetables, she receives some candy

Eating veggies shall be Φ (phi) and receiving candy shall be Ψ (psi). The whole sentence itself would be Φ → Ψ, meaning if the sentence is true, the parent told the truth, and if the sentence is wrong the parent lied.

Consider that the child eats veggies and gets candy, the implication would be the parent is telling the truth, therefore Φ → Ψ = True. Or the parent choses to not honor its promise and withold the candy, then it would be a lie and the sentence (proposition) would be False.

In case the child does not eat her veggies, the parent can withold the candy and the promise (premise) would be True. But in the important case the parent choses to give the candy anyway, the proposition would still be True, because there was no case designed for this in the proposition, the even it is outside the scope of the proposition which is still logically intact.

Φ Ψ Φ → Ψ
True True True
True False False
False True True
False False True

Table 1.2 - Implication and Interference

Applying Logic to Programming

Suppose you have a fairly complex loop guard, like

while (x > y or y > z) or (not x > y and not y > z):

To find out when and when not the guard will evaluate to True, we will use what we just learned about propositional logic.

Let's aggregate the while loop guard a bit. Let Φ be x > y and let be Ψ be y > z. Now we outline the following truth table header:

Φ Ψ ¬ Φ ¬ Ψ Φ ∧ Ψ Φ ∨ Ψ (¬Φ ∨ ¬Ψ) ∨ (¬Φ ∧ ¬Ψ)

Now in order to fill this table quickly and intelligently we use iteration.

Now if you invoke print (truthTableGuardTest()), you will get the correct truthtable.

It is last column which we are interested in, (¬Φ ∨ ¬Ψ) ∨ (¬Φ ∧ ¬Ψ). This is above loop guard while (x > y or.. translated into formal logic. The result will be True for all possible combinations. Congratulations, we just found a bug in the while loop guard. This is what happens: if the condition is met and the program enters the loop, it will never exit and loop forever, because the loop guard always evaluates to True. In formal logic such a behaviour is called a tautology. The opposite of such would be called a contradiction (in case the guard would always evaluate to False).

Pre- and Postconditions

Let's move to another breed of bugs. Imagine a function that finds the highest number of a series of numbers, let them be integers.

Now there is one problem with above function. If you pass it an empty list like findHighest([]), it will return an error and the program will abort. To address this issue you will have to use a pre-condition for the function call or check the condition in the function itself.

Just alter the function with a checking for a pre-condition:

Also in Python you could do an assert len(intList) > 0, which is throwing an assert error if the list is empty. assert can be used to check the internal state of a program with the goal of finding bugs.

You can specify this function in a more mathematical way like this:

Function: FindHighest
Input Sequence of integers I := (i1, i2, i3, …, in)
Output An Integer h
Precondition Length of I > 0
Postcondition h ∈ I and h ≥ ik for all ik in I

In terms of propositional logic we can define precondition P, an algorithm A and a postcondition Q in the following way:

(P ∧ A executes + terminates) → Q

In this way we define clarity in the way of the obligations between the function caller (client) and the function itself (supplier). We also will have the advantage of implementing non-redundancy as well as simplicity, as the program code becomes easier to comprehend and debug.

The opposite of applying formal logic in ones code is called defensive programming and is used quite often, it will slow code down and reduce algorithmic efficency.

Design by Contract

Betrand Meyer developed design by contract, a set of agreements an Abstract Data Type (ADT) offers its clients.

Take Python's ADT Stack for example. If you use one of its operations pop() on an empty stack you will receive an IndexError:

stack = []
stack.pop()

Traceback (most recent call last):
File "<stdin>", line 1, in <module>
IndexError: pop from empty list

In terms of design by contract the stack ADT offers the operation pop() but it lies within the responsibility of the client to ensure the stack to perform pop() upon is not empty. If the caller fails to ensure this, Stack offers no guarantee of successfully returning a result.

If the precondition is met, stack's pop() operation must now honor its side of the contract and must remove and return the top element of the stack and decrease the size of the stack.

ADT Stack
Operation: pop()
Precondition: ¬isEmpty()
Postcondition: Remove & return top element, decrease stack by 1

Please note that in reality there is actually no isEmpty operation in Pyhton, so you could do something like this instead:

not stack
True

We could now define the fictional ADT LimitedStack by an operation push() (in Python's Stack ADT: append()). Imagine our LimitedStack has a maxSize and a isFull operation, the operation for push() would be defined as follows:

ADT LimitedStack
Operation: push(x)
Precondition: ¬isFull()
Postcondition: Append supplied argument to top of LimitedStack, increase size of stack by 1

Inertial Convention is applied, which means above contract are the only changes that are being made.

Obligations and Benefits to the Client and Supplier of the Contract should be clear now. The client has to check that isFull() is False before calling push(x) and the supplier has to add it on top of the stack. The supplier in return don't have to check if the LimitedStack is full.

Design by contract can be expressed in a more general way by a logical sentence, an ADT invariant, an inheritable conditions that applies to all implementations of an ADT, for instance the size of a stack or even LimitedStack can never be negative:

size() ≥ 0

By using preconditions, postconditions and invariants, programmers have a precise way of describing under which condition an operation can be called and what it results can be. This implied contract is always there even if it is not written down, it helps to write code correctly.

Formal Methods make use of design by contract, in order to avoid creating bugs. A whole branch of Computer Science is devoted to the research of formal methods and the ability to prove the corectness of a program mathematically.

This concludes this overview of common bugs in software development and the overview over the logical and mathematical means on how to avoid creating bugs during the process of implementing a system design.

References:

Wyss, P. (2013) First Steps in Formal Logic: Propositional Logic I, Oxford, OUDCE University of Oxford.

Dobbyn, C. (2013) Algorithms, data structures and computability: Iteration and logic, Milton Keynes, The Open University.