How to prove a side effect in a function

Question

I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and databases.

In this question I am wondering about a more middle-level proof, this time about transforming an object $f : A \to B$ with side effect $C$. Say I have as input a string $A$, and as output an Abstract Syntax Tree (AST) $B$. All of this happens in memory with a small string of say a few KB. Right now, ignoring all the details of the hardware implementation and all the details of any particular language.

I am wondering at a high level what it takes to prove something like this. Specifically I wanted to focus on side effects in this question. Say during the parse process, we create a global symbol table to store classes. Then as we are parsing through the code and we encounter the class, we add to the symbol table. So instead of $f : A \to B$, we really have:

\begin{align} f : A &\to B\\ &\downarrow\\ &C \end{align}

That is for the symbol table $C$ and AST output $B$. Somewhere in the function $f$ implementation there is another function $g : \{C,c\} \to C'$, which adds the new symbol $c$ to $C$.

What I would like to prove (in this question, just at a high level, some key points) is that the function generates the symbol table $C$, even though the output of the function is the AST $B$. In type theory, the proof for AST $B$ could possibly just be the sequence of type definitions and transformations, similar to Hoare Logic. But to prove that the function $f$ has side effect $C$ seems much harder/trickier.

It seems that you have to go and step through the algorithm one step at a time, and (assuming everything is strongly typed), figure out what the "current state" would look like at that point (of the whole program). Then you would compare your pattern (the assertion of the post-condition if it were Hoare Logic) with the current state of the program at that point, and see if it was a match. And see if that stayed true until the end of the function/algorithm. But this sort of seems like it's becoming Model Checking, which I only know the basics about, not sure if that is correct to assume though. Also, this one-step-at-a-time stepping through the algorithm seems like program simulation, so wondering if that is true or not or if simulation has a role here.

So I'm wondering, at a high level, what is required to prove that function $f$ generates a side effect $C$. As a specification, I would write "$f$ generates the symbol table $C$".

Answer 1

If the function has two outputs, a standard way to represent this is as a function $f: A \to (B \times C)$, i.e., $f$ outputs a pair of an AST and a symbol table.

If the function updates an existing symbol table, you could represent this as a function $f : (A \times C) \to (B \times C)$. It takes as an input a pair of a string and a symbol table, and outputs a pair of an AST and an updated symbol table.

You could also read about monads, which are a way to structure and reason about side effects in a functional programming language. They are notoriously challenging to understand.

You don't prove a side effect. You can prove a fact about the possible side effects, but you need to state what you are claiming; a side effect isn't something that can be proven or not. Similarly, you don't prove a function. You can prove the correctness of a function, if you specify what correctness means for that particular function, but you don't prove the function.

Answer 2

It depends on how you model the system and what proof approach you're using. For early versions of Hoare Logic, there isn't really any notion of "scope", so there's absolutely nothing special you need to do. You simply have a pre-conditions and post-conditions on the global state. For Hoare Logic, types have nothing to do with it.

In a bit more detail, in a Hoare triple like $\{P\}\ y\,\mathtt{:=}\,f(x)\ \{Q\}$, $P$ and $Q$ are predicates on the entire program state. If $f(x)$ updates some (global) variable, you simply include the appropriate condition in the post-condition $Q$. It's no different than $y$ or any of the other, presumably "local", variables $f(x)$ may mutate.

Most type theories have no notion of mutable state. If you want to talk about mutable state in such systems, you have to model it, e.g. via state passing (i.e. a state monad). In this case, a function $f:A\to B$ which may "mutate" some "global" state may be modeled as a function of type $S\times A\to S\times B$ where $S$ is a type representing "global" state. You can consider more refined versions of this type to capture the actual behavior.