next_digit_sum.mlw 2.95 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18

(*
   ACM Portugese National Programming Contest (MIUP) 2010

   Given an integer X >= 0, with N digits, and another integer Y > 0,
   find the smallest Z > X such that digit_sum(Z) = Y.

   Ocaml code given at the end of file.
*)

{
  use array.ArrayLength as A

  type array 'a = A.t int 'a

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

19 20
let array_get (a : ref (array 'a)) i = 
  { 0 <= i < A.length !a } A.get !a i { result = A.get !a i }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21

22 23
let array_set (a : ref (array 'a)) i v = 
  { 0 <= i < A.length !a } a := A.set !a i v { !a = A.set (old !a) i v }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24

25
parameter x : ref (array int)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26 27 28 29 30 31 32 33 34

{ 
  logic n : int
  logic y : int
  
  use import int.MinMax
  use import int.EuclideanDivision

  logic m : int = 1 + max n (div y 9)
35

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
36 37
}

38 39
exception Success

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
40
let search () =
41
  { n >= 0 and y > 0 and A.length !x = m and
42 43 44
    (n = 0 or !x#(n-1) <> 0) and
    (forall i:int. 0 <= i < n -> 0 <= !x#i <= 9) and
    (forall i:int. n <= i < m -> !x#i = 0) }
45
  label Init:
46 47
  let s = ref 0 in
  let i = ref 0 in
48 49 50 51
  while !i < n do 
    invariant { 0 <= !i <= n } variant { n - !i }
    s := !s + array_get x !i; 
    i := !i + 1 
52
  done;
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
  let d = ref 0 in
  while !d < m do
    invariant { 0 <= !d <= m and !x = at !x Init } 
    variant { m - !d }
    let c = ref (array_get x !d) in
    while !c <= 9 do
      invariant { !x # !d <= !c <= 10 and !x = at !x Init } 
      variant { 10 - !c }
      let delta = y - !s - !c + array_get x !d in
      if 0 <= delta && delta <= 9 * !d then begin
        array_set x !d !c;
	let k = div delta 9 in
        assert { k <= !d };
        i := 0;
	while !i < k do 
 	  invariant { 0 <= !i <= k and A.length !x = m } variant { k - !i }
          array_set x !i 9; i := !i + 1
        done;
        array_set x !i (mod delta 9);
        i := !i + 1;
        while !i < !d do 
          invariant { k+1 <= !i and A.length !x = m } variant { !d - !i }
	  array_set x !i 0; i := !i + 1 
	done;
        raise Success
      end;
      c := !c + 1
    done;
    d := !d + 1
  done
  { true(*false*) } | Success -> { true }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124

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



(*
let s = Sys.argv.(1)
let n = String.length s
let y = int_of_string Sys.argv.(2)

let max_digits = 1 + max n (y / 9)
let x = Array.create max_digits 0
let () = 
  for i = 0 to n - 1 do x.(n - 1 - i) <- Char.code s.[i] - Char.code '0' done

let () =
  let s = ref 0 in
  for i = 0 to max_digits - 1 do s := !s + x.(i) done;
  for d = 0 to max_digits - 1 do
    (* s is the sum of digits d..n-1 *)
    (* solution with digits > d intacts, and digit d increased by 1 or more *)
    for c = x.(d) + 1 to 9 do
      let delta = y - !s - c + x.(d) in
      if 0 <= delta && delta <= 9 * d then begin
	x.(d) <- c;
	let k = delta / 9 in
	for i = 0 to d-1 do 
	  x.(i) <- if i < k then 9 else if i = k then delta mod 9 else 0
	done;
	for i = max d (n-1) downto 0 do printf "%d" x.(i) done;
	printf "@.";
	exit 0
      end
    done;
    s := !s - x.(d)
  done
*)