Delivering provably-correct code

A while ago on this blog I mentioned the idea that a programmer’s job is not to deliver code, but to deliver provably correct code. Twitter responses ranged from strongly negative (wrong on so many levels I don’t know where to start) to mildly negative (not completely wrong, but incompletely right). There were no positive responses.

The converse of deliver provably correct code is deliver crap code, as I read it. Yet, it seems unlikely that is what those people meant to say. Unfortunately, no one followed up to explain their interpretation. I can only speculate that my choice of words has different implications for them than it does for me.

Since no one wants to explain their interpretation of the phrase, I’ll explain mine.

The key point is that everyone who has a stake in the product needs to feel confident that the code works. Different stakeholders will have different levels of interest in this, and will want assurances of it at different times. To that end, we would like to have reliable, repeatable, easy-to-use, and possibly even automatic means to give people confidence in the code. These methods should not depend on the physical presence of the original author. (Here ends the short version.)

The phrase deliver provably correct code comprises words that are subject to interpretation. The word programmer is also subject to interpretation. Here are my interpretations of the words.

Programmer

Software development calls for the application of several different skill sets. These include such things as analysis, user experience design, data architecture, solution architecture, software design, programming, testing, documentation, deployment, and user training. In very simple cases, a single individual can handle all the development work. This is probably not feasible in an effort of any significant complexity.

When I use the word developer I am thinking of a person who performs one or more of these activities, and who may specialize in as few as one of them. When I use the word programmer I am thinking of a developer whose primary area of specialization is designing and writing the code. Other developers may specialize in different areas, such as software testing, database design, network security, and others. Usually, a subset of these development skill sets is required to deliver a solution. Here we are concerned specifically with the programming skill set.

Deliver

In the context of the phrase, deliver provably correct code, the word deliver means to make your code available to someone else. Your way of working will determine who “someone else” is and at what point they see your code. Here is a non-exhaustive list of possibilities for illustration:

• Traditional environment, old school methods. You work alone. There is no continuous integration. There may or may not be a version control system. If there is, then programmers only check in their code when they believe it is “finished.” No one else sees your code until you declare it is complete enough to be seen. The point you are ready to show your code (or check it in) is your delivery point.
• Collaborative environment, mixed methods. You mainly work alone, but engage other team members as needed. Programmers may check in incomplete code from time to time, but this does not rise to the level of continuous integration. Testers may informally check some of the code before it is formally handed off, on request. Each point when you check in code or show it to a team mate for early testing or for technical collaboration is a delivery point, for purposes of this definition.
• Highly collaborative environment, multi-skilled team members, frequent crossing of “role” boundaries. You mainly code in pairs. Integration and testing are frequent, if not nearly continuous. Team members routinely check in code throughout the day and use feedback from the build to guide their work. You deliver code nearly continuously.

Regardless of exactly how you go about producing code, any time you deliver the code other interested parties need a simple and low-effort way to be confident it is correct, even (or especially) if you are not in the office at the moment.

Correct code

For purposes of this definition, correct refers to functional correctness, and possibly to some basic non-functional requirements. It does not imply the code is production-ready. It is the level of correctness we can expect a professional programmer to provide. It is the level of correctness the code must have before it can be exercised properly by software testing specialists. In a collaborative development environment, it is the level of functional correctness your team mates have a right to expect when they check your code out from version control. Minimally, this includes:

• Code behaves according to expectations through a representative set of sample executions, given both valid and invalid input values, at least at the unit level.
• Code handles border conditions properly.
• Code handles unexpected (but typical) events such as exceptions in a way consistent with the team’s or organization’s standards.
• Code complies with any relevant standards or guidelines for naming, branding, structure, and interaction with other systems in the environment.
• Code deals with well-known technical issues that are not usually explicitly stated in application requirements, but that are expected in professionally-developed code, such as preventing buffer overflow exploits, etc.
• Code supports any relevant governance requirements and regulatory requirements.
• Code provides any relevant “hooks” into enterprise facilities such as auditing, business activity monitoring, or security systems.
• Code satisfies basic non-functional requirements insofar as this can be validated using the tools normally available to programmers.

