LARA

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)