Commit 4850f8fb authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

remove_duplicate: slightly prettier code

parent 0ebb4d5f
...@@ -25,14 +25,13 @@ module RemoveDuplicateQuadratic ...@@ -25,14 +25,13 @@ module RemoveDuplicateQuadratic
use import Spec use import Spec
use import ref.Refint use import ref.Refint
let rec test_appears (ghost w:ref int) (v: 'a) (a: array 'a) (s: int) : bool let rec test_appears (ghost w: ref int) (v: 'a) (a: array 'a) (s: int) : bool
requires { 0 <= s <= length a } requires { 0 <= s <= length a }
ensures { result=true <-> appears v a s } ensures { result=true <-> appears v a s }
ensures { result=true -> 0 <= !w < s && a[!w] = v } ensures { result=true -> 0 <= !w < s && a[!w] = v }
variant { s } variant { s }
= s > 0 && if a[s-1] = v = s > 0 &&
then begin w := s - 1 ; true end if a[s-1] = v then begin w := s - 1; true end else test_appears w v a (s-1)
else test_appears w v a (s-1)
let remove_duplicate (a: array 'a) : int let remove_duplicate (a: array 'a) : int
ensures { 0 <= result <= length a } ensures { 0 <= result <= length a }
...@@ -41,7 +40,7 @@ module RemoveDuplicateQuadratic ...@@ -41,7 +40,7 @@ module RemoveDuplicateQuadratic
= let n = length a in = let n = length a in
let r = ref 0 in let r = ref 0 in
let ghost from = make n 0 in let ghost from = make n 0 in
let ghost to_ = make n 0 in let ghost to_ = make n 0 in
'L: 'L:
for i = 0 to n - 1 do for i = 0 to n - 1 do
invariant { 0 <= !r <= i } invariant { 0 <= !r <= i }
......
Supports Markdown
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