example in full
swap procedure
List swap (List c) { List p; if (c != null) {
p = c ;
c = c.next ;
p.next = c.next ;
c.next = p ; }
return c;
}
translation
no derefs ? ((c != null ? (
p’ = c ? c’ = c ? all x | x.next’ = x.next ;
c’ = c.next ? p’ = p ? all x | x.next’ = x.next ? derefs’ = derefs + c ;
p.next’ = c.next ? p’ = p ? c’ = c ? all x | x != p -> x.next’ = x.next ? derefs’ = derefs + c + p ;
c.next’ = p ? p’ = p ? c’ = c ? all x | x != c -> x.next’ = x.next ? derefs’ = derefs + c )
? (c = null ? p’ = p ? c’ = c ? all x | x.next’ = x.next ? derefs’ = derefs )) ;
result = c