Program Memory as a Graph
Example state of program that inserts new element into doubly-linked list.
Variables in program state:
Total functions (as in predicate logic, to make all variables well-defined).
Special value (constant):
Program state as interpretation in language .
Values of in example state:
- before Insertion into Doubly-Linked List and
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)