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) }