external parameter null : pointer
external parameter eq_pointer : 
  p1:pointer -> p2:pointer -> {} bool { if result then p1=p2 else p1<>p2 }
external parameter ne_pointer : 
  p1:pointer -> p2:pointer -> {} bool { if result then p1<>p2 else p1=p2 }
external parameter is_null : p:pointer -> {} bool { if result then p=null else p<>null }

external parameter get_int : int_store -> pointer -> int
external parameter set_int : int_store -> pointer -> int -> int_store

external parameter pget : pointer_store -> pointer -> pointer
external parameter pset : pointer_store -> pointer -> pointer -> pointer_store

external logic is_valid_int : int_store, pointer -> prop
external logic is_valid_pointer : pointer_store, pointer -> prop

external logic llist : pointer_store, pointer, plist -> prop
external logic is_list : pointer_store, pointer -> prop

external logic store_pointer_pair : pointer_store, pointer -> StorePointerPair

(* global state = stores for fields hd and tl *)

parameter Lhd : int_store ref
parameter Ltl : pointer_store ref

(* in-place list reversal *)

external logic rev : plist -> plist
external logic app : plist, plist -> plist
external logic disjoint : plist, plist -> prop

let rev (p0:pointer) =
  { is_list(Ltl, p0) }
  init:
  let p = ref p0 in
  let r = ref !p in
  begin
    p := null;
    while (ne_pointer !r null) do
      { invariant  exists lp:plist. exists lr:plist.
                   llist(Ltl, p, lp) and llist(Ltl, r, lr) and
	           disjoint(lp, lr) and 
	           forall l:plist. 
	           llist(Ltl@init, p0, l) -> app(rev(lr), lp) = rev(l)
        variant store_pointer_pair(Ltl, r) for ll_order }
      let q = ref !r in
      begin
      r := (pget !Ltl !r);
      Ltl := (pset !Ltl !q !p);
      p := !q
      end
    done;
    !p
  end
  { exists l:plist. 
      llist(Ltl, result, l) and
      forall l0:plist. llist(Ltl@, p0, l0) -> l = rev(l0) }