examples/linked_list_rev.mlw

   1
   2
   3 (**
   4
   5 {1 In-place linked list reversal }
   6
   7 Version designed for the {h <a href="http://www.lri.fr/~marche/MPRI-2-36-1/">MPRI lecture ``Proof of Programs''</a>}
   8
   9 This is an improved version of {h <a href="linked_list_rev.html">this
  10 one</a>}: it does not use any Coq proofs, but lemma functions instead.
  11
  12 *)
  13
  14
  15
  16 module InPlaceRev
  17
  18   use map.Map
  19   use ref.Ref
  20   use int.Int
  21   use list.List
  22   use list.Quant as Q
  23   use list.Append
  24   use list.Mem
  25   use list.Length
  26   use export list.Reverse
  27
  28   type loc
  29
  30   val function eq_loc (l1 l2:loc) : bool
  31     ensures { result <-> l1 = l2 }
  32
  33   val constant null : loc
  34
  35   predicate disjoint (l1:list loc) (l2:list loc) =
  36     forall x:loc. not (mem x l1 /\ mem x l2)
  37
  38   predicate no_repet (l:list loc) =
  39     match l with
  40     | Nil -> true
  41     | Cons x r -> not (mem x r) /\ no_repet r
  42     end
  43
  44   let rec ghost mem_decomp (x: loc) (l: list loc)
  45     : (l1: list loc, l2: list loc)
  46     requires { mem x l }
  47     variant  { l }
  48     ensures  { l = l1 ++ Cons x l2 }
  49   = match l with
  50     | Nil -> absurd
  51     | Cons h t -> if eq_loc h x then (Nil,t) else
  52        let (r1,r2) = mem_decomp x t in (Cons h r1,r2)
  53     end
  54
  55   val acc (field: ref (map loc 'a)) (l:loc) : 'a
  56     requires { l <> null }
  57     reads { field }
  58     ensures { result = get !field l }
  59
  60   val upd (field: ref (map loc 'a)) (l:loc) (v:'a):unit
  61     requires { l <> null }
  62     writes { field }
  63     ensures { !field = set (old !field) l v }
  64
  65
  66   inductive list_seg loc (map loc loc) (list loc) loc =
  67   | list_seg_nil: forall p:loc, next:map loc loc. list_seg p next Nil p
  68   | list_seg_cons: forall p q:loc, next:map loc loc, l:list loc.
  69       p <> null /\ list_seg (get next p) next l q ->
  70          list_seg p next (Cons p l) q
  71
  72   let rec lemma list_seg_frame_ext (next1 next2:map loc loc)
  73     (p q r v: loc) (pM:list loc)
  74     requires { list_seg p next1 pM r }
  75     requires { next2 = set next1 q v }
  76     requires { not (mem q pM) }
  77     variant  { pM }
  78     ensures  { list_seg p next2 pM r }
  79   = match pM with
  80     | Nil -> ()
  81     | Cons h t ->
  82        assert { p = h };
  83        list_seg_frame_ext next1 next2 (get next1 p) q r v t
  84     end
  85
  86   let rec lemma list_seg_functional (next:map loc loc) (l1 l2:list loc) (p: loc)
  87     requires { list_seg p next l1 null }
  88     requires { list_seg p next l2 null }
  89     variant  { l1 }
  90     ensures  { l1 = l2 }
  91   = match l1,l2 with
  92     | Nil, Nil -> ()
  93     | Cons _ r1, Cons _ r2 -> list_seg_functional next r1 r2 (get next p)
  94     | _ -> absurd
  95     end
  96
  97   let rec lemma list_seg_sublistl (next:map loc loc) (l1 l2:list loc) (p q: loc)
  98     requires { list_seg p next (l1 ++ Cons q l2) null }
  99     variant { l1 }
 100     ensures { list_seg q next (Cons q l2) null }
 101   = match l1 with
 102     | Nil -> ()
 103     | Cons _ r -> list_seg_sublistl next r l2 (get next p) q
 104     end
 105
 106   let rec lemma list_seg_no_repet (next:map loc loc) (p: loc) (pM:list loc)
 107     requires { list_seg p next pM null }
 108     variant  { pM }
 109     ensures  { no_repet pM }
 110   = match pM with
 111     | Nil -> ()
 112     | Cons h t ->
 113       if mem h t then
 114          (* absurd case *)
 115          let (l1,l2) = mem_decomp h t in
 116          list_seg_sublistl next (Cons h l1) l2 p h;
 117          list_seg_functional next pM (Cons h l2) p;
 118          assert { length pM > length (Cons h l2) }
 119       else
 120         list_seg_no_repet next (get next p) t
 121     end
 122
 123   let rec lemma list_seg_append (next:map loc loc) (p q r: loc) (pM qM:list loc)
 124     requires { list_seg p next pM q }
 125     requires { list_seg q next qM r }
 126     variant  { pM }
 127     ensures  { list_seg p next (pM ++ qM) r }
 128   = match pM with
 129     | Nil -> ()
 130     | Cons _ t ->
 131       list_seg_append next (get next p) q r t qM
 132     end
 133
 134   val next : ref (map loc loc)
 135
 136   let app (l1 l2:loc) (ghost l1M l2M:list loc) : loc
 137     requires { list_seg l1 !next l1M null }
 138     requires { list_seg l2 !next l2M null }
 139     requires { disjoint l1M l2M }
 140     ensures { list_seg result !next (l1M ++ l2M) null }
 141   =
 142     if eq_loc l1 null then l2 else
 143     let p = ref l1 in
 144     let ghost pM = ref l1M in
 145     let ghost l1pM = ref (Nil : list loc) in
 146     while not (eq_loc (acc next !p) null) do
 147       invariant { !p <> null }
 148       invariant { list_seg l1 !next !l1pM !p }
 149       invariant { list_seg !p !next !pM null }
 150       invariant { !l1pM ++ !pM = l1M }
 151       invariant { disjoint !l1pM !pM }
 152       variant   { !pM }
 153         match !pM with
 154         | Nil -> absurd
 155         | Cons h t ->
 156           pM := t;
 157           assert { disjoint !l1pM !pM };
 158           assert { not (mem h !pM) };
 159           l1pM := !l1pM ++ Cons h Nil;
 160         end;
 161         p := acc next !p
 162     done;
 163     upd next !p l2;
 164     assert { list_seg l1 !next !l1pM !p };
 165     assert { list_seg !p !next (Cons !p Nil) l2 };
 166     assert { list_seg l2 !next l2M null };
 167     l1
 168
 169
 170
 171   let in_place_reverse (l:loc) (ghost lM:list loc) : loc
 172     requires { list_seg l !next lM null }
 173     ensures  { list_seg result !next (reverse lM) null }
 174   = let p = ref l in
 175     let ghost pM = ref lM in
 176     let r = ref null in
 177     let ghost rM = ref (Nil : list loc) in
 178     while not (eq_loc !p null) do
 179       invariant { list_seg !p !next !pM null }
 180       invariant { list_seg !r !next !rM null }
 181       invariant { disjoint !pM !rM }
 182       invariant { (reverse !pM) ++ !rM = reverse lM }
 183       variant   { !pM }
 184       let n = get !next !p in
 185       upd next !p !r;
 186       assert { list_seg !r !next !rM null };
 187       r := !p;
 188       p := n;
 189       match !pM with
 190       | Nil -> absurd
 191       | Cons h t -> rM := Cons h !rM; pM := t
 192       end
 193       done;
 194     !r
 195
 196 end
 197
 198 (** Using sequences instead of lists *)
 199
 200 module InPlaceRevSeq
 201
 202   use int.Int
 203   use map.Map as Map
 204   use seq.Seq
 205   use seq.Mem
 206   use seq.Reverse
 207
 208   type loc
 209
 210   val function null: loc
 211
 212   val function eq_loc (l1 l2:loc) : bool
 213     ensures { result <-> l1 = l2 }
 214
 215   predicate disjoint (s1: seq 'a) (s2: seq 'a) =
 216     (* forall x:'a. not (mem x s1 /\ mem x s2) *)
 217     forall i1. 0 <= i1 < length s1 ->
 218     forall i2. 0 <= i2 < length s2 ->
 219     s1[i1] <> s2[i2]
 220
 221   predicate no_repet (s: seq loc) =
 222     forall i. 0 <= i < length s -> not (mem s[i] s[i+1..])
 223
 224   lemma non_empty_seq:
 225     forall s: seq 'a. length s > 0 ->
 226     s == cons s[0] s[1..]
 227
 228   let rec ghost mem_decomp (x: loc) (s: seq loc) : (s1: seq loc, s2: seq loc)
 229     requires { mem x s }
 230     variant  { length s }
 231     ensures  { s == s1 ++ cons x s2 }
 232   =
 233     if eq_loc s[0] x then (empty, s[1..])
 234     else begin
 235       assert { s == cons s[0] s[1..] };
 236       let (s1, s2) = mem_decomp x s[1..] in (cons s[0] s1, s2)
 237     end
 238
 239   use ref.Ref
 240
 241   type memory 'a = ref (Map.map loc 'a)
 242
 243   val acc (field: memory 'a) (l:loc) : 'a
 244     requires { l <> null }
 245     reads    { field }
 246     ensures  { result = Map.get !field l }
 247
 248   val upd (field: memory 'a) (l: loc) (v: 'a) : unit
 249     requires { l <> null }
 250     writes   { field }
 251     ensures  { !field = Map.set (old !field) l v }
 252
 253   type next = Map.map loc loc
 254
 255   predicate list_seg (next: next) (p: loc) (s: seq loc) (q: loc) =
 256     let n = length s in
 257     (forall i. 0 <= i < n -> s[i] <> null) /\
 258     (   (p = q /\ n = 0)
 259      \/ (1 <= n /\ s[0] = p /\ Map.get next s[n-1] = q /\
 260          forall i. 0 <= i < n-1 -> Map.get next s[i] = s[i+1]))
 261
 262   lemma list_seg_frame_ext:
 263     forall next1 next2: next, p q r v: loc, pM: seq loc.
 264     list_seg next1 p pM r ->
 265     next2 = Map.set next1 q v ->
 266     not (mem q pM) ->
 267     list_seg next2 p pM r
 268
 269   let rec lemma list_seg_functional (next: next) (l1 l2: seq loc) (p: loc)
 270     requires { list_seg next p l1 null }
 271     requires { list_seg next p l2 null }
 272     variant  { length l1 }
 273     ensures  { l1 == l2 }
 274   = if length l1 > 0 && length l2 > 0 then begin
 275       assert { l1[0] = l2[0] = p };
 276       list_seg_functional next l1[1..] l2[1..] (Map.get next p)
 277     end
 278
 279   let rec lemma list_seg_tail (next: next) (l1: seq loc) (p q: loc)
 280     requires { list_seg next p l1 q }
 281     requires { length l1 > 0 }
 282     variant  { length l1 }
 283     ensures  { list_seg next (Map.get next p) l1[1..] q }
 284   = if length l1 > 1 then
 285       list_seg_tail next l1[1..] (Map.get next p) q
 286
 287   let rec lemma list_seg_append (next: next) (p q r: loc) (pM qM: seq loc)
 288     requires { list_seg next p pM q }
 289     requires { list_seg next q qM r }
 290     variant  { length pM }
 291     ensures  { list_seg next p (pM ++ qM) r }
 292   =  if length pM > 0 then
 293       list_seg_append next (Map.get next p) q r pM[1..] qM
 294
 295   lemma seq_tail_append:
 296     forall l1 l2: seq 'a.
 297     length l1 > 0 -> (l1 ++ l2)[1..] == l1[1..] ++ l2
 298
 299   let rec lemma list_seg_prefix (next: next) (l1 l2: seq loc) (p q: loc)
 300     requires { list_seg next p (l1 ++ cons q l2) null }
 301     variant  { length l1 }
 302     ensures  { list_seg next p l1 q }
 303   = if length l1 > 0 then begin
 304       list_seg_tail next (l1 ++ cons q l2) p null;
 305       list_seg_prefix next l1[1..] l2 (Map.get next p) q
 306     end
 307
 308   let rec lemma list_seg_sublistl (next: next) (l1 l2: seq loc) (p q: loc)
 309     requires { list_seg next p (l1 ++ cons q l2) null }
 310     variant  { length l1 }
 311     ensures  { list_seg next q (cons q l2) null }
 312   = assert { list_seg next p l1 q };
 313     if length l1 > 0 then begin
 314       list_seg_tail next l1 p q;
 315       list_seg_sublistl next l1[1..] l2 (Map.get next p) q
 316     end
 317
 318   lemma get_tail:
 319     forall i: int, s: seq 'a. 0 <= i < length s - 1 -> s[1..][i] = s[i+1]
 320   lemma tail_suffix:
 321     forall i: int, s: seq 'a. 0 <= i < length s -> s[1..][i..] == s[i+1..]
 322
 323   let rec lemma list_seg_no_repet (next: next) (p: loc) (pM: seq loc)
 324     requires { list_seg next p pM null }
 325     variant  { length pM }
 326     ensures  { no_repet pM }
 327   = if length pM > 0 then begin
 328       let h = pM[0] in
 329       let t = pM[1..] in
 330       if mem h t then
 331          (* absurd case *)
 332          let (l1,l2) = mem_decomp h t in
 333          list_seg_sublistl next (cons h l1) l2 p h;
 334          list_seg_functional next pM (cons h l2) p;
 335          assert { length pM > length (cons h l2) }
 336       else begin
 337         assert { not (mem pM[0] pM[0+1..]) };
 338         list_seg_no_repet next (Map.get next p) t;
 339         assert { forall i. 1 <= i < length pM -> not (mem pM[i] pM[i+1..]) }
 340       end
 341     end
 342
 343   val next : ref next
 344
 345   let app (l1 l2: loc) (ghost l1M l2M: seq loc) : loc
 346     requires { list_seg !next l1 l1M null }
 347     requires { list_seg !next l2 l2M null }
 348     requires { disjoint l1M l2M }
 349     ensures  { list_seg !next result (l1M ++ l2M) null }
 350   =
 351     if eq_loc l1 null then l2 else
 352     let p = ref l1 in
 353     let ghost pM = ref l1M in
 354     let ghost l1pM = ref (empty : seq loc) in
 355     ghost list_seg_no_repet !next l1 l1M;
 356     while not (eq_loc (acc next !p) null) do
 357       invariant { !p <> null }
 358       invariant { list_seg !next l1 !l1pM !p }
 359       invariant { list_seg !next !p !pM null }
 360       invariant { !l1pM ++ !pM == l1M }
 361       invariant { disjoint !l1pM !pM }
 362       variant   { length !pM }
 363       assert { length !pM > 0 };
 364       assert { not (mem !p !l1pM) };
 365       let ghost t = !pM[1..] in
 366       ghost l1pM := !l1pM ++ cons !p empty;
 367       ghost pM := t;
 368       p := acc next !p
 369     done;
 370     upd next !p l2;
 371     assert { list_seg !next l1 !l1pM !p };
 372     assert { list_seg !next !p (cons !p empty) l2 };
 373     assert { list_seg !next l2 l2M null };
 374     l1
 375
 376   let in_place_reverse (l:loc) (ghost lM: seq loc) : loc
 377     requires { list_seg !next l lM null }
 378     ensures  { list_seg !next result (reverse lM) null }
 379   = let p = ref l in
 380     let ghost pM = ref lM in
 381     let r = ref null in
 382     let ghost rM = ref (empty: seq loc) in
 383     while not (eq_loc !p null) do
 384       invariant { list_seg !next !p !pM null }
 385       invariant { list_seg !next !r !rM null }
 386       invariant { disjoint !pM !rM }
 387       invariant { (reverse !pM) ++ !rM == reverse lM }
 388       variant   { length !pM }
 389       let n = acc next !p in
 390       upd next !p !r;
 391       assert { list_seg !next !r !rM null };
 392       r := !p;
 393       p := n;
 394       rM := cons !pM[0] !rM;
 395       pM := !pM[1..]
 396     done;
 397     !r
 398
 399 end
 400
 401 (** This time with a fully automated proof.
 402
 403     The key to a fully automated proof is to introduce an array of
 404     cells, called `cell` below, and then to resort to arithmetic and
 405     universal quantifiers to define lists (predicates `listLR` and
 406     `listRL` below).
 407
 408     This proof requires no lemma function and no transformation.
 409     A single call to Z3 completes the proof in no time (0.04 s).
 410 *)
 411
 412 module YetAnotherInPlaceRev
 413
 414   use int.Int
 415   use map.Map
 416
 417   type loc
 418
 419   val (=) (l1 l2: loc) : bool ensures { result <-> l1 = l2 }
 420
 421   val constant null : loc
 422
 423   type mem = { mutable next: loc -> loc }
 424
 425   val mem: mem
 426
 427   let cdr (p: loc) : loc
 428     requires { p <> null }
 429     ensures  { result = mem.next p }
 430   = mem.next p
 431
 432   let set_cdr (p: loc) (v: loc) : unit
 433     requires { p <> null }
 434     ensures  { mem.next = (old mem.next)[p <- v] }
 435   = let m = mem.next in
 436     mem.next <- fun x -> if x = p then v else m x
 437
 438   predicate valid_cells (s: int -> loc) (n: int) =
 439     (forall i. 0 <= i < n -> s i <> null) &&
 440     (forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j)
 441
 442   predicate listLR (m: mem) (s: int -> loc) (l: loc) (lo hi: int) =
 443     0 <= lo <= hi &&
 444     if lo = hi then l = null else
 445       l = s lo && m.next (s (hi-1)) = null &&
 446       forall k. lo <= k < hi-1 -> m.next (s k) = s (k+1)
 447
 448   predicate listRL (m: mem) (s: int -> loc) (l: loc) (lo hi: int) =
 449     0 <= lo <= hi &&
 450     if lo = hi then l = null else
 451       m.next (s lo) = null && l = s (hi-1) &&
 452       forall k. lo < k < hi -> m.next (s k) = s (k-1)
 453
 454   predicate frame (m1 m2: mem) (s: int -> loc) (n: int) =
 455     forall p. (forall i. 0 <= i < n -> p <> s i) ->
 456       m1.next p = m2.next p
 457
 458   let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc)
 459     requires { valid_cells s n }
 460     requires { listLR mem s l 0 n }
 461     ensures  { listRL mem s r 0 n }
 462     ensures  { frame mem (old mem) s n }
 463   = let ref l = l in
 464     let ref p = null in
 465     let ghost ref i = 0 in
 466     while l <> null do
 467       invariant { if n = 0 then l = p = null else
 468                   i = 0     && p = null    && l = s 0
 469                || i = n     && p = s (n-1) && l = null
 470                || 0 < i < n && p = s (i-1) && l = s i }
 471       invariant { listRL mem s p 0 i }
 472       invariant { listLR mem s l i n }
 473       invariant { frame mem (old mem) s n }
 474       variant   { n - i }
 475       let tmp = l in
 476       l <- cdr l;
 477       set_cdr tmp p;
 478       p <- tmp;
 479       i <- i + 1
 480     done;
 481     return p
 482
 483   let rec ghost predicate is_list (m: mem) (l: loc) (s: int -> loc) (n: int)
 484     requires { n >= 0 }
 485     variant  { n }
 486   = if n = 0 then l = null else
 487       l = s 0 <> null && is_list m (m.next l) (fun i -> s (i+1)) (n - 1)
 488
 489   let rec lemma cells_of_list (l: loc) (s: int -> loc) (n: int)
 490     requires { n >= 0 }
 491     requires { is_list mem l s n }
 492     variant  { n }
 493     ensures  { valid_cells s n }
 494     ensures  { listLR mem s l 0 n }
 495   = if n <> 0 then cells_of_list (cdr l) (fun i -> s (i+1)) (n - 1)
 496
 497   let rec lemma list_of_cells (r: loc) (s: int -> loc) (n: int)
 498     requires { n >= 0 }
 499     requires { valid_cells s n }
 500     requires { listRL mem s r 0 n }
 501     variant  { n }
 502     ensures  { is_list mem r (fun i -> s (n-1-i)) n }
 503   = if n <> 0 then list_of_cells (cdr r) s (n - 1)
 504
 505   let list_reversal_final (ghost s) (ghost n: int) (l: loc) : (r: loc)
 506     requires { n >= 0 }
 507     requires { is_list mem l s n }
 508     ensures  { is_list mem r (fun i -> s (n-1-i)) n }
 509     ensures  { frame mem (old mem) s n }
 510   = cells_of_list l s n;
 511     let r = list_reversal s n l in
 512     list_of_cells r s n;
 513     r
 514
 515 end
 516
 517 (** On a null-terminated list, `list_reversal` terminates. We have shown it
 518     already e.g. in the previous module.
 519
 520     But `list_reversal` actually terminates on *any* list, even when it
 521     contains a loop. Indeed, the code will reach the loop while reversing
 522     the initial segment, will reverse the loop, and then will restore the
 523     initial segment. So we end up with a list where only the loop has been
 524     reversed.
 525
 526       before          +---o<--o<--+
 527                       v           |
 528           o-->o-->o-->o-->o-->o-->o
 529
 530       after           +-->o-->o---+
 531                       |           V
 532           o-->o-->o-->o<--o<--o<--o
 533
 534     In the module below, we show that `list_reversal` always terminates.
 535     This requires ruling out inifitely-long lists i.e. assuming a finite
 536     amount of memory.
 537 *)
 538 module Termination
 539
 540   use int.Int
 541   use int.NumOf
 542   use map.Map
 543
 544   type loc
 545
 546   val (=) (l1 l2: loc) : bool ensures { result <-> l1 = l2 }
 547
 548   val constant null : loc
 549
 550   type mem = { mutable next: loc -> loc }
 551
 552   val mem: mem
 553
 554   let cdr (p: loc) : loc
 555     requires { p <> null }
 556     ensures  { result = mem.next p }
 557   = mem.next p
 558
 559   let set_cdr (p: loc) (v: loc) : unit
 560     requires { p <> null }
 561     ensures  { mem.next = (old mem.next)[p <- v] }
 562   = let m = mem.next in
 563     mem.next <- fun x -> if x = p then v else m x
 564
 565   (* Finite memory hypothesis: the list is entirely contained in a finite
 566      set `s` of `n` cells *)
 567
 568   predicate valid_cells (s: int -> loc) (n: int) =
 569     (forall i. 0 <= i < n -> s i <> null) &&
 570     (forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j)
 571
 572   predicate inside_memory (s: int -> loc) (n: int) (l: loc) =
 573     l = null || exists i. 0 <= i < n && l = s[i]
 574
 575   predicate finite_memory (m: mem) (s: int -> loc) (n: int) =
 576     forall i. 0 <= i < n -> inside_memory s n (m.next s[i])
 577
 578   (* The variant is lexicographic, as follows:
 579
 580      - as long as we still discover new cells, we mark them with
 581        increasing numbers (with function `idx` below) and the number
 582        of unmarked cells decreases;
 583
 584      - once we reach a marked cell, this means we are back in the initial
 585        segment and then the mark decreases.
 586   *)
 587
 588   function seen (s: int -> loc) (idx: loc -> int) (lo hi: int) : int =
 589     numof (fun i -> idx s[i] > 0) lo hi
 590
 591   let ghost set_idx (s: int -> loc) (n: int) (idx: loc -> int) (l: loc) (k: int)
 592     requires { valid_cells s n }
 593     requires { inside_memory s n l }
 594     requires { l <> null }
 595     requires { idx l = -1 }
 596     requires { k = seen s idx 0 n >= 0 }
 597     ensures  { seen s idx[l <- k+1] 0 n = 1 + seen s idx 0 n }
 598   = assert { seen s idx[l <- k+1] 0 n = 1 + seen s idx 0 n by
 599              exists il. 0 <= il < n && l = s[il] so
 600                seen s idx 0 n = seen s idx 0 il + seen s idx (il+1) n &&
 601                seen s idx[l <- k+1] 0 n =
 602                  seen s idx[l <- k+1] 0 il + 1 + seen s idx[l <- k+1] (il+1) n }
 603
 604   let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc)
 605     requires { n >= 0 }
 606     requires { valid_cells s n }
 607     requires { finite_memory mem s n }
 608     requires { inside_memory s n l }
 609   = let ref l = l in
 610     let ref r = null in
 611     (* marking function: -1 for unmarked / 0 for null / >0 for marked *)
 612     let ghost ref idx = fun p -> if p = null then 0 else -1 in
 613     let ghost ref k = 0 in (* last mark *)
 614     while l <> null do
 615       invariant { inside_memory s n l }
 616       invariant { inside_memory s n r }
 617       invariant { finite_memory mem s n }
 618       invariant { k = seen s idx 0 n >= 0 }
 619       invariant { forall i. 0 <= i < n -> -1 <= idx s[i] <= k }
 620       invariant { forall p. idx p = 0 <-> p = null }
 621       invariant { if idx l = -1 then
 622                     idx r = k && forall i. 0 <= i < n ->
 623                     0 < idx s[i] -> idx (mem.next s[i]) = idx s[i] - 1
 624                   else forall i. 0 <= i < n ->
 625                     0 < idx s[i] <= idx l -> idx (mem.next s[i]) = idx s[i] - 1 }
 626       variant { n - k, 1 + idx l }
 627       if idx l = -1 then (set_idx s n idx l k; k <- k + 1; idx <- idx[l <- k]);
 628       let tmp = l in
 629       l <- cdr l;
 630       set_cdr tmp r;
 631       r <- tmp;
 632     done;
 633     return r
 634
 635 end