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:semantics_of_field_reads_and_writes [2009/03/18 10:02]
vkuncak
sav08:semantics_of_field_reads_and_writes [2015/04/21 17:30] (current)
Line 6: Line 6:
 ++++| ++++|
 Use function update construct: Use function update construct:
-\[+\begin{equation*}
     f = f(x:=y)     f = f(x:=y)
-\]+\end{equation*}
 State variable $f$, which denotes a function, is assigned an updated version of this function. State variable $f$, which denotes a function, is assigned an updated version of this function.
 ++++ ++++
  
-What about null pointer checks? 
- 
-Examples: ​ 
-  y = x.next.next 
-  x.next.next.prev = y 
-  (x = null | x.next == y) 
- 
-Statement simplification. 
- 
-Short-circuit evaluation. 
- 
-Compiler intermediate representation is sometimes more convenient than source code 
-  * or verification system can repeat the compilation process from source to relations (guarded commands) 
-  * [[:​compilation:​top]] 
 
sav08/semantics_of_field_reads_and_writes.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice