Math for CS: State Machines -- Invariants
State machines are a simple, abstract model of step-by-step processes.
One of the most important uses of induction in computer science involves proving one or more desirable properties continues to hold at every step in a process. A property that is preserved through a series of operations or steps is known as a preserved invariant . Examples of desirable invariants include properties such as a variable never exceeding a certain value, the altitude of a plane never dropping below 1,000 feet without the wing flaps being deployed, and the temperature of a nuclear reactor never exceeding the threshold for a meltdown.
Formally, a state machine is nothing more than a binary relation on a set, except that the elements of the set are called “states,” the relation is called the transition relation, and an arrow in the graph of the transition relation is called a transition.
We are given a simple example of a bounded counter, which counts from 0 to 99 and overflows at 100.
We are also given an example of a diagonally moving robot. We come up with some theorems about it and prove one by induction. Then we are introduced to the Invariant Principle.
The Invariant Principle
If a preserved invariant of a state machine is true for the start state, then it is true for all reachable states.
The text shows a brief summary of Robert W. Floyd, the man who formulated the Invariant Principle in 1967.
Die hard example is next. A state machine is formulated based on the riddle from the movie Die Hard. This riddle also comes out in the video game Star Wars, Knights of the Old Republic !
I won’t go into details here, you can look it up.
Floyd distinguished two required properties to verify a program. The first property is called partial correctness; this is the property that the final results, if any, of the process must satisfy system requirements. You might suppose that if a result was only partially correct, then it might also be partially incorrect, but that’s not what Floyd meant. The word “partial” comes from viewing a process that might not terminate as computing a partial relation. Partial correctness means that when there is a result, it is correct, but the process might not always produce a result, perhaps because it gets stuck in a loop.
The second correctness property, called termination, is that the process does always produce some final value. Partial correctness can commonly be proved using the Invariant Principle. Termination can commonly be proved using the Well Ordering Principle.
These are illustrated by verifying the Fast Exponentiation procedure. I think this is a leetcode problem ! Yes, it is implementation of Pow(x, y). Now we get a discrete math perspective using recursion.
The last topic of this lesson is Derived Variables. That is, the technique of assigning values to states. Not necessarily integers and not necessarily decreasing under transitions.
Some of these theorems, like Theorem 5.4.8. - If there exists a strictly decreasing derived variable whose range is a well ordered set, then every execution terminates, remind me of recursion from systematic program design. Maybe some of these theorems can be used to prove that a recursive function will terminate, though it’s not always clear, for example, the hailstone function.
The in class problems look challenging. Going to spend some extra time trying to understand what they are asking, and give it an honest attempt before looking at the solutions and then understanding the solutions.