Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:insertion_into_doubly-linked_list [2009/03/18 09:36] vkuncak |
sav08:insertion_into_doubly-linked_list [2015/04/21 17:30] (current) |
||
---|---|---|---|
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). |