assume P;
   if (first == null) {
     first = n;
     n.next = null;
     n.prev = null;
   } else {
     n.next = first;
     first.prev = n;
     n.prev = null;
     first = n;
   }
   assert Q;

Where is \[\begin{array}{l}

 n \neq null\ \land  \\
 next(n) = null \land prev(n)=null\ \land \\
 prev(first) = null\ \land \ Q

\end{array} \] and where is \[\begin{array}{l}

 \forall x.\forall y. prev(x)=y\ \ \rightarrow \\
 \qquad (y \neq null \rightarrow next(y)=x)\ \land \\
 \qquad (y = null \land x \neq null \rightarrow (\forall z. next(z) \neq x))

\end{array}\]

Corresponding Jahob file which verifies quickly using e.g.

jahob.opt dll-example.java -method Simple.add -usedp cvcl

How can we build a verification conditions for such programs?