LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Next revision Both sides next revision
sav08:program_memory_as_graph [2008/04/08 20:03]
vkuncak
sav08:program_memory_as_graph [2009/03/18 10:38]
vkuncak
Line 15: Line 15:
 Program state as interpretation $I = (Obj,​\alpha)$ in language ${\cal L} = \{ next, prev, null \}$. Program state as interpretation $I = (Obj,​\alpha)$ in language ${\cal L} = \{ next, prev, null \}$.
  
-Values of $next,​prev,​n,​first$ in example state.+Values of $next,​prev,​n,​first$ in example state
 +  * before [[Insertion into Doubly-Linked List]] and 
 +  * after 
 + 
 +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)