I began programming in Ada in 1990 but, like many users, it took me a while to become a fan of the language. A brief interlude with Pascal in the early 90’s gave me a better appreciation of the strong-typing aspects of Ada, but continued usage helped me learn many of the other selling points.

I’ve recently started working at AdaCore as a Mentor, which means part of my job is to help companies transition from other languages to Ada and/or SPARK. At my last job, the development environment was mixed C++ and Ada (on multiple platforms) so, to simplify things, we were coding in Ada95. Some of our customers’ code involved Ada2005 and Ada2012 constructs, so I did learn the new language variants and see the benefits, but I hadn’t actually written anything using contracts or expression functions or the like.

We all know the best way to learn is to do, so I needed to come up with something that would require me to increase my knowledge not only of the Ada language, but also to get some more experience with the AdaCore tools (GPS, CodePeer) as well as learning how to prove the correctness of my SPARK code. So I settled on Conway’s Game of Life (Wikipedia). This is an algorithmic model of cell growth on a 2-dimensional grid following four simple rules about cell life and death:

• A live cell with fewer than two live neighbors dies (underpopulation)
• A live cell with two or three live neighbors stays alive (life)
• A live cell with more than three live neighbors dies (overpopulation)
• A dead cell with exactly three live neighbors becomes a live cell (birth)

This little application gave me everything I needed to experiment with, and even a little more. Obviously, this was going to be written in Ada following SPARK rules, so I could program using the latest language variant. The development environment was going to be AdaCore’s GPS Integrated Development environment, and I could use CodePeer for static analysis on the code I was writing, so I could get some experience with these tools. I then could use the SPARK provers to prove that my code was correct. In addition, as Life has a visual aspect, I was able to do a little work with GtkAda to make a graphical representation of the algorithm.

I started with the lower level utilities needed to perform the algorithm – counting the number of live neighbors. Easy, right? Yes, it is easy to code, but not so easy to prove using the SPARK provers. If I wasn’t worried about provability, I could just write a simple doubly-nested loop that would iterate over rows and columns around the target cell, and count how many neighboring cells are alive.

The issue is that, with loops in SPARK, we need to “remind” SPARK what has happened in previous loop iterations (typically using “pragma Loop_Invariant”) so it has all the knowledge it needs to prove the current iteration. This issue is made more difficult when we use nested loops. So, I rewrote my “count all neighbors” routine into two routines - “count neighbors in a row” and “total neighbors in all rows”. Each routine has a single loop, which made specifying the loop invariant much easier.

And that “rewriting” helped reinforce my understanding of “good coding practices”. Most of us were taught that high-complexity subroutines were problematic because they were difficult to test. So we write code that tries to keep the complexity down. The next level in safety-critical software – provability – is also made more difficult by higher complexity subroutines. In my case, my counting routines needed to check to see if a cell was alive and, if so, increment the count. That’s just a simple “if” statement. But, to make it easier on the prover, I created a new routine that would return 1 if the cell was alive and 0 otherwise. Very simple, and therefore very easy to prove correctness. Now, my counting routine could just iterate over the cells, and sum the calls to the function – once again, easier to prove.

Once the low-level functions were created the “real” coding began. And in trying to write pre- and post-conditions for higher level algorithms, I found a great help in the CodePeer tool. This tool performs static analysis on the code base, from simple and quick to exhaustive and slow. The correlation between this tool and the prover tools is that, if I was having a problem writing a valid postcondition, more often than not a CodePeer report would show some warning indicating my preconditions were not complete. For example, every time you add numbers, CodePeer would remind you that a precondition would have to be set to ensure no overflow. Without that warning, everything looks fine, but the prover will not be able to validate the routine. In addition, when using GPS, CodePeer will insert annotations into the Source Code View detailing many of the aspects of each subprogram. These annotations typically include pre- and post-conditions, making it easier to determine which of these aspects could be written into the code to make proving easier.

So, a development cycle was created. First, write a subprogram to “do something” (usually this means writing other subprograms to help!) Next, run CodePeer to perform static analysis. In addition to finding run-time errors, the annotations would help determine pre-conditions for the routines. I would study these annotations, and, for each pre- and post-condition, I had to determine if it made sense or not. If the condition did not make sense, I needed to modify my subprogram to get the correct results. If the condition made sense, then I needed to decide if I wanted to encode that condition using aspects, or just ignore – because sometimes the annotations were more detailed than I needed. Once I got past CodePeer analysis, I would try to prove the subprograms I created. If they could be proven, I could go onto the next step in building my application. If not, I needed to modify my code and start the cycle over.

This process is basically a one-person Code Review! In a large software project, these steps would be the same on some portion of the code, and only then would the code go into a peer review process – with the benefit that the reviewers are only concerned with design issues, and don’t have to be worried about dealing with run-time errors or verifying that the implementation was correct. So, not only did I achieve my objective of learning aspects of the languages and the tools, I got first-hand evidence of the benefits of writing software “the right way!”

To access the source code for this project, please checkout my github repository here: https://github.com/frank-at-adacore/game_of_life