Reasoning about side-effects (EECS490Lec18,19)

Mar 30, 2020

I was not present for Lecture 18, which did not get recorded, unfortunately. Thus, this will focus on Lecture 18/19’s content, but might be a bit less on-topic than other lectures.

So last time, we had talked about reasoning equationally w/ side effects on memory.

We want to reason about our functions in some way still, but now we have two separate behaviors to account for:

The functions I/O behavior, which we can reason equationally with using our traditional approach whenever possible
The functions side-effects, which we can reason about by specifying pre-conditions and post-conditions

As an example, we can consider the following:

let counter = ref 0 in
  let tick (n: int) = 
   counter := !counter + n
(Where tick has type int -> unit)

From here, if we only looked at the functional behavior of tick, we could get the following theorem:

$\forall \text{ valuable n : int, tick n }\cong\text{ ()}$

Which really doesn’t tell us much. However, if we now look at the imperative behavior, we could have the following theorem:

If !counter === m, for some m: int, 
   then executing tick n (for some n : int),
   ensures that !counter = m + n

Where we’re essentially saying that, if we execute tick n once, we add n to the counter. This type of logic, where we assume something and, after executing some program, ensure something else, is called Hoare Logic, named after the man that invented QuickSort, among other things. It revolves around Hoare triples, which contain Preconditions, Executables, and Postconditions, in the following syntax:

$\{P\} e \{Q\}$

where, in this case:

P = !counter === m
Q = !counter === m + n
e = tick n

--> {!counter === m } tick n {!counter === m + n}

The way to look at these is that the pre-conditions restrict the starting state, the execution is the program being run, and the post-conditions restrict the ending state assuming the starting state.

So, for example, here are some more valid Hoare Triples:

{T} x := 5 {!x ===5 }
{!x===!y} x:= !x + 3 {!x === !y + 3}
{!x > -1} x != !x - 2 + 3 {!x > 1}

We then define valid Hoare triples as Hoare triples that work in our computational framework, and invalid Hoare triples as those that do not.

Strongest Post-Condition

Now, when reasoning with these new Hoare triples, we now can prove many properties with a single pre-condition. (For example, we can prove, in the first part, that !counter > m-n instead. However, as you can guess, proving this result makes no sense, when you’ve already proven the earlier statement. For this reason, we wish to figure out a way to define the so-called ""Strongest Post-Condition”:

The Strongest Postcondition: The strongest thing, Q, we can conclude about a program given pre-Condition P and executable e.

We can prove that something is the strongest post-condition, Q, if:

Pre-condition P and executable e lead to Q
For all valid post-conditions Q’, Q contains Q’ in some manner ( like how !counter === m + n contains the statement !counter > m - n)

Formally, this translates to the following:

$\{P\}e\{Q\} \text{, and }\forall Q's.t. \{P\}e\{Q'\}, Q'\subset Q$

So, if we had the following sequence of valid Hoare Triples:

{P} e {T}
{P} e {!x > 0}
{P} e {!x===10 or !x===5}
{P} e {!x===10}

Then the last condition would have to be the strongest, as it’s validity implicitly makes the other statements valid as well, as it contains everything else.

Weakest Pre-Conditions

With the strongest-post condition out of the way, there is a similar concept called a “weakest pre-condition” that we can look at. As an example, consider some sorting algorithm, like QuickSort. If we had some imperative implementation of it, it’d probably be a very buggy program, due to how hard it is to write if you haven’t memorized it and due to all of the sub-cases involved, but the strongest post-condition would be that we have a sorted array, as that property encapsulates the goal of such a program.

However, we could easily prove our strongest post-condition using some simple pre-condition, like:

{!my_array = []} sort my_array {!my_array is the 
                  sorted version of the old array}

Obviously, then, we have a problem, as we haven’t proven that our sorting algorithm sorts; only that it sorts with the empty list. So what can we do? We can assume a weaker pre-condition, like the following:

{!my_array is an array} sort my_array {my_array refers to
                     the sorted version of the old array}

Now here, if this Hoare triple is valid, we have achieved the strongest result for any IO pair, proving our sorting algorithm, and its implementation, conclusively, as that is the weakest condition we can assume for our postcondition to hold (although you’d need to more formally encode the notion of a sorted array to put this into Coq or another symbolic logic tool)

Thus, we’ve come up with the idea of the Weakest Pre-condition:

The Weakest Pre-Condition is the most minimal thing you have to assume to make some post-condition hold

Like the strongest post-condition, P , for something to be the weakest pre-condition we need the following:

P, along with the executable e, needs to lead to Q
For any other precondition P’ that also leads to Q given e, P’ must contain P in some way.

Formally, this looks like the following:

$\{P\}e\{Q\} \text{ and } \forall \text{ pre-conditions } P' s.t. \{P'\}e \{Q\}, P \subset P'$

Generally, the closer a function is to real-world usage, the harder this process becomes ( SEE: How do you define what a stack-overflow is formally? ), but this still allows us to reason through our imperative programs in a manner that makes sense, so we’ll use it here.

Lastly, an example of this sort of proof.

Let’s say we had the following, imperative, version of factorial:

let fac ( n : int ) ( r : int ref ) = 
   let k = ref 1 in
     r := 1;
   while (!k < n) do
       k := !k + 1;
       r := !r * !k;
   done

