A magazine about programmers, code, and society. Written by humans since 2018.

How To Reason About Mutable State

The idea, prevalent among those who would prefer you to use functional programming languages, that it is impossible to reason using non-functional programming languages due to the existence of mutable state, is newer than many of the reasoning mechanisms and tools that we use to understand programs that use mutable state.

Let us first unpack the idea of a “functional programming language”, because I am sorry to tell you that there is no such thing. Wikipedia would give you a different impression: it would tell you that programming paradigms are an ontology of programming languages; a categorisation system that lets us say that this language supports this way of writing programs, and that language supports that way of writing.

This clearly does not hold. One of the mathematical statements proved about computer programs even before there were any programmable computers is that any model of computer has, other than physical limitations like size and speed, the capability to run any program written for any other computer. The reason is that any one of these computers can run a program that makes it work like any other one of these computers, then read the program written for the other computer.

Say I have a program for the (virtual) Haskell computer, for example the model of computation exposed by the Haskell programming language. Can I run it on the (equally virtual) Python computer? According to mathematicians Kurt Gödel, Alonzo Church, and Alan Turing, the answer is yes: I can write a Python program that runs Haskell programs (an interpreter) and I can run my Haskell program on that interpreter. When I do so, the Haskell program is running on the Python computer.

So which programming paradigm is Python a member of? The argument above tells us that it must belong to the same paradigm as Haskell. And it also must belong to the same paradigm as Smalltalk, Java, C, Logo, Eiffel, Intercal, COBOL, Algol, APL, Postscript, Raku…

If we want to define a programming language’s “paradigm”, we are going to need a fuzzier, more psychological definition of that language’s paradigm. The programming language makes it easy to express ideas that were formulated using a particular mental toolset. This shows us the underlying truth, wooly though it is: the programmer is thinking about their program in a particular way, and expressing that thought through the medium of the programming language. That means the “paradigm” is actually the mental framework, which is the same meaning of “paradigm” that everybody else who is not a programmer uses. That is beneficial, programmers using words the same way that everybody else does would help in a lot of situations!

Now we could also notice that the paradigms (the thought models) themselves have interchangeable power, which is unsurprising because we are all thinking about programs that we are going to run on interchangeable computers. But we can stop here: what we need to bear in mind is that the paradigm is how we think about the program we are writing. Getting back to our starting point, it is really not true at all that if you are thinking about a program using mutable state, you cannot think about what your program will do.

Here is how it works. Your computer starts in some initial configuration, which we will call the environment, E. You do not have to think of this as the initial state of all the bytes in memory and all the buses and all the CPU registers, because your programming language provides some abstraction over this in terms of named slots or variables. The environment can be the values of the variables in the program, and an idea of what operation will run next. Again, the “what operation” does not have to be a machine instruction that is currently referenced in the instruction pointer or program counter register, it can be a programming language statement or a group of statements like a subroutine, procedure, function, or method.

So the computer runs the operation that should run next, which may take one clock cycle (it almost never does on a modern CPU) or many seconds depending on the complexity of the operation that is coming up. That is not important though, we pretend that the computer atomically “ticks” from E to some new state, E’, which is the values of the variables and the instruction pointer after that operation has completed. For example, if it is the assignment statement x = 3; then E’ is the same as E except for two things: x now has the value 3, and the instruction pointer has moved to the operation after the assignment. If the operation is the go to statement, then the instruction pointer becomes equal to the parameter of the statement and the environment is otherwise unchanged.

These “environments”, the before and after state, can become quite large (though we will see tricks to handle that later in the article), so rather than writing them exactly, we just think about predicates, boolean tests of the environment, and say that we will test the initial environment with one predicate, p, and the resulting environment with another, q. We can then write an assertion about the result of running a statement or subroutine S in the form {p}S{q}. That is: if p is true, and we run S, then q will be true.

This is called a Hoare triple after C.A.R. “Tony” Hoare, and if you have written any form of automated software test then you are already familiar with the Hoare triple. A unit test is “assemble-act-assert”: in other words, get into a state where p, run S, test q. A BDD spec or user story is “given-when-then”: given p, when S happens, then q. The only real difference is that tests specify single examples, where as the predicates in Hoare triples can be general statements about the state of the computer: preconditions that must be true before S to ensure that the postconditions will be true after S.

As I said, the whole environment of the computer, even in the abstract model of a programming language, can be too much to think about, so we have a few tricks to deal with that. The first is structured programming. Dikstra and others explored the composability of these Hoare triples (for example, what happens when you run multiple statements sequentially) and showed how you get from sequences of statements about individual operations to preconditions and postconditions about whole loops, conditionals, and procedures. If you know the behaviour of the instructions in a function, you can gather the initial conditions of those together into a single precondition that must be true before the whole function is run. If you know the outcomes of the instructions, you can gather those together into a single postcondition that will be true after the whole function is run. Now wherever you want to call that function, you do not need to worry about the states of all the variables in the computer: you just need to ensure that the function precondition is true, and that what you do after is compatible with the postcondition being true.

This whole precondition-action-postcondition thing being tedious to write, we call it a contract after the similar real-world idea. A contract says “if you do this for me, then I will do that for you” and that is what it does in software too: if you make sure my preconditions are met, then I will guarantee to satisfy these postconditions.

Object-oriented programming takes this idea of design by contract even further, which is true in all OOP contexts even if it is only made explicit in the Eiffel programming language. Instead of thinking about whole computers, we use encapsulation to break the world up into tiny sub-computers with small environments, and call those tiny sub-computers “objects”. Inside this object, its instance variables are contextually relevant and everything else is out of scope. It will receive some additional parameters via messages, and can send information out via messages, but the only things it needs to track are its ivars. Outside the object, its ivars are off-limits and you can think purely in terms of the contract it exposes.

There is one trick left we need to know about. When we have concurrent threads of execution and shared memory, we cannot rely on arbitrarily bundling up larger and larger operations into atomic changes in environment and pretending nothing else happened in between. That point “and shared memory” is an important one though; with judicious design using encapsulation, you absolutely can treat methods as atomic actions, though you still have to wonder what is going on in the context where all the methods’ effects are being applied. For those times, you have to think about all the different interleavings of operations on different threads and the effects of those sequences on the overall outcome. Is that it, then, is that the death of Design by Contract?

No, that is the time to reach for a computer. Remember those? We use them to render other people unemployed and give them fake news about whose fault it is, all the while pretending they are good tools for enhancing human thought. Well they actually can be used to augment thought, and you can use a computer to enumerate those interleavings and tell you whether a contract ever gets broken. When the functional programmers tell you they do not need to do that, remember to ask whether they or their compiler are doing all the type checking.

Footnote: of course Bertrand Meyer and the folks at Eiffel took a different approach to concurrency: rather than showing whether the contract can be violated for a given specification, they use the contracts to construct a (concurrent) program where violation is impossible.

Cover photo by National Cancer Institute on Unsplash.

Continue reading "Robert L. Glass" or go back to Issue 038: Design By Contract. Did you like this article? Consider subscribing to our newsletter or contributing to the sustainability of this magazine. Thanks!
Back to top