This is an old revision of the document!

Program Memory as a Graph

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

Variables in program state: \[

 next,prev : Obj \to Obj

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

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, program variables determines

function symbols and predicate symbols for first-order logic formula
variables, if we use HOL (predicate and function symbols become variables, like others)