Commit e6e5f3f0 authored by MARCHE Claude's avatar MARCHE Claude

linked_list_rev: use of ghost variables

parent 6d9c66b4
......@@ -70,14 +70,14 @@ module InPlaceRev
val next : ref (map loc loc)
let in_place_reverse (l:loc) (lM:list loc) : loc
let in_place_reverse (l:loc) (ghost lM:list loc) : loc
requires { list_seg l !next lM null }
ensures { list_seg result !next (reverse lM) null }
= 'Init:
let p = ref l in
let pM = ref lM in
let ghost pM = ref lM in
let r = ref null in
let rM = ref (Nil : list loc) in
let ghost rM = ref (Nil : list loc) in
while !p <> null do
invariant { list_seg !p !next !pM null }
invariant { list_seg !r !next !rM null }
......
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