Beware: Spoilers for Advent of Code Day 3 ahead!
Also: Don’t read this on mobile, math typesetting is hard on small screens :(
I’m doing Advent of Code again this year, and part 1 of today’s problem reminded me immediately of some of the problems I’m doing in my Program Construction module at UCD. In the class, we cover the foundations of Edsger W. Dijsktra’s Structured Programming. It teaches you how to formally verify your program by finding the pre-conditions and post-conditions, then deriving and proving theorems that build up towards the final program.
It’s a very different style of thinking about programming than most people are used to, but I’ll try my best to explain the notation and the logic I’m using.
We start out by writing our post-condition. This is what we want to be true once our program has finished running — in other words, it’s what we want to calculate. We’re going to use this funky-looking syntax called Quantified Notation.
As an intro, here’s a basic quantified expression:
< + i : 0 ≤ i < N : f . i > <+\;i : 0 \leq i < N: f.i> <+i:0≤i
f . i f.i f.i is the syntax we’ll use for accessing the i t h i^{th} ith element of some array f f f. This is simply shorthand for this longer expression:
f .0 + f .1 + f .2 + f .3 + ⋯ + f . ( N − 1 ) f.0 + f.1 + f.2 + f.3 + \dotsb + f.(N - 1) f.0+f.1+f.2+f.3+⋯+f.(N−1)
For those of you more familiar with functional programming, you’ll find that this is just a reduction over a list. f f f is the list in question and + + + is the operation we want to use to combine each element with the accumulator. However, program construction is designed around an imperative language, and so we need an index variable i i i to keep track of our position in the array. We also have to specify the range of i i i, which is from 0 0 0 to the length of the array.
... continue reading