Technical Reasoning/Example of Program Validation

An Example of Program Validation

Pseudo-code

For a final example, we will look at a computer program written in pseudo-code.

"Pseudo-code" is a term meaning that the code is not written in an actual programming language. Rather, pseudo-code is like a formal blueprint which could be easily written in any programming language.

Because pseudo-code is not an official or uniformly defined language, but rather something in-between a computer language and a natural human language, there is no one version of pseudo-code.

Therefore everyone has their own system of pseudo-code, and I will describe the one that I find useful for this course.

Assignment and Comparison Equality

Let us begin to contrast two very different kinds of equal signs in pseudo-code.

:=, the assignment operator
=, comparison operator

The choice of these symbols, and the operation that each expresses, is consistent with the OCaml syntax for these concepts.

Both of them have a flavor that is similar to what we mean by "equals", but they each do vastly different things.

The assignment operator takes a variable and assigns to it a value.

So for instance, s := 0 will assign to the variable s the value 0.

The assignment operator requires that the only thing to the left of := is a variable, and the only thing to the right of it is some expression which evaluates to a value. Therefore it is acceptable to have, for example,

s := 1+1

because the expression 1+1 evaluates to the value 2. 2 can then be assigned to the variable.

Now contrast this with the comparison operator. This performs a "test" for equality of two objects.

As a test, it returns a value which may be True or False.

For example,

1 = 1

returns

True

and

1 = 0

returns

False

For comparison, the left-hand side and the right-hand side must each be an expression which evaluates to some value. Therefore

1+1 == 2

returns

True

Lists

The program that we will use below assumes that there is a list of numbers, stored in the variable lst.

The list may be [1,2,3] or it may be [0,-2,-1,-7]. Let us not worry about how the list gets there.

Although the program will assume that some list is stored in the variable lst, it will not make any assumption about which list is there. The program will only assume that lst is filled with numbers that can be added together.

A list essentially represents a collection of data, bundled together. A single list may contain the heights of a bunch of people, or the temperatures for a location over some sequence of days, or anything else.

By putting related data together in a list, is often a signal that somehow the data is related to each other. If the list contains the heights of various people, then by computing the average over the list, one is able to produce the average height for this set of people.

We will not spend much time in this course interpreting the data or values in computer programs. I mention the example of heights only to give a very brief indication of why one might want to bundle data together in the first place.

Structuring and Destructuring

Since lists represent a bundle of information, then it is important to know how one may place data into the bundle and also remove data out of the bundle. One can think of the former as "giving structure" to disparate data, and the later as "removing from structure" or "destructuring" the data in a structure.

Suppose for instance that we want to create a list and place the value 1 in it. One way to do that would be to create an empty list, and then add the value 1 into it. In the code below, I show how one could do this.

Note that the symbol # indicates the start of a "comment". A comment is text inside the program which does not execute, and is only there to help the reader to understand the program.

lst := []        # Create an empty list and place it in the variable lst.
lst.append(1)    # Append the value 1 to lst.

Another more elegant way to do this, is to directly write the data into a list and do the assignment all in one line, like so:

lst := [1]

Now once a list contains values, we can retrieve them by way of indexing.

The very first element of a list is located at "index" zero. For this reason, we say that computer lists are "zero indexed". (There are some programming languages, like R, which do not use zero for the first index of a list. But they are quite rare.)

To access the index 0 of the list lst one writes lst[0]. That is to say, one writes the list, then immediately adjacent to it (with no space) an "open square-bracket", then a number for a position in the list, followed by a close square-bracket.

To demonstrate the use of this, the following program will evaluate to True, because the "zeroth" element of the list is 2, and the "oneth" element of the list is 3.

lst := [2,3,5,7]
lst[1] = 3

For-loops

The code snippet

1. for element e in lst:
2.   s := s+e
3.   s := s+1

is a somewhat random example of a for-loop.

Let us assume, for the current conversation, that the list, lst, is equal to [5,10,15,20]. That is to say, lst = [5,10,15,20]) evaluates to True.

Note: Throughout the rest of this course, I will write something like lst = [5,10,15,20] to tell you what is in a given variable. When I write this, I am essentially telling you that the code expression evaluates to True.

The for-loop is initiated by line 1 in the snippet, which is called the "head" of the for-loop.

