Lab for Automated Reasoning and Analysis LARA


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]
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
    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}
 and where $Q$ is and where $Q$ is
    ​\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))
 Corresponding {{sav08:​|Jahob file}} (call it Corresponding {{sav08:​|Jahob file}} (call it
sav08/insertion_into_doubly-linked_list.txt · Last modified: 2015/04/21 17:30 (external edit)
© EPFL 2018 - Legal notice