examples/foveoos11_challenge3.mlw

   1
   2 (* FoVeOOS 2011 verification competition
   3    http://foveoos2011.cost-ic0701.org/verification-competition
   4
   5    Challenge 3
   6 *)
   7
   8 module TwoEqualElements
   9
  10   use int.Int
  11   use ref.Refint
  12   use array.Array
  13
  14   predicate appear_twice (a: array int) (v: int) (u: int) =
  15     exists i: int. 0 <= i < u /\ a[i] = v /\
  16     exists j: int. 0 <= j < u /\ j <> i /\ a[j] = v
  17
  18   let two_equal_elements (a: array int) (n: int) : (v1:int, v2:int)
  19     requires { length a = n+2 /\ n >= 2 }
  20     requires { forall i: int. 0 <= i < length a -> 0 <= a[i] < n }
  21     requires {
  22       exists v1: int. appear_twice a v1 (n+2) /\
  23       exists v2: int. appear_twice a v2 (n+2) /\ v2 <> v1 }
  24     ensures  {
  25       appear_twice a v1 (n+2) /\ appear_twice a v2 (n+2) /\ v1 <> v2 }
  26   = let deja_vu = make n False in
  27     let v1 = ref (-1) in
  28     let v2 = ref (-1) in
  29     for i = 0 to n+1 do
  30       invariant { !v1 = -1 -> !v2 = -1 }
  31       invariant { !v1 <> -1 -> appear_twice a !v1 i }
  32       invariant { !v2 <> -1 -> appear_twice a !v2 i /\ !v2 <> !v1 }
  33       invariant { forall v: int. 0 <= v < n ->
  34            if deja_vu[v]=True then exists j: int. 0 <= j < i /\ a[j] = v
  35                               else forall j: int. 0 <= j < i -> a[j] <> v }
  36       invariant { !v1 = -1 ->
  37         forall v: int. 0 <= v < n -> not (appear_twice a v i) }
  38       invariant { !v2 = -1 -> forall v: int. 0 <= v < n -> v <> !v1 ->
  39            not (appear_twice a v i) }
  40       let v = a[i] in
  41       if deja_vu[v] then begin
  42         if !v1 = -1 then v1 := v
  43         else if !v2 = -1 && v <> !v1 then v2 := v
  44       end else
  45         deja_vu[v] <- True
  46     done;
  47     (!v1, !v2)
  48
  49 end