new proof in progress: inverse of a permutation, in place

that proof was started during the preparation of the second VScomp,
but never completed
parent 925ebd38
(*
Inverse of a permutation, in place
Algorithm I
The Art of Computer Programming, volume 1, Sec. 1.3.3, page 176
*)
module InverseInPlace
use import int.Int
use import ref.Ref
use import array.Array
function (~_) (x: int) : int = -x-1
type param = M.map int int
predicate pr (a: param) (n: int) = M.([]) a n >= 0
clone import int.NumOfParam with type param = param, predicate pr = pr
lemma num_of_decrease:
forall m: param, l r i v: int. l <= i < r ->
M.get m i >= 0 -> v < 0 -> num_of (M.set m i v) l r < num_of m l r
predicate is_permutation (a: array int) =
forall i: int. 0 <= i < length a ->
0 <= a[i] < length a /\
forall j: int. 0 <= j < length a -> i <> j -> a[i] <> a[j]
lemma is_permutation_inverse:
forall a b: array int. length a = length b ->
is_permutation a ->
(forall i: int. 0 <= i < length b -> 0 <= b[i] < length b) ->
(forall i: int. 0 <= i < length b -> a[b[i]] = i) ->
is_permutation b
(***
predicate is_permutation_neg (a: array int) =
forall i: int. 0 <= i < length a ->
- (length a) <= a[i] < length a /\
forall j: int. 0 <= j < length a -> i <> j ->
a[i] <> a[j] /\ a[i] <> lnot a[j]
lemma is_permutation_neg_is_permutation:
forall a: array int. is_permutation_neg a ->
(forall i: int. 0 <= i < length a -> 0 <= a[i]) ->
is_permutation a
***)
predicate nodup (a: M.map int int) (m: int) =
forall i j: int. 0 <= i < j < m ->
(M.get a i <> M.get a j /\ M.get a i <> ~ (M.get a j))
\/ (M.get a i = ~ (M.get a j) = m)
\/ (~ (M.get a i) = M.get a j = m)
let inverse_in_place (a: array int)
requires { is_permutation a }
ensures { is_permutation a }
ensures { forall i: int. 0 <= i < length a -> (old a)[a[i]] = i }
=
'L:let n = length a in
for m = n-1 downto 0 do
invariant { forall e: int. 0 <= e < n -> -n <= a[e] < n }
invariant { forall e: int. m < e < n -> "FOO1" 0 <= a[e] }
invariant { forall e: int. m < e < n -> "FOO2" (at a 'L)[a[e]] = e }
invariant { forall e: int. 0 <= e <= m ->
a[e] < 0 -> "FOO3" (at a 'L)[~ a[e]] = e }
invariant { forall e: int. 0 <= e <= m ->
a[e] >= 0 -> "FOO4" (at a 'L)[e] = a[e] }
let i = ref a[m] in
if !i >= 0 then begin
(* unrolled loop once *)
a[m] <- -1;
let j = ref (~m) in
let k = ref !i in
i := a[!i];
(* ghost let pre_a = ref a.elts in *)
(* ghost let pre_pre_a = ref a.elts in *)
while !i >= 0 do
invariant { a[!k] = !i <= m /\ 0 <= !k <= m /\ -n <= !j < 0 /\
(at a 'L)[~ !j] = !k }
invariant { forall e: int. 0 <= e < n -> -n <= a[e] < n }
invariant { forall e: int. m < e < n -> 0 <= a[e] }
invariant { forall e: int. m < e < n -> (at a 'L)[a[e]] = e }
invariant { forall e: int. 0 <= e < m ->
a[e] < 0 -> (at a 'L)[~ a[e]] = e }
invariant { forall e: int. 0 <= e < m ->
a[e] >= 0 -> (at a 'L)[e] = a[e] }
(* nodup a.elts m /\ nodup pre_a m /\ nodup pre_pre_a m *)
variant { num_of a.elts 0 n }
a[!k] <- !j;
j := ~ !k;
k := !i;
i := a[!k]
done;
assert { !k = m };
i := !j
end;
assert { (at a 'L)[~ !i] = m };
a[m] <- ~ !i
done
end
module Harness
end
(*
Local Variables:
compile-command: "why3ide inverse_in_place.mlw"
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