LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:program_memory_as_graph [2008/04/08 20:03]
vkuncak
sav08:program_memory_as_graph [2015/04/21 17:30]
Line 1: Line 1:
-====== 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.