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:insertion_into_doubly-linked_list [2009/03/18 09:35]
vkuncak
sav08:insertion_into_doubly-linked_list [2015/04/21 17:30] (current)
Line 1: Line 1:
 ====== Insertion into Doubly-Linked List ====== ====== Insertion into Doubly-Linked List ======
  
-Doubly-linked list of size 3.+(Figure of doubly-linked list of size 3.)
  
 Code: Code:
Line 21: Line 21:
  
 Where $P$ is Where $P$ is
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
    n \neq null\ \land  \\    n \neq null\ \land  \\
    ​next(n) = null \land prev(n)=null\ \land \\    ​next(n) = null \land prev(n)=null\ \land \\
    ​prev(first) = null\ \land \ Q    ​prev(first) = null\ \land \ Q
 \end{array} \end{array}
-\]+\end{equation*}
 and where $Q$ is and where $Q$ is
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
    ​\forall x.\forall y. prev(x)=y\ \ \rightarrow \\    ​\forall x.\forall y. prev(x)=y\ \ \rightarrow \\
    ​\qquad (y \neq null \rightarrow next(y)=x)\ \land \\    ​\qquad (y \neq null \rightarrow next(y)=x)\ \land \\
    ​\qquad (y = null \land x \neq null \rightarrow (\forall z. next(z) \neq x))    ​\qquad (y = null \land x \neq null \rightarrow (\forall z. next(z) \neq x))
-\end{array}\]+\end{array}\end{equation*}
  
 Corresponding {{sav08:​simpledll.java.txt|Jahob file}} (call it dll-example.java). Corresponding {{sav08:​simpledll.java.txt|Jahob file}} (call it dll-example.java).
 
sav08/insertion_into_doubly-linked_list.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice