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

(* list length *)

let length (p0:pointer) =
  { is_list(Ltl, p0) }
  let p = ref p0 in
  let n = ref 0 in
  begin
  while not (is_null !p) do
    { invariant is_list(Ltl, p)
      variant store_pointer_pair(Ltl, p) for ll_order }
    n := !n + 1;
    p := (pget !Ltl !p)
  done;
  !n
  end
  {}