foveoos11_challenge3.mlw 1.6 KB
Newer Older
1 2 3 4 5 6 7 8 9

(* FoVeOOS 2011 verification competition
   http://foveoos2011.cost-ic0701.org/verification-competition

   Challenge 3
*)

module TwoEqualElements

10
  use import int.Int
11 12
  use import ref.Refint
  use import array.Array
13 14 15 16 17

  predicate appear_twice (a: array int) (v: int) (u: int) =
    exists i: int. 0 <= i < u /\ a[i] = v /\
    exists j: int. 0 <= j < u /\ j <> i /\ a[j] = v

18 19 20 21
  let two_equal_elements (a: array int) (n: int)
    requires { length a = n+2 /\ n >= 2 }
    requires { forall i: int. 0 <= i < length a -> 0 <= a[i] < n }
    requires {
22 23
      exists v1: int. appear_twice a v1 (n+2) /\
      exists v2: int. appear_twice a v2 (n+2) /\ v2 <> v1 }
24 25 26
    returns { v1, v2 ->
      appear_twice a v1 (n+2) /\ appear_twice a v2 (n+2) /\ v1 <> v2 }
  = let deja_vu = make n False in
27 28 29
    let v1 = ref (-1) in
    let v2 = ref (-1) in
    for i = 0 to n+1 do
30 31 32 33
      invariant { !v1 = -1 -> !v2 = -1 }
      invariant { !v1 <> -1 -> appear_twice a !v1 i }
      invariant { !v2 <> -1 -> appear_twice a !v2 i /\ !v2 <> !v1 }
      invariant { forall v: int. 0 <= v < n ->
34
           if deja_vu[v]=True then exists j: int. 0 <= j < i /\ a[j] = v
35 36 37 38 39
                              else forall j: int. 0 <= j < i -> a[j] <> v }
      invariant { !v1 = -1 ->
        forall v: int. 0 <= v < n -> not (appear_twice a v i) }
      invariant { !v2 = -1 -> forall v: int. 0 <= v < n -> v <> !v1 ->
           not (appear_twice a v i) }
40 41 42 43 44 45 46 47 48 49
      let v = a[i] in
      if deja_vu[v] then begin
        if !v1 = -1 then v1 := v
        else if !v2 = -1 && v <> !v1 then v2 := v
      end else
        deja_vu[v] <- True
    done;
    (!v1, !v2)

end