(Image by Leonardo Solaas)

[hamzh_toggle title=”Series Parts” state=”closed”]

• Part 1 – Execution Tables
• Part 2 – Trace Tables
• Part 3 – Karnaugh Maps

[/hamzh_toggle]

Welcome back! In the previous article I explained why you might be interested in software verification techniques and then showed you how to use Execution Tables to verify your software for specific cases.

In this article, we’ll generalize Execution Tables into a format that will allows us to create simple inductive proofs about our loops.

Trace Tables

To demonstrate this technique, we’ll use some code from a previous blog post I wrote about fixing Python’s str.title() function. As a refresher, here is the code from that post:

import re
 
def fixed_title(input_string):
    parts = re.split(r'\s', input_string)
 
    for idx, value in enumerate(parts):
        if re.match(r'[A-Za-z]', value[0]):
            parts[idx] = value[0].upper() + value[1:]
 
    return ' '.join(parts)

When constructing a trace table, we begin by enumerating all the logical cases we want to check. Let’s try to be exhaustive here:

• The empty string
• A single non-space character
• A single space character
• Single word with single spaces
• Single word with multiple spaces
• Multiple words with single spaces
• Multiple words with multiple spaces

Now we construct a simple trace table for each non-trivial case, I won’t do all the cases here, but let’s pick the non-trivial example of a string with 3 leading spaces and a word:

[table id=1 use_datatables=False]

As you can see, we take the loop through multiple cycles until it terminates. When it terminates, we have the final state of all the variables after loop execution.

In the article the code comes from we were interested in correcting a very particular string, “West 62nd st.”, let’s generalize this string and use it to verify that our code does what we expect it to do:

[table id=2 use_datatables=False]

Sure enough, it looks like it works for our example case.

Inductive Proofs

It’s not too far of a stretch to see how this could be used to perform proofs by induction. Simply:

• Test the function for some known value to verify that it works.
• Assume the function works as expected for some value n.
• Show that the function works for n+1.

Conclusion

We have now seen how we can generalize symbolic execution tables into a format that allows us to construct simple inductive proofs about our programs. These kinds of proofs can be constructed and reviewed in a few minutes, and provide us some level of formal assurance about the validity of our programs.

In the next article we’ll see a technique that we can use to validate programs that have state-machine like behavior.