Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:program_memory_as_graph [2009/03/18 10:38]
vkuncak
sav08:program_memory_as_graph [2015/04/21 17:30] (current)
Line 4: Line 4:
  
 Variables in program state: Variables in program state:
-\[+\begin{equation*}
    ​next,​prev : Obj \to Obj    ​next,​prev : Obj \to Obj
-\]+\end{equation*}
 Total functions (as in predicate logic, to make all variables well-defined). Total functions (as in predicate logic, to make all variables well-defined).
 +
 +We define:
 +  next(null)=null
  
 Special value (constant): $null \in Obj$ Special value (constant): $null \in Obj$
 
sav08/program_memory_as_graph.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice