Program Memory as a Graph

Example state of program that inserts new element into doubly-linked list.

Variables in program state:

$\begin{equation*} next,prev : Obj \to Obj \end{equation*}$

Total functions (as in predicate logic, to make all variables well-defined).

We define:

next(null)=null

Special value (constant): $null \in Obj$

Local variable: $n, first \in Obj$

Program state as interpretation $I = (Obj,\alpha)$ in language ${\cal L} = \{ next, prev, null \}$ .

Values of $next,prev,n,first$ in example state:

In general, the declared fields determine

function symbols, constants, and predicate symbols - if we use FOL
variables, if we use HOL (predicate and function symbols become variables, like variables denoting elements)