examples_in_progress/next_digit_sum.mlw

   1 module M
   2
   3 (*
   4    ACM Portugese National Programming Contest (MIUP) 2010
   5
   6    Given an integer X >= 0, with N digits, and another integer Y > 0,
   7    find the smallest Z > X such that digit_sum(Z) = Y.
   8
   9    Ocaml code given at the end of file.
  10 *)
  11
  12   use int.Int
  13   use ref.Ref
  14   use array.Array
  15   use int.MinMax
  16   use int.EuclideanDivision
  17   use int.Power
  18
  19   function sum_digits int : int
  20
  21   axiom Sum_digits_def : forall n : int. sum_digits n =
  22     if n <= 0 then 0 else sum_digits (div n 10) + mod n 10
  23
  24   (* interp x i j is the integer X[j-1]...X[i] *)
  25
  26   function interp (int -> int) int int : int
  27
  28   axiom Interp_1 :
  29     forall x : int -> int, i j : int.
  30     i >= j -> interp x i j = 0
  31
  32   axiom Interp_2 :
  33     forall x : int -> int, i j : int.
  34     i < j -> interp x i j = x i + 10 * interp x (i+1) j
  35
  36   (* to allow provers to prove that an assignment does not change the
  37      interpretation on the left (or on the right); requires induction *)
  38   let rec lemma interp_eq
  39     (x1 x2 : int -> int) (i j : int)
  40     requires { forall k : int. i <= k < j -> x1 k = x2 k }
  41     ensures  { interp x1 i j = interp x2 i j }
  42     variant  { j - i }
  43   = if i < j then interp_eq x1 x2 (i+1) j
  44
  45   (* the sum of the elements of x[i..j[ *)
  46   use int.Sum
  47
  48   function sum (m: int -> int) (i j: int) : int =
  49     Sum.sum m i (j - 1)
  50
  51   lemma Sum_is_sum_digits_interp:
  52     forall x : int -> int, i j : int.
  53     sum x i j = sum_digits (interp x i j)
  54
  55   lemma Sum_digits_a_set_eq:
  56     forall x : array int, i j k v : int.
  57     (k < i \/ k >= j) -> sum (Map.set x.elts k v) i j = sum x.elts i j
  58
  59   (* interp9 X i j is the j-digit integer obtained by replacing the i least
  60      significant digits in X by 9, i.e. X[j-1]...X[i]9...9 *)
  61
  62   function interp9 (x : int -> int) (i j : int) : int =
  63     power 10 i * (interp x i j + 1) - 1
  64
  65   lemma Interp9_step:
  66     forall x : int -> int, i j : int.
  67     i < j -> interp9 (Map.set x i 9) i j = interp9 x (i+1) j
  68
  69   val x : array int
  70
  71   (* the number of digits of X *)
  72   val constant n : int
  73     ensures { 0 <= result }
  74
  75   (* the target digit sum *)
  76   val constant y : int
  77     ensures { 0 < result }
  78
  79   let constant m : int = 1 + max n (div y 9)
  80
  81 exception Success
  82
  83 (* 1. Safety: we only prove that array access are within bounds
  84    (and termination, implicitely proved since we only have for loops) *)
  85
  86 let search_safety ()
  87   requires { length x = m }
  88   ensures  { true }
  89   raises   { Success -> true }
  90 = let s = ref 0 in
  91   for i = 0 to m - 1 do (* could be n instead of m *)
  92     s := !s + x[i]
  93   done;
  94   for d = 0 to m - 1 do
  95     invariant { length x = m }
  96     for c = x[d] + 1 to 9 do
  97       invariant { length x = m }
  98       let delta = y - !s - c + x[d] in
  99       if 0 <= delta && delta <= 9 * d then begin
 100         x[d] <- c;
 101         let k = div delta 9 in
 102         for i = 0 to d - 1 do
 103           invariant { length x = m }
 104           if i < k then x[i] <- 9
 105           else if i = k then x[i] <- mod delta 9
 106           else x[i] <- 0
 107         done;
 108         raise Success
 109       end
 110     done;
 111     s := !s - x[d]
 112   done
 113
 114 (* 2. Correctness, part 1: when Success is raised, x contains an integer
 115       with digit sum y *)
 116
 117   (* x[0..m-1] is a well-formed integer i.e. has digits in 0..9 *)
 118   predicate is_integer (x : int -> int) =
 119     forall k : int. 0 <= k < m -> 0 <= x k <= 9
 120
 121 let search ()
 122   requires { length x = m /\ is_integer x.elts }
 123   ensures  { true }
 124   raises   { Success -> is_integer x.elts /\ sum x.elts 0 m = y }
 125 = let s = ref 0 in
 126   for i = 0 to m - 1 do (* could be n instead of m *)
 127     invariant { !s = sum x.elts 0 i }
 128     s := !s + x[i]
 129   done;
 130   assert { !s = sum x.elts 0 m };
 131   for d = 0 to m - 1 do
 132     invariant {
 133       x = old x /\
 134       !s = sum x.elts d m
 135     }
 136     for c = x[d] + 1 to 9 do
 137       invariant { x = old x }
 138       let delta = y - !s - c + x[d] in
 139       if 0 <= delta && delta <= 9 * d then begin
 140         x[d] <- c;
 141         assert { sum x.elts d m = y - delta };
 142         let k = div delta 9 in
 143         assert { k <= d };
 144         for i = 0 to d - 1 do
 145           invariant { length x = m /\ is_integer x.elts /\
 146                       sum x.elts d m = y - delta /\
 147                       sum x.elts 0 i = if i <= k then 9*i else delta }
 148           if i < k then x[i] <- 9
 149           else if i = k then x[i] <- (mod delta 9)
 150           else x[i] <- 0
 151         done;
 152         (* assume { sum !x 0 d = delta }; *)
 153         assert { sum x.elts 0 d = delta };
 154         raise Success
 155       end
 156     done;
 157     s := !s - x[d]
 158   done
 159
 160 (* 3. Correctness, part 2: we now prove that, on success, x contains the
 161    smallest integer > old(x) with digit sum y
 162
 163    4. Completeness: we always raise the Success exception *)
 164
 165   (* x1 > x2 since x1[d] > x2[d] and x1[d+1..m-1] = x2[d+1..m-1] *)
 166   predicate gt_digit (x1 x2 : int -> int) (d : int) =
 167     is_integer x1 /\ is_integer x2 /\ 0 <= d < m /\
 168     x1 d > x2 d /\ forall k : int. d < k < m -> x1 k = x2 k
 169
 170   lemma Gt_digit_interp:
 171     forall x1 x2 : int -> int, d : int.
 172     gt_digit x1 x2 d -> interp x1 0 m > interp x2 0 m
 173
 174   lemma Gt_digit_update:
 175     forall x1 x2 : int -> int, d i v : int.
 176     gt_digit x1 x2 d -> 0 <= i < d -> 0 <= v <= 9 ->
 177     gt_digit (Map.set x1 i v) x2 d
 178
 179   (* the number of digits of a given integer *)
 180   function nb_digits int : int
 181
 182   axiom Nb_digits_0 :
 183     nb_digits 0 = 0
 184
 185   axiom Nb_digits_def :
 186     forall y : int. y > 0 -> nb_digits y = 1 + nb_digits (div y 10)
 187
 188   (* the smallest integer with digit sum y is (y mod 9)9..9
 189      with exactly floor(y/9) trailing 9s *)
 190
 191   function smallest int : int -> int
 192
 193   function smallest_size int : int
 194
 195   axiom Smallest_size_def0:
 196     smallest_size 0 = 0
 197
 198   axiom Smallest_size_def1:
 199     forall y : int. y > 0 ->
 200     smallest_size y = if mod y 9 = 0 then div y 9 else 1 + div y 9
 201
 202   (* smallest(y) is an integer *)
 203   axiom Smallest_def1:
 204     forall y : int. y >= 0 ->
 205     forall k : int. 0 <= k < smallest_size y -> 0 <= smallest y k <= 9
 206
 207   (* smallest(y) has digit sum y *)
 208   axiom Smallest_def2:
 209     forall y : int. y >= 0 ->
 210     sum (smallest y) 0 (smallest_size y) = y
 211
 212   (* smallest(y) is the smallest integer with digit sum y *)
 213   axiom Smallest_def3:
 214     forall y : int. y >= 0 ->
 215     forall u : int. 0 <= u < interp (smallest y) 0 (smallest_size y) ->
 216     sum_digits u <> y
 217
 218   lemma Smallest_shape_1:
 219     forall y : int. y >= 0 -> mod y 9 = 0 ->
 220     forall k : int. 0 <= k < smallest_size y -> smallest y k = 9
 221
 222   lemma Smallest_shape_2:
 223     forall y : int. y >= 0 -> mod y 9 <> 0 ->
 224     (forall k : int. 0 <= k < smallest_size y - 1 -> smallest y k = 9) /\
 225     smallest y (smallest_size y - 1) = mod y 9
 226
 227   lemma Smallest_nb_digits:
 228     forall y : int. y >= 0 ->
 229     nb_digits (interp (smallest y) 0 (smallest_size y)) = smallest_size y
 230
 231   lemma Any_nb_digits_above_smallest_size:
 232     forall y : int. y > 0 ->
 233     forall d : int. d >= smallest_size y ->
 234     exists u : int. nb_digits u = d /\ sum_digits u = y
 235
 236   (* there exists an integer u with m digits and digit sum y *)
 237   lemma Completeness:
 238     m >= smallest_size y /\ (* cut *)
 239     exists u : int. nb_digits u = m /\ sum_digits u = y
 240
 241 let search_smallest ()
 242   requires { length x = m /\ is_integer x.elts /\
 243     (* x has at most n digits *)
 244     forall k : int. n <= k < m -> x[k] = 0 }
 245   ensures  { false }
 246   raises   { Success -> is_integer x.elts /\ sum x.elts 0 m = y /\
 247     interp x.elts 0 m > interp (old x.elts) 0 m /\
 248     forall u : int. interp (old x.elts) 0 m < u < interp x.elts 0 m ->
 249       sum_digits u <> y }
 250 = let s = ref 0 in
 251   for i = 0 to m - 1 do (* could be n instead of m *)
 252     invariant { !s = sum x.elts 0 i }
 253     s := !s + x[i]
 254   done;
 255   assert { !s = sum x.elts 0 m };
 256   for d = 0 to m - 1 do
 257     invariant {
 258       x = old x /\
 259       !s = sum x.elts d m /\
 260       forall u : int.
 261          interp (old x.elts) 0 m < u <= interp9 x.elts d m -> sum_digits u <> y
 262     }
 263     for c = x[d] + 1 to 9 do
 264       invariant {
 265         x = old x /\
 266         forall c' : int. x[d] < c' < c ->
 267           forall u : int.
 268           interp (old x.elts) 0 m < u <= interp9 (Map.set x.elts d c') d m ->
 269             sum_digits u <> y }
 270       let delta = y - !s - c + x[d] in
 271       if 0 <= delta && delta <= 9 * d then begin
 272         assert { smallest_size delta <= d };
 273         x[d] <- c;
 274         assert { sum x.elts d m = y - delta };
 275         assert { gt_digit x.elts (old x.elts) d };
 276         let k = div delta 9 in
 277         assert { k <= d };
 278         for i = 0 to d - 1 do
 279           invariant {
 280              length x = m /\ is_integer x.elts /\
 281              sum x.elts d m = y - delta /\
 282              sum x.elts 0 i = (if i <= k then 9*i else delta) /\
 283              (forall j : int. 0 <= j < i ->
 284                 (j <  smallest_size delta -> x[j] = smallest delta j) /\
 285                 (j >= smallest_size delta -> x[j] = 0)) /\
 286              gt_digit x.elts (old x.elts) d }
 287           if i < k then x[i] <- 9
 288           else if i = k then x[i] <- mod delta 9
 289           else x[i] <- 0;
 290           assert { is_integer x.elts }
 291         done;
 292         assert { sum x.elts 0 d = delta };
 293         assert { interp x.elts 0 d = interp (smallest delta) 0 d };
 294         raise Success
 295       end
 296     done;
 297     s := !s - x[d]
 298   done
 299
 300 end
 301
 302 (*
 303 let ys = Sys.argv.(1)
 304 let zs = Sys.argv.(2)
 305 let n = String.length zs
 306 let y = int_of_string ys
 307
 308 let max_digits = 1 + max n (y / 9)
 309 let x = Array.create max_digits 0
 310 let () =
 311   for i = 0 to n - 1 do x.(n - 1 - i) <- Char.code zs.[i] - Char.code '0' done
 312
 313 let () =
 314   let s = ref 0 in
 315   for i = 0 to max_digits - 1 do s := !s + x.(i) done;
 316   for d = 0 to max_digits - 1 do
 317     (* s is the sum of digits d..n-1 *)
 318     (* solution with digits > d intacts, and digit d increased by 1 or more *)
 319     for c = x.(d) + 1 to 9 do
 320       let delta = y - !s - c + x.(d) in
 321       if 0 <= delta && delta <= 9 * d then begin
 322         x.(d) <- c;
 323         let k = delta / 9 in
 324         for i = 0 to d-1 do
 325           x.(i) <- if i < k then 9 else if i = k then delta mod 9 else 0
 326         done;
 327         for i = max d (n-1) downto 0 do Format.printf "%d" x.(i) done;
 328         Format.printf "@.";
 329         exit 0
 330       end
 331     done;
 332     s := !s - x.(d)
 333   done
 334 *)
 335