examples/foveoos11-cm/duplets.mlw

   1 (*
   2 COST Verification Competition. vladimir@cost-ic0701.org
   3
   4 Challenge 3: Two equal elements
   5
   6 Given: An integer array a of length n+2 with n>=2. It is known that at
   7 least two values stored in the array appear twice (i.e., there are at
   8 least two duplets).
   9
  10 Implement and verify a program finding such two values.
  11
  12 You may assume that the array contains values between 0 and n-1.
  13 *)
  14
  15 module Duplets
  16
  17   use int.Int
  18   use option.Option
  19   use ref.Ref
  20   use array.Array
  21
  22   (* duplet in array a is a pair of indexes (i,j) in the bounds of array
  23      a such that a[i] = a[j] *)
  24   predicate is_duplet (a:array int) (i:int) (j:int) =
  25      0 <= i < j < length a /\ a[i] = a[j]
  26
  27   let predicate eq_opt (x:int) (o:option int) =
  28     match o with
  29     | None -> false
  30     | Some v -> v=x
  31     end
  32
  33   exception Break
  34
  35   (* (duplet a) returns the indexes (i,j) of a
  36      duplet in a. *)
  37   let duplet (a:array int) (except:option int)
  38      requires { 2 <= length a /\
  39        exists i j:int. is_duplet a i j /\
  40                        not (eq_opt a[i] except) }
  41      ensures { let (i,j) = result in
  42        is_duplet a i j /\ not (eq_opt a[i] except) }
  43    = let res = ref (0,0) in
  44      try
  45       for i=0 to length a - 2 do
  46         invariant {
  47           forall k l:int. 0 <= k < i /\ k < l < length a ->
  48             not (eq_opt a[k] except) -> not (is_duplet a k l)
  49         }
  50          let v = a[i] in
  51          if eq_opt v except then () else
  52          for j=i+1 to length a - 1 do
  53            invariant {
  54              forall l:int. i < l < j -> not (is_duplet a i l)
  55            }
  56              if a[j] = v then
  57                begin
  58                 res := (i,j);
  59                 raise Break
  60                end
  61          done
  62       done;
  63       assert { forall i j:int. not (is_duplet a i j) };
  64       absurd
  65      with Break -> !res
  66      end
  67
  68   let duplets (a: array int)
  69     requires { 4 <= length a /\ exists i j k l:int.
  70       is_duplet a i j /\ is_duplet a k l /\ a[i] <> a[k] }
  71     ensures { let ((i,j),(k,l)) = result in
  72       is_duplet a i j /\ is_duplet a k l /\ a[i] <> a[k] }
  73   = let (i,j) = duplet a None in
  74     let (k,l) = duplet a (Some a[j]) in
  75     ((i,j),(k,l))
  76
  77 end