linked_list_rev: added in_place_reverse

parent 1b646a1d
......@@ -203,6 +203,7 @@ module InPlaceRevSeq
use import int.Int
use map.Map
use import seq.Seq
use import seq.Reverse
use import ref.Ref
predicate mem (x: 'a) (s: seq 'a) =
......@@ -220,7 +221,8 @@ module InPlaceRevSeq
variant { length s - i }
returns { (s1,s2) -> s == s1 ++ cons x s2 }
=
if s[i] = x then (s[0 .. i], s[i+1 ..]) else mem_decomp x s (i+1)
if s[i] = x then (s[0 .. i], s[i+1 ..])
else begin assert { mem x s[i+1 .. ] }; mem_decomp x s (i+1) end
type loc
......@@ -363,6 +365,30 @@ module InPlaceRevSeq
assert { list_seg !next l2 l2M null };
l1
let in_place_reverse (l:loc) (ghost lM: seq loc) : loc
requires { list_seg !next l lM null }
ensures { list_seg !next result (reverse lM) null }
= 'Init:
let p = ref l in
let ghost pM = ref lM in
let r = ref null in
let ghost rM = ref (empty: seq loc) in
while !p <> null do
invariant { list_seg !next !p !pM null }
invariant { list_seg !next !r !rM null }
invariant { disjoint !pM !rM }
invariant { (reverse !pM) ++ !rM == reverse lM }
variant { length !pM }
let n = acc next !p in
upd next !p !r;
assert { list_seg !next !r !rM null };
r := !p;
p := n;
rM := cons !pM[0] !rM;
pM := !pM[ 1 .. ]
done;
!r
end
(*
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment