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):
Local variable:
Program state as interpretation in language .
Values of 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)