Lines 2 and 3 are what we call the "body" of the for-loop. These lines execute repeatedly, in a loop.

What this for-loop does, by a high-level description, is that it takes each element of the list and adds it into the variable s. Then (for no reason other than to show some more lines of code in this demonstration) it also adds 1 to whatever is currently in s.

If you assume that s = 0 before the for-loop initiates, then when the for-loop terminates, s = 54.

At a lower-level description, when a computer runs this code, it maintains an index variable which we cannot see. Let us call the index variable i just so that you and I can talk about it; but of course, there isn't actually a variable i in this program.

First Iteration, i = 0:

When the computer reads the for-loop declaration on line 1, it creates the variable i and initializes its value to 0. Therefore, by the time the computer first reaches line 2, i = 0.

At the same time, it assigns to e the value lst[i]. Therefore, after line 1 is finished, e = 5 for our example.

After it does this on line 1, it moves on to line 2. Here, whatever value was previously stored in the variable s, the computer now uses to evaluate s+e. Finally, still on line 2, the computer uses this value to store it into the variable s, as is instructed by the assignment operator.

In our example, since s = 0 before this line is reached, then it evaluates s+e = 0+5 = 5. (Chaining the equations together is just my shorthand way of telling you that all three of these are equal.) Then due to the assignment operator, this is assigned to s. Therefore after line 2 executes, s=5.

Now line 2 is complete so it moves to line 3, where it takes the content of s, adds 1, and assigns this new value into s. Before line 3 executes, s = 5. After line 3 executes, s = 6.

Now line 3 is complete, which marks the end of the body of the for-loop. Whenever reaching the end of a for-loop, we return to the head of the loop, which is line 1 here.

Second Iteration, i = 1:

We increment the index and reassign the variable e. Therefore, after line 1 finishes executing again, i = 1 and e = lst[1] = 10.

We now proceed again to line 2, after which s = 6+10 = 16.

After line 3 finishes, s = 16+1 = 17.

Third Iteration, i = 2:

Again we return to the head at line 1, after which i = 2 and e = 15. We make another "pass through the body of the for-loop", after which s = 17+15+1 = 33.

Fourth Iteration, i = 3:

Again we return to the head, after which i = 3 and e = 20. We make anther pass through the body, after which s = 33+20+1 = 54.

End:

Again we return to the head, after which i = 4. However, at this point the computer realizes that the list only has four elements and therefore there is no value at i = 4.

Therefore the program ends the for-loop at this point, and moves on to the next part of the program if there is one. (In the code snippet for this example, there is no rest of the program for the computer to move on to. In the example below, there will be.)

The Program

Finally we have reviewed all of the syntax and components needed to analyze the following program.

This program will assume that there is a variable, lst, holding a list of numbers. Intuitively, this program should sum all the elements of the list.

1. let lst be a given list of integers
2. let s := 0 initially
3. for element e in lst:
4.   s := s+e
5. return s

Proof of Validity

When we write a computer program, it is often important to prove the validity of the program.

Not every programmer will write a proof of the correctness of every one of her programs. But it is especially important when a computer system controls something very sensitive and important, like hospital systems or financial records.

Validity

The program above is valid.

Proof

Before the execution of the for-loop, s holds the partial sum of the list lst before index i = 0. This is simply because the sum of no elements defaults to 0.

Suppose that, before iteration number i of the for-loop, s holds the partial sum of lst before index i. Then after iteration i of the loop, s holds the partial sum of the list up to and including index i.

Subproof

By the assumption, s holds the value lst[0]+lst[1]+...+lst[i-1], before the ith iteration. (If i = 0 we understand this to mean that s = 0.)

After line 4 executes, s = (lst[0]+...+lst[i-1])+lst[i]), which shows that s then holds the partial sum of the list up to and including index i.

Because the last iteration occurs at the final index of the list, then when the for-loop terminates, s holds the sum of all the elements in the list.

Since the program then returns s, therefore the program returns the sum over lst.

Admittedly this proof seems very verbose and is probably no clearer than the pseudo-code itself!

However, as programs become more complicated, proofs of validity allow us to summarize and abstract some of the behavior of programs while still arguing for their validity. So as always, this is merely a "toy" example to get us started. As we progress in complexity, the reader should see the value added by performing these proofs.