How to deal with arrays during Hoare-style correctness proofs

Question

In the discussion around this question, Gilles mentions correctly that any correctness proof of an algorithm that uses arrays has to prove that there are no out-of-bounds array accesses; depending on the runtime model, this would cause a runtime error or access to non-array elements.

One common technique to perform such correctness proofs (at least in undergrad studies and probably in automated verification) is by using Hoare logic. I am not aware that the standard set of rules containes anything relating to arrays; they seem to be restricted to monadic variables.

I can imagine adding axioms of the form

$\qquad \displaystyle \frac{}{\{0 \leq i \lt A.\mathrm{length} \land {P[A[i]/E]} \}\ A[i] := E;\ \{P\}}$

However, it is not clear to me how you would deal with an array access on the right hand side, i.e. if it is part of a complex expression $E$ in some statement $x := E$.

How can arrays accesses be modelled in Hoare logic so that the absence of invalid accesses can and has to be proven for program correctness?

Answers may assume that we disallow array elements to be used in statements other than $A[i] := E$ or as part of some $E$ in $x := E$ as this does not restrict expressiveness; we can always assign a temporary variable the desired value, i.e. write $t := A[i];\ \mathtt{if} ( t > 0 ) \dots$ instead of $\mathtt{if} ( A[i] > 0 )\dots$.

Answer 1

Your axiom is not really an axiom, it's missing hypotheses. Simple presentations of Hoare logic manipulate formulas of the form $\{P\} C \{P'\}$ where $P$ and $P'$ are logical formulas and $C$ is a command. You do need to ensure that $C$ is well-formed. In simple languages such as the ones often used for a first introduction to Hoare logic, well-formedness is syntactic: it's typically a matter of checking that $C$ conforms to a context-free grammar, and possibly that the free variables are within a permitted set. If the language includes constructs that have a semantic correctness, such as accesses to array elements, you need to add hypotheses to express this semantic correctness.

Formally, you can add judgements to express the correction of expressions and commands. If expressions have no side effects, they need no postconditions, only preconditions. For example, you can write well-formedness rules such as $$ \dfrac{\{P\} \;\; E \text{ wf}} {\{P \wedge 0 \le E < \mathrm{length}(A)\} \;\; A[E] \text{ wf}} \qquad \dfrac{\{P\} \;\; E_1 \text{ wf} \qquad \{P\} \;\; E_2 \text{ wf}} {\{P\} \;\; E_1 + E_2 \text{ wf}} $$ and only allow well-formed expressions in commands: $$ \dfrac{\{P[x\leftarrow E]\} \;\; E \text{ wf}} {\{P[x\leftarrow E]\} \;\; x := E \{P\}} $$

A different approach is to treat all expressions as well-formed, but to make any expression involving an ill-formed calculation have a special value $\mathbf{error}$. In languages with run-time bounds checking, $\mathbf{error}$ means “this program raised a fatal exception”. You would then keep track of whether a program errored out through a logical predicate $\mathbf{Error}$; a program is only valid if you can prove that its postcondition implies $\neg\mathbf{Error}$. $$ \dfrac{} {\{P[x\leftarrow E]\} \;\; x := E \;\; \{P \vee \mathbf{Error}\}} \qquad \dfrac{P[x\leftarrow E] \implies E \not\rightarrow \mathbf{error}} {\{P[x\leftarrow E]\} \;\; x := E \;\; \{P\}} $$

Yet another approach is to consider a Hoare triple to hold only if the program terminates correctly. This is the usualy approach for nonterminating programs: the postcondition holds when the command terminates, which might not always happen. If you treat run-time errors as non-termination, you sweep all correctness issues under the hood. You will still need to prove the correctness of the program somehow, but it need not be in Hoare logic if you prefer some other formalism for that task.

By the way, note that expressing what happens when a compound variable such as an array is modified is more involved that what you wrote. Suppose $P$ was, say, $\mathrm{IsSorted}(A)$: the substitution $A[i]\leftarrow E$ would not change $P$, yet the assignment $A[i] \leftarrow P$ might invalidate $P$. Even if you restrict the syntax of predicates to only talk about atoms, consider the assignment $A[A[0]-1] := A[0]$ under the precondition $A[0] = 2 \wedge A[1] = 3$: you cannot make a simple substitution to obtain the correct postcondition $A[0] = 1 \wedge A[1] = 1$, you need to evaluate $A[0]$ (which can be difficult in general, since the precondition might not specify a single possible value for $A[0]$). You need to perform the substitution on the array itself: $A \leftarrow A[i\leftarrow E]$. Mike Gordon's lecture notes have a good presentation Hoare logic with arrays (but without error checking).

Answer 2

As mentioned by Gilles, there is an array assignment axiom (see Gordon's notes, Sec. 2.1.10): $$ \dfrac{} {\{Q[A \mapsto A.store(i,expr) ] \} \;\; A[i] = expr \;\;\{ Q \}} $$ In words, if you have an array assignment, then replace the original array by array A.store(i,expr) which has at position i the value expr. Note that if you already have A.store(i,vi) on the post, and assign A[j]=vj, then you should get A.store(j,vj).store(i,vi) as the pre (yes, in this order -- recent update is executed first!).

Additionally, we need the array access axiom: A.store(i,v)[i] can be replaced by v ("if you access $i$th element that you just updated, then return the assigned value").

I think in order to prove a program with arrays is correct ("no out-of-bound accesses"), the above axioms are enough. Let's consider the program:

...
A[i] = 12
...

We would annotate this program:

...
@ {0<i<A_length}
A[i] = 12
...

where A_length is a variable that specifies the array length. Now try to prove the annotation -- namely, work it out backwards (from bottom to top, "as usually" in Hoare proofs). If on top you get {false}, then the out of bound access can happen, otherwise, the expression you got is the precondition under which no out-of-bound accesses are possible. (also, we need to ensure that when array is created like int A=int[10]; then in the post-condition we have {A_length==10}).