Where the result is stored in the int ref r, so our function has the type signature fac : int -> int ref -> unit .

Obviously, we could prove the following, very important, and very useful theorem about the Functional Behavior of fac:

Forall n : int and r : int ref, fac n r === ()

However, and jokes aside, we’d rather like to prove the following theorem, which conveys the imperative behavior of fac:

If {n >= 1}, then when we executre fac n r (where n : int and r : int ref), 
  we want {!r === n!}.

In Hoare-Triple Form, that’d be:

$\{n \geq 1 \} \text{fac n r} \{ !r = n!\}$

To prove this, what we’re going to do is called forward reasoning. We’re going to start with our pre-condition, n≥1, and move it down each and every line of our program, until we get to the end and (hopefully) prove the post-condition.

{n >= 1}
let k = ref 1 in
{n >= 1 and !k === 1}

Here, as we define a new variable, we need to include that in our context, as it’s a new condition we can assume for the rest of the program.

{n >= 1 and !l === 1}
r := 1;
{n >= 1 and !k === 1 and !r === 1}

Again, here we re-define the input, as the input is a reference, and so we have a new-precondition for the rest of the program.

{n >= 1 and !k === 1 and !r === 1}
{ Loop invariant: {!r === (!k)! and 0 < !k <= n }}
   while (!k < n ) do
...

Before I continue, we’ve now reached a do-while loop in our program, and it’s not entirely obvious how to proceed. What we need to do here is we need to define a so-called loop invariant, or something that holds after each and every execution of the loop.

Loop invariant: Something that stays the same at the beginning and end of every loop

This is really similar to our proofs by induction for functional languages, where we assume Pk-1 and then go to Pk to show something.

If we can assume the loop invariant at the start, and show that the loop invariant holds across each iteration, then we’re get it at the end for free.

Now, this particular loop invariant does hold at the start, as 1! = 1 and as !k ==1, which is less than or equal to n and n is greater than 0, so we’re set here.

So, for this program, we had the above loop invariant. Now, when we proceed, we’ll have the following:

while (!k < n ) do
 {!k < n and !r === (!k)! and 0 < !k <= n }
 i.e. {0 < !k < n and !r === (!k)!}

Then:

{0 < !k < n and !r === (!k)!}
k := !k + 1;
{0 < !k <= n and !r === (!k - 1)!}

as, now that k is incremented, r must be one less than k’s factorial

Then:

{0 < !k <= n and !r === (!k - 1)!}
r := !r * !k
{!r === (!k - 1)! * !k === (!k)! and 0 < !k <= n}

And notice that the loop-invariant still holds! Thus, we’re able to keep it, and can use it to finish off our proof.

Now, we’re exiting the loop, so the while condition must be false. Thus:

{!r === (!k)! and 0 < !k <= n}
done
{!r === (!k)! and 0 < !k <= n and not (!k < n)}
{!r === (!k)! and 0 < !k <= n and !k >= n}
{!r === (!k)! and !k === n}
{!r === (!n)!}, through substitution!

Thus, we’re able to prove this fact, though a few key details are of note:

Like in most of the proofs we have, the proof structure is largely mechanical, making the majority of it a walk in the park, so long as we remember to condense our assumptions
Finding loop invariants, like finding the inductive structure in a problem, can be a very daunting and creative task when presented with an unknown function. We’ll need to be careful to make sure it plays out, as otherwise we’re going to have verification troubles.
As you might have guessed, instead of going forwards through a program, we can also go backwards. This is known as backwards reasoning, and so we’d start with the post-condition and go to a valid pre-condition. This can lead to simpler proofs, but it’s key to remember that this form of reasoning can really take more time to work with, and is a bit less intuitive than forward reasoning.

Lastly, in Lecture 19, Cyrus goes through all of this again, but with one more full example and a half-completed example showing how this could be useful for a more interesting program, reversing an array in-place. For the sake of brevity, I’ll simply type up the former proof to make it easier to look at:

let max ( xs: int array ) = 
    { length(xs) > 0 }
let i = ref 0 in
    {length(xs) > 0 and !i === 0}
let max = ref Int.MinInt in 
    {length(xs) > 0 and !i === 0 and !max === Int.MinInt}
    {LoopInvariant: !max === greatest of xs[0],...,xs[!i-1] and !i <= length(xs)}
while(!i < length(xs)) do
    {!max === greatest of xs[0],...,xs[!i-1] and !i < length(xs)}
    let ith = xs.(i) in
    {ith === xs[!i] and !max === greatest of xs[0],...,xs[!i-1] and !i < length(xs)}
    if (ith > !max) then
      {... and ith > !max}
      !max := ith
      {!max === ith and the rest}
    else 
       {..... and ith <= !max}
       (); 
    {!max == greatest of xs[0]... xs[!i]}
    i := !i + 1
    {!max === greatest of xs[0] ... xs[!i-1]}
done
{!max === greatest of xs[0] ... xs[!i-1] ^ !i >= length(xs) and !i <= length(xs)}
{!max === greatest of xs}

Again, this proof isn’t hard per-se (minus creating and maintaining the loop invariant), but it’s a great one to do to make sure you’re ready for the final, should this appear on it.