LARA

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$

Values of $next,prev,n,first$ in the current state.