Whichever of these aspects is relevant to the code you are writing must be in an acceptable state each time you deliver code. If you deliver once a month, you can get away with deferring the non-functional aspects and doing them just prior to delivery. On the other hand, if you are working in a collaborative, rapid-delivery mode, then you will have to learn to build support for these aspects incrementally.

Provable

For purposes of this definition, provable means there is a way for interested parties to assure themselves the code is in acceptable condition at any time. We want this to require a minimum of effort on their part.

Earlier I described the means we use to prove code correctness as “reliable, repeatable, easy-to-use, and possibly even automatic.” When people have to expend additional effort to prove the correctness of the code, they will tend to overlook details or to neglect to do it at all. We want our “proof” to be as painless and mistake-resistant as possible.

What you don’t write, you need not prove

The most automatic, most repeatable, and most reliable way to produce correct code is to avoid writing it altogether. Generally, we can assume code that other people wrote has already been vetted. We only need to worry about code we write ourselves. Depending on the development tools we use, some portion of the solution may be provided without any need for custom code. Those portions of the solution are automatically valid. Different kinds of tools provide different levels of pre-proven code:

• code generator
• service orchestrator
• framework
• callable service
• third-party library
• language features

Code generator

For very straightforward applications with little or no unusual functionlity, it may be possible to use a code generator to produce a complete or nearly-complete solution. For example, Oracle’s Application Development Framework (ADF) can produce a fully-functional CRUD application based on an Oracle database schema. It offers configuration options that allow for customization, and the generated application can be extended with custom code if necessary. Only the custom code has to be “proven” explicitly.

Even custom applications usually contain quite a bit of boilerplate code. Many development tools can generate some or most of this code. Tools like Visual Studio for .NET, IntelliJ and Eclipse for Java, and Ruby Mine for Ruby can produce certain common blocks of code automatically. We need not “prove” this generated code is correct. An example of this is Eclipse’s feature to generate accessor methods for Java classes.

Service orchestration

When reusable components are implemented (or wrapped in) Web Services or RESTful services, some applications (or portions of applications) can be constructed by orchestrating selected services. Products like Microsoft’s BizTalk provide tools to assemble existing services into a meaningful sequence of execution. Tools like Juju support the same approach using cloud services. (This is not meant to be an exhaustive list of products or a recommendation.) When the nature of the problem lends itself to this approach, it may be possible to create a useful solution with a minimum of custom code by orchestrating existing services.

Frameworks

When our solution aligns with a well-known reference architecture, we can usually find frameworks designed to support that architecture. For example, many business applications these days are based on Web technologies. The Model 2 architectural model — a variant of model-view-controller in which the controller and view are tightly coupled — is a popular reference architecture for Web-based business applications. Quite a few frameworks exist that support Model 2, such as Rails, Django, Spring MVC, and JSF, to name just a few.

Provided we take care to keep our application code loosely coupled with our framework-interaction code, we can “prove” our application code without burdensome dependencies on the framework. It also falls to us to prove our application interacts properly with the framework. We need not prove functionality the framework supports directly.

Callable services

Sometimes a portion of our solution requirements can be supported by a third-party component that exposes a public interface. Examples include Web Services, RESTful services, and various forms of RPC-based services. These are loosely coupled with our application code, making it easy to isolate our custom code for explicit “proof” while trusting the third-party components have already been vetted by their owners.

Examples include the Weather Channel’s API for access to weather information, described at http://portal.theweatherchannel.com/, and Google Maps web service APIs described at https://developers.google.com/maps/documentation/webservices/. Any organization that uses a service-oriented architecture will have its own services that are available to application developers, typically providing implementation-independent access to enterprise information assets. Earlier technologies for component-based solutions may still be in use in some environments, as well. These may not be entirely implementation-independent.

Libraries

Third-party libraries that provide utility functions offer a slightly finer-grained level of pre-proven code than services. Libraries typically contain several functions that relate to the same general area of software, such as object-relational mapping, XML processing, mathematical and statistical functions, transforming and formatting data, or wrapping a low-level communication protocol.

