vstte10_max_sum.mlw 643 Bytes
Newer Older
1
2
(* VSTTE'10 competition 
   Problem 1: max and sum of an array *)
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

{
  use array.ArrayLength as A

  type array 'a = A.t int 'a

  logic (#) (a : array 'a) (i : int) : 'a = A.get a i
}

let max_sum a n =
  { n >= 0 and forall i:int. 0 <= i < n -> a#i >= 0 }
  let sum = ref 0 in
  let max = ref 0 in
  for i = 0 to n-1 do
    invariant { !sum <= i * !max and forall j:int. 0 <= j < i -> a#j <= !max }
    if !max < a#i then max := a#i;
    sum := !sum + a#i
  done;
  (!sum, !max)
  { let (sum, max) = result in sum <= n * max }

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_max_sum.gui"
End: 
*)