nicer code for vstte12_two_way_sort

parent 3e60ff81
......@@ -20,16 +20,17 @@ module TwoWaySort
forall i1 i2: int. 0 <= i1 <= i2 < a.length -> le a[i1] a[i2]
let two_way_sort (a: array bool)
ensures { sorted a /\ permut_all (old a) a }
ensures { sorted a }
ensures { permut_all (old a) a }
= 'Init:
let i = ref 0 in
let j = ref (length a - 1) in
while !i < !j do
invariant { 0 <= !i /\ !j < length a /\
(permut_all (at a 'Init) a) /\
(forall k: int. 0 <= k < !i -> a[k] = False) /\
(forall k: int. !j < k < length a -> a[k] = True) }
variant { !j - !i }
invariant { 0 <= !i /\ !j < length a }
invariant { forall k: int. 0 <= k < !i -> a[k] = False }
invariant { forall k: int. !j < k < length a -> a[k] = True }
invariant { permut_all (at a 'Init) a }
variant { !j - !i }
if not a[!i] then incr i
else if a[!j] then decr j
else begin swap a !i !j; incr i; decr j end
......
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