With respect to “provability,” libraries have the same general considerations as services. That is, we need not prove the functions work, but we do need to prove our own code behaves properly regardless of what happens when we call a function. Libraries are not implementation-independent, like services. They are packaged in whatever manner works with the given programming language — .NET assemblies, Java packages, Ruby gems, .dll or .so files, etc.

Language features

Programming languages offer various levels of assurance that code written in the language will be “correct” for some definition of correct. Obviously, no programming language can “know” and guarantee the intent of an application. But languages that have strong type systems can provide a level of confidence about correctness.

For example, Idris (see http://idris-lang.org/) supports a strong type system that can assure certain kinds of code correctness. Edwin Brady, the creator of Idris, explains that “dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type.” By virtue of the fact you are writing in a language that supports dependent types, you automatically have a certain level of “proof” of correctness with no additional effort on your part.

Some categories of problems may be solvable using this kind of type system alone, but it has limited application in the business application domain. Even so, similar reasoning applies to more-conventional statically-typed languages, in a much more limited way. A Java collection declared as follows

    List myList = new ArrayList();

might contain objects of any type. If our application requires the collection to contain objects of type Pokemon, then we have to go to some special effort to prove it will always contain objects of that type. We will also have to include logic in the solution to deal with cases when the list contains some other type, and in turn we will have to prove that code is correct. On the other hand, if we declare the list this way

    List<Pokemon> myList = new ArrayList<Pokemon>();

then it is not possible for the application to add any other type of object to the list. We need not “prove” this is true because it is guaranteed by a feature of the programming language.

Proving the correctness of code you can’t avoid writing

Sooner or later, you will arrive at a part of your new application that no one else has already written for you, and that cannot be generated automatically by a tool. When you deliver that code, it has to be provably correct, but it won’t happen automatically. You have to do something to make it so.

Early in the history of computer science, people became interested in the idea of using computer programs to prove the correctness of other computer programs automatically. Seminal papers by Robert Floyd in 1967 and C.A.R. Hoare in 1969 gave the field its start. There is too much material to summarize in a blog post. Please allow me a bit of an oversimplification — if we think of a program execution as a state machine, we can make assertions about the state of the machine before and after the program executes. A formal approach to this makes the process mechanical and therefore programmable. Because they are programmable, formal proofs of this kind can be made automatic. If you want to pursue the formalities further, I suggest the following resources as a starting point:

• http://se.inf.ethz.ch/courses/2012b_fall/sv/slides/02-AxiomaticSemantics.pdf
• http://homepage.cs.uiowa.edu/~slonnegr/plf/Book/Chapter11.pdf
• http://en.wikipedia.org/wiki/Hoare_triple
• http://classes.soe.ucsc.edu/cmps290g/Fall09/Papers/IntroProving.pdf

On a practical level, what we can get from all this when we’re in the middle of a development project in a corporate IT shop is a couple of types of tools for proving the correctness of code.

One type of tool performs a static analysis of the code that can determine whether the code is semantically valid. It consists of a grammar that defines how statements can be codified, axioms that are formulae asserted to be theorems, and inference rules that define mechanical ways to derive new theorems from old ones.

The other type of tool dynamically exercises the code by executing it and making assertions about the state of the system before and after the execution. This seems to be of more practical use in a business software development context than the static analysis type. It does not necessarily prove the code will handle literally every possible input value, but it can go beyond proving just the semantic validity of the code.

Both static and dynamic proofs are expressed as Hoare Triples. The standard notation looks like this:

    {P} C {Q}

where P asserts the precondition, Q asserts the postcondition, and C is the code to be verified. An example might look something like this (not a real language):

    { a > b } 
    begin max(int a, int b) {
        if a >= b 
            return a
        else 
            return b
        end
    end
    { result == a }

This became the basis for development techniques called design by contract and test-driven development, as well as providing the underpinnings for automated unit testing tools. These techniques and tools give us exactly what we need to deliver provably correct code.

Using design by contract, each function or method has a well-defined calling protocol known as a contract. If the type system of the language we are using is robust enough to define the contract completely, we are in good shape. Otherwise, we include assertions in the code to check that callers have adhered to the contract. For example, consider a Java method whose purpose is to average two numerical values.

We specify a contract that the input values must be positive and non-zero floats. The type system of the Java language can guarantee that the input values are floats, but cannot guarantee that they will be positive and non-zero values. We declare the method in a way that exploits the type system as far as it will take us, and we write assertion statements to fill in the rest of the contract:

    public float average(float value1, float value2) {
        assert value1 > 0 : value1;
        assert value2 > 0 : value2;
        return ( (value1 + value2) / 2);
    }

The Java language allows assertions to be enabled or disabled at compile time. We might decide to enable assertions in the test environment and disable them in production for performance reasons. Alternatively we might decide to keep the assertions enabled in production for safety.

Many languages support assertion statements to specify invariants, and something similar to the example above might work just fine, but the example is not ideal for Java. It is not recommended to use assertions to validate method arguments in Java (see this guide for a discussion). One reason is that when an assertion is not satisfied it will throw AssertionError, which is not very descriptive.

In Java, assertions are normally used as a last resort in the default clause of a switch statement or in the last else block in a series of if-else blocks, as a sort of safety valve to protect against proceeding with a routine using dangerously wrong inputs. They aren’t really meant to validate functionality.

We can include conditional logic rather than assert statements to verify that method arguments adhere to the contract:

    public float average(float value1, float value2) {
        if (value1 <= 0 || value2 <= 0) {
            throw new IllegalArgumentException("Arguments to average() must be positive and non-zero; called with " + value1 + " and " + value2);
        return ( (value1 + value2) / 2);
    }

It’s a bit more verbose, but possibly better when we are using Java. Other languages may not have this sort of issue. With this code in place, whenever we run the application it will throw InvalidArgumentException if client code invokes the average() method with inappropriate arguments. That exeption gives us a more precise clue than AssertionError about what’s wrong.

We can provide a higher degree of confidence in the code by verifying this behavior at a finer level of detail. We can write unit test cases to ensure the average() method behaves according to expectations. Unit test cases can be written after the fact or they can be used to drive development of the production code (test-driven development, or TDD).

If you are writing fresh code, consider using TDD. If you are working with existing code, you may need to refactor to break dependencies so that it becomes feasible to write properly-isolated unit test cases.

Unit test cases written for the JUnit test framework might look like this:

	
    @Test
    public void average_returns_the_average_of_two_floats() throws Exception {
        assertEquals(5.0f, average(2.5f, 7.5f), 0.5f);
    }

    @Test(expected=IllegalArgumentException.class)
    public void average_throws_when_first_argument_is_zero() throws Exception {
        average(0.0f, 7.5f);
    }

    @Test(expected=IllegalArgumentException.class)
    public void average_throws_when_first_argument_is_negative() throws Exception {
        average(-1.0f, 7.5f);
    }

    @Test(expected=IllegalArgumentException.class)
    public void average_throws_when_second_argument_is_zero() throws Exception {
        average(2.5f, 0.0f);
    }

    @Test(expected=IllegalArgumentException.class)
    public void average_throws_when_second_argument_is_negative() throws Exception {
        average(2.5f, -1.0f);
    }

The same general idea applies to other Java unit test frameworks and to unit test frameworks for other languages.

This approach provides the repeatability and automation we want, both for checking the basic behavior of the code and for serving as a unit-level regression test suite to help us with future enhancements.

Exploit well-known software design principles

There are various software design guidelines that help us craft clean code. Possibly the most popular set of guidelines for object-oriented design is known as the SOLID principles (see Robert C. Martin’s paper at http://www.objectmentor.com/resources/articles/Principles_and_Patterns.pdf). At the heart of all these ideas is the notion that we should strive for high cohesion and low coupling.

Keeping that basic principle in mind helps us structure our code in a way that makes it easier to deliver provably correct code. One situation in particular is very common — using a framework of some kind in conjunction with custom code. When we use a framework, our application consists of three (at least) distinct types of code:

1. Custom code that we write ourselves;
2. Functionality provided directly by the framework; and
3. The “glue” between 1 and 2.

The functionality provided directly by the framework is code that someone else has kindly written and tested for us. We don’t have to prove it works.

Our custom code is hand-written, and there are no shortcuts for proving it works. A set of well-considered, automated unit tests seems to be the best way to prove the correctness of this sort of code. The unit tests should cover all the issues that are not provided automatically for us by the language’s type system or by our development tools.

The “glue” code should also be covered by automated unit tests, using test doubles for any framework components so that the unit tests can run outside the framework’s usual execution environment. Running the tests outside the normal execution environment means we know the reason for a test failure will be that the code does not behave as expected, and not that we configured the runtime environment incorrectly or some remote resource outside our direct control happens to be unavailable. It also enables unit test cases to run very fast, so that we can include many of them in each build that the continuous integration server starts.

The reason I call out this situation in particular is that I have seen quite a bit of code in the field in which the application logic is tightly intertwined with the “glue” code — webapps that commingle input validation logic with the code to move values in and out of framework-specific containers, database apps that embed product-specific SQL statements directly in the application code, functions or methods that include calls to static methods that are only available in a framework’s runtime environment, etc.

This sort of tight coupling makes it all but impossible to write fine-grained unit test cases that can run independently of the framework’s runtime environment. By implication, it means programmers have no practical way to deliver provably correct code. It is important to maintain loose coupling between the application logic and the “glue” code for interacting with the framework.

Here is a Java example that proves the correctness of the “glue” code in a Portlet filter class, as well as a little bit of custom functionality. A Portlet filter must call the doFilter() method on the FilterChain object that is passed in (glue). Our filter sets an attribute value on the RenderRequest object that is passed in (custom functionality). We assume the framework knows how to instantiate and pass those two objects (framework functionality), so we don’t explicitly verify that behavior.

A Portlet container is not required to run the test because the framework components RenderRequest, RenderResponse, and FilterChain are fake. The test cases demonstrate that the custom code we wrote to interact with the framework does in fact interact with the framework in the way we expect. It’s okay that the framework components are fake because our immediate purpose is not to verify the functionality of the framework itself.

public class SampleRenderFilterTest {

	private SampleRenderFilter filter;
	private RenderRequest request;
	private RenderResponse response;
	private FilterChain chain;

	@Before
	public void before_each_test_case() throws Exception {
		filter = new SampleRenderFilter();
		request = mock(RenderRequest.class);
		response = mock(RenderResponse.class);
		chain = mock(FilterChain.class);
		filter.doFilter(request, response, chain);
	}

	@Test
	public void it_calls_doFilter_on_the_filter_chain() throws Exception {
		verify(chain).doFilter(request, response);
	}

	@Test
	public void it_sets_the_value_of_request_attribute_foo() throws Exception {
		verify(request).setAttribute("foo", "bar");
	}

}

This is the code under test:

public class SampleRenderFilter implements RenderFilter {

	@Override
	public void destroy() {
	}

	@Override
	public void init(FilterConfig arg0) throws PortletException {
	}

	@Override
	public void doFilter(RenderRequest request, RenderResponse response, FilterChain chain) 
			throws IOException, PortletException {
		request.setAttribute("foo", "bar");
		chain.doFilter(request, response);
	}

}

Summary

Depending on the nature of the solution and the development tools in use, we can choose from a range of different ways to provide high confidence in the basic behavior of the code. Code generators, the type systems of programming languages, frameworks, standardized services, and libraries can provide pre-validated building blocks we can use to construct our solutions. When it comes to proving the correctness of code that we write with our own hands, we have to take special measures such as writing automated unit tests. Each of these things takes us part of the way toward provably correct code.

Given the characteristics of our working context, we want to choose the lightest-weight and least-intrusive methods of proof that make sense. We want it to be as easy as possible for people to prove the correctness of the code at any time they need to do so.

An invitation

It’s possible that even after all this explanation, people will consider the idea of delivering provably-correct code incompletely right at best. I invite them to help me make the explanation more completely right, keeping in mind the intended scope of the statement — that is, not intended to assure the code is absolutely production-ready, but just that it is clean enough for others on the team to use with confidence even when the original author is not available for consultation.

It’s possible that people will consider the whole idea to be wrong on so many levels that they don’t know where to start criticizing it. I invite them to imagine, for a moment, that I am their team mate, QA lead, project manager, or key stakeholder, and to explain how they propose to give me confidence that their code is correct, if not by using one or more of the means described here.

I look forward to learning.