examples_in_progress/maximal_rectangle.mlw

   1 (* Grands rectangles - Concours d'Informatique X-ENS PC 2014 *)
   2
   3
   4 (* Partie I *)
   5 module Search_in_array
   6
   7   use int.Int
   8   use ref.Ref
   9   use array.Array
  10  (* use int.MinMax*)
  11
  12   (* Qeustion 1 *)
  13  let nombreZeroDroite i tab n
  14      requires { 1 <= i <= n < tab.length }
  15      requires { forall k. i <= k <= n -> tab[k] = 1 \/ tab[k] = 0 }
  16      ensures  { i <= result <= n + 1 }
  17      ensures  { forall k. i <= k < result -> tab[k] = 0 }
  18      ensures  { result <= n -> tab[result] = 1  }
  19   =
  20    let j = ref i in
  21     while !j <= n && tab[!j] = 0 do
  22       variant   { n - !j }
  23       invariant { i <= !j <= n + 1}
  24       invariant { forall k. i <= k < !j -> tab[k] = 0 }
  25      j := !j + 1;
  26     done;
  27   !j
  28
  29 (* Question 2 *)
  30 let nombreZeroMaximum tab n =
  31     requires { 1 <= n < tab.length }
  32     requires { forall k. 1 <= k <= n -> tab[k] = 1 \/ tab[k] = 0 }
  33     ensures  { let (p,q) = result in
  34                 (1 <= p <= q <= n + 1) /\
  35                 (forall k. p <= k < q -> tab[k] = 0) }
  36     ensures  { let (p,q) = result in
  37                 forall i j.
  38                  (1 <= i <= j <= n + 1) ->
  39                    (forall k. i <= k < j -> tab[k] = 0) ->
  40                     j - i <= q - p }
  41   let p    = ref 1 in
  42   let q    = ref 1 in
  43   let i    = ref 1  in
  44   while !i <= n do
  45    variant   { n - !i }
  46    invariant { 1 <= !i <= n + 1 }
  47    invariant { 1 <= !p <= !q <= !i }
  48    invariant { forall k. !p <= k < !q -> tab[k]= 0 }
  49    (*invariant { 2 <= !i -> !q <= n -> tab[!q] = 1 }*)
  50    invariant { forall a b.
  51                  (1 <= a <= b <= !i) ->
  52                    (forall k. a <= k < b -> tab[k] = 0) ->
  53                     b - a <= !q - !p }
  54    invariant { 1 < !i <= n -> (tab[!i] = 1 \/ tab[!i-1] = 1) }
  55     let next = nombreZeroDroite !i tab n in
  56     begin
  57       if next - !i > !q  - !p then begin p:= !i; q := next end;
  58       i:= if !i = next then !i + 1 else next;
  59     end
  60   done;
  61   (!p, !q)
  62
  63
  64 (*
  65   (* Question 1 *)
  66   let nombreZeroDroite i tab n
  67      requires { 1 <= i <= n }
  68      requires { n = tab.length - 1 }
  69      requires { forall k. i <= k <= n -> tab[k] = 1 \/ tab[k] = 0 }
  70      ensures  { 0 <= result <= n - i + 1 }
  71      ensures  { forall k. 0 <= k < result -> tab[i + k] = 0 }
  72      ensures  { let j = i + result in j <= n -> tab[j] = 1  }
  73   =
  74    let j = ref i in
  75     while !j <= n && tab[!j] = 0 do
  76       variant   { n - !j }
  77       invariant { 0 <= !j - i <= n - i + 1}
  78       invariant { forall k. 0 <= k < (!j - i) -> tab[i + k] = 0 }
  79      j := !j + 1;
  80     done;
  81   !j - i
  82
  83   let test_0 () =
  84     let tab = make 14 0 in
  85      tab[0]<- (-1);
  86      tab[1] <- 0; tab[2] <- 0;
  87      tab[3] <- 1; tab[4] <- 1;
  88      tab[5] <- 0; tab[6] <- 0; tab[7] <- 0;
  89      tab[8] <- 1;
  90      tab[9] <- 0; tab[10] <- 0; tab[11] <- 0;
  91      tab[12] <- 1; tab[13] <- 1;
  92      let n1 = nombreZeroDroite 4 tab 13  in
  93       assert { n1 = 0 };
  94      let n2 = nombreZeroDroite 6 tab 13  in
  95       assert { n2 = 2 }
  96
  97
  98
  99 (* Question 2 *)
 100 (*TODO*)
 101 let nombreZeroMaximum tab n =
 102     requires { 1 <= n /\ n = tab.length - 1}
 103     requires { forall k. 1 <= k <= n -> tab[k] = 1 \/ tab[k] = 0 }
 104     ensures  { exists i.
 105                 (1 <= i <= n) /\
 106                 (0 <= result <= n - i + 1) /\
 107                 (forall k. 0 <= k < result -> tab[i + k] = 0) /\
 108                 (i + result <= n -> tab[i + result] = 1) }
 109     ensures  { forall j ofs.
 110                 (1 <= j <= n) ->
 111                  (0 <= ofs <= n - j + 1) ->
 112                   (forall k. 0 <= k < ofs -> tab[j + k] = 0) ->
 113                      ofs <= result }
 114   let max = ref (nombreZeroDroite 1 tab n) in
 115   let ghost max_i = ref 1 in
 116   let i   = ref (if !max = 0 then 2 else !max + 1) in
 117   while !i <= n do
 118    variant   { n - !i }
 119    invariant { 1 <= !i <= n + 1}
 120    invariant { 1 <= !max_i < !i }
 121    invariant {0 <= !max < !i - !max_i + 1 }
 122    invariant {forall k. 0 <= k < !max -> tab[!max_i + k]= 0 }
 123    invariant {!max_i + !max <= n -> tab[!max_i + !max] = 1  }
 124    invariant { forall j ofs.
 125                 1 <= j <= !i ->
 126                  (0 <= ofs <= !i - j + 1) ->
 127                   (forall k. 0 <= k < ofs -> tab[j + k] = 0) ->
 128                      ofs <= !max }
 129
 130      let ofs_i = nombreZeroDroite !i tab n in
 131     begin
 132       if ofs_i > !max then begin max := ofs_i; max_i := !i end;
 133       if ofs_i = 0 then i := !i + 1 else i:= !i + ofs_i;
 134     end
 135   done;
 136   !max
 137 *)
 138
 139 end
 140
 141
 142
 143 (* Partie II. De la 1D vers la 2D *)
 144
 145
 146
 147 (* Partie III. Algorithme optimisé *)
 148 (*Questions 7 - 12 *)
 149 (*
 150 let rec calculeL_aux i histo l =
 151   let j = ref i in
 152   while !j > 1 && histo.(!j-1) >= histo.(i) do
 153     j := calculeL_aux (!j-1) histo l
 154   done;
 155   l.(i) <- !j; !j
 156
 157 let calculeL histo =
 158   let l = Array.make (Array.length histo) 0 in
 159   let i = ref (Array.length histo - 1) in
 160   while !i > 0 do
 161     let j = calculeL_aux !i histo l in
 162     if j < !i then i := j else i := !i - 1
 163   done;
 164   l
 165
 166 let rec calculeR_aux i histo r  =
 167   let j = ref i in
 168   while !j < Array.length histo - 1 && histo.(!j+1) >= histo.(i) do
 169     j := calculeR_aux (!j+1) histo r
 170   done;
 171   r.(i) <- !j; !j
 172
 173 let calculeR histo =
 174   let r = Array.make (Array.length histo) 0 in
 175   let i = ref 1 in
 176   while !i < Array.length histo do
 177     let j = calculeR_aux !i histo r in
 178     if j > !i then i := j else i := !i + 1
 179   done; r
 180
 181 let calculeLR histo = (calculeL histo, calculeR histo)
 182
 183 let plusGrandRectangleHistogramme lx histo =
 184   let l, r = calculeLR histo in
 185   let cx = ref 0 in
 186   let ly = ref 0 in
 187   let cy = ref 0 in
 188   let s  = ref 0 in
 189   for i = 1 to Array.length histo - 1 do
 190     let s' = (r.(i) - (l.(i) - 1)) * histo.(i) in
 191     if s' > !s  then
 192       begin
 193         cx := l.(i);
 194         cy := r.(i);
 195         ly := lx - (histo.(i) - 1);
 196         s := s';
 197       end
 198   done;
 199   ((lx, !cx), (!ly, !cy), !s)
 200
 201
 202 let res col =
 203   let lx, cx, ly, cy, s = ref 0, ref 0, ref 0,ref 0, ref 0 in
 204   for i = 1 to Array.length col - 1 do
 205     let (lx', cx'), (ly', cy'), s' = plusGrandRectangleHistogramme i col.(i)  in
 206     if s' > !s then
 207       begin
 208         lx := i;
 209         cx := cx';
 210         ly := ly';
 211         cy := cy';
 212         s := s';
 213       end
 214   done;
 215   (!lx, !cx), (!ly, !cy), !s
 216
 217
 218 let histo = [|-1;3;1;2;4;2;2;0;1|]
 219
 220 let col =
 221   [|
 222     [|-1 |];
 223     [|-1; 1; 1; 0; 0; 1; 1; 1; 0 |];
 224     [|-1; 2; 2; 1; 1; 0; 2; 2; 0 |];
 225     [|-1; 0; 3; 2; 2; 1; 3; 3; 0 |];
 226     [|-1; 1; 0; 3; 3; 2; 4; 4; 0 |];
 227     [|-1; 2; 1; 0; 0; 3; 5; 5; 0 |];
 228     [|-1; 3; 2; 0; 1; 4; 6; 6; 0 |];
 229     [|-1; 4; 0; 0; 0; 5; 0; 7; 0 |];
 230     [|-1; 5; 1; 0; 0; 6; 1; 8; 0;|]
 231   |]
 232
 233 let _ = plusGrandRectangleHistogramme 4 histo
 234 let _ = res col *)
 235
 236
 237 (************************************************)
 238 (*
 239 module Recherche_bidimensionnelle
 240
 241 use int.Int
 242 use ref.Ref
 243 use array.Array
 244
 245
 246 let rec calculeL_aux i histo l
 247   requires {l.length = histo.length}
 248   requires {0 <= i < histo.length }
 249   ensures  {0 <= result <= i}
 250   ensures  {forall k. result <= k <= i -> histo[k] >= histo[i]}
 251   ensures  {result > 0 -> histo[result-1] < histo[i]}
 252   ensures  {result = l[i]}
 253   variant { i }
 254   =
 255    let j = ref i in
 256     while !j > 0 && histo[!j-1] >= histo[i] do
 257      variant {!j}
 258      invariant {forall k. !j <= k <= i -> histo[k] >= histo[i]}
 259      invariant {0 <= !j <= i }
 260      j := calculeL_aux (!j-1) histo l
 261     done;
 262     l[i] <- !j; !j
 263
 264 let calculeL i histo l
 265   requires {l.length = histo.length}
 266   requires {0 <= i < histo.length }
 267   ensures  {forall k. result <= k <= i -> histo[k] >= histo[i]}
 268   ensures  {result > 0 -> histo[result-1] < histo[i]}
 269   ensures  {0 <= result <= i}
 270   ensures  {result = l[i]}
 271  = calculeL_aux i histo l
 272
 273 let rec calculeR_aux i histo r
 274   requires {r.length = histo.length}
 275   requires {0 <= i < histo.length }
 276   ensures  {i <= result < histo.length}
 277   ensures  {forall k. i <= k <= result -> histo[k] >= histo[i]}
 278   ensures  {result < histo.length - 1 -> histo[result+1] < histo[i]}
 279   ensures  {result = r[i]}
 280   variant { histo.length - i }
 281   =
 282    let j = ref i in
 283     while !j < histo.length - 1 && histo[!j+1] >= histo[i] do
 284      variant {histo.length - !j}
 285      invariant {forall k. i <= k <= !j -> histo[k] >= histo[i]}
 286      invariant {i <= !j < histo.length }
 287      j := calculeR_aux (!j+1) histo r
 288     done;
 289     r[i] <- !j; !j
 290
 291 let calculeR i histo r
 292   requires {r.length = histo.length}
 293   requires {0 <= i < histo.length }
 294   ensures  {forall k. i <= k <= result -> histo[k] >= histo[i]}
 295   ensures  {result < histo.length -1 -> histo[result+1] < histo[i]}
 296   ensures  {i <= result < histo.length}
 297   ensures  {result = r[i]}
 298  = calculeR_aux i histo r
 299
 300
 301 let calculeLR i histo l r
 302   requires {r.length = histo.length}
 303   requires {l.length = histo.length}
 304   requires {0 <= i < histo.length }
 305   ensures  {
 306    let (li, ri) = result in forall k. li <= k <= ri -> histo[i] <= histo[k]}
 307   = (calculeL i histo l, calculeR i histo r)
 308
 309
 310 predicate is_li (i j: int) (histo : array int) =
 311   0 <= j <= i < histo.length /\
 312  (forall k. j <= k <= i -> histo[k] >= histo[i]) /\
 313  (j > 0 -> histo[j-1] < histo[i])
 314
 315
 316 let test () =
 317     let histo = make 8 0 in
 318     let l     = make 8 0 in
 319     histo[0] <- 3; histo[1] <- 1; histo[2] <- 2; histo[3] <- 4;
 320     histo[4] <- 2; histo[5] <- 2; histo[6] <- 0; histo[7] <- 1;
 321     let l0 = calculeL 0 histo l in
 322      assert {l0 = 0 /\ is_li 0 0 histo};
 323     let l1 = calculeL 1 histo l in
 324      assert {l1 = 0 /\ is_li 1 0 histo};
 325     let l2 = calculeL 2 histo l in
 326      assert {histo[1] < histo[2]};
 327      assert {not is_li 2 1 histo};
 328      assert {l2 = 2 /\ is_li 2 2 histo};
 329     let l3 = calculeL 3 histo l in
 330      assert {l3 = 3 /\ is_li 3 3  histo};
 331     let l4 = calculeL 4 histo l in
 332      assert {l4 = 2 /\ is_li 4 2 histo};
 333     let l5 = calculeL 5 histo l in
 334      assert {l5 = 2 /\ is_li 5 2 histo};
 335     let l6 = calculeL 6 histo l in
 336      assert {l6 = 0 /\ is_li 6 0 histo};
 337     let l7 = calculeL 7 histo l in
 338      assert {l7 = 7 /\ is_li 7 7 histo};
 339      assert {not is_li 7 6 histo};
 340      assert {not is_li 7 5 histo};
 341      assert {not is_li 7 2 histo};
 342
 343 end *)
 344
 345 (*
 346 let rec calcule i k
 347   requires {0 < k}
 348   requires {l.length > 0}
 349   requires {l.length = histo.length}
 350   requires {0 <= i < histo.length}
 351   ensures  {0 <= result <= i }
 352   variant { k }
 353   =
 354   let li = (aux i i (k-1)) in
 355    l[i] <- li;
 356    li
 357
 358 with aux i j k
 359   requires { l.length > 0 }
 360   requires {0 <        k}
 361   requires { l.length = histo.length }
 362   requires { 0 <= i < histo.length }
 363   requires { 0 <= j < histo.length }
 364   requires { 0 <= j <= i}
 365   ensures  { 0 <= result <= j}
 366   variant {k}
 367  =
 368   if j = 0
 369    then 0
 370    else
 371     if histo[j-1] < histo[i]
 372      then j
 373      else aux i (calcule (j-1) (k-1)) (k-1)
 374 *)
 375
 376     (* ((ri < histo.length -1 -> histo[ri+1] < histo[i])  /\ *)
 377      (* li > 0 -> histo[li-1] < histo[i]) /\
 378         (i <= ri < histo.length) /\
 379          (0 <= li <= i)} *)
 380 (*(* Partie II. De la 1D vers la 2D *)
 381 module recherche_bidimen
 382
 383 use int.Int
 384 use ref.Ref
 385 use array.Array
 386
 387 predicate is_li (i j: int) (histo : array int) =
 388   0 <= j <= i < histo.length /\
 389  (forall k. j <= k <= i -> histo[k] >= histo[i]) /\
 390  (j > 0 -> histo[j-1] < histo[i])
 391
 392 let rec f i j histo l =
 393   requires {l.length = histo.length}
 394   requires {forall k. j <= k <= i -> histo[k] >= histo[i]}
 395   requires {0 <= j <= i < histo.length }
 396   ensures  {is_li i result histo}
 397   ensures  {result = l[i]}
 398   variant {j}
 399   let li =
 400     if j = 0 then 0
 401     else if histo[j-1] < histo[i] then j
 402          else f i (f (j-1) (j-1) histo l) histo l
 403   in l[i] <- li; li
 404
 405 let calculeL i histo l =
 406   requires {0 <= i < histo.length}
 407   requires {l.length = histo.length}
 408   ensures  {is_li i result histo}
 409   ensures  {result = l[i]}
 410  f i i histo l
 411
 412
 413 let test () =
 414     let histo = make 8 0 in
 415     let l     = make 8 0 in
 416     histo[0] <- 3; histo[1] <- 1; histo[2] <- 2; histo[3] <- 4;
 417     histo[4] <- 2; histo[5] <- 2; histo[6] <- 0; histo[7] <- 1;
 418     let l0 = calculeL 0 histo l in
 419      assert {l0 = 0 /\ is_li 0 0 histo};
 420     let l1 = calculeL 1 histo l in
 421      assert {l1 = 0 /\ is_li 1 0 histo};
 422     let l2 = calculeL 2 histo l in
 423      assert {histo[1] < histo[2]};
 424      assert {not is_li 2 1 histo};
 425      assert {l2 = 2 /\ is_li 2 2 histo};
 426     let l3 = calculeL 3 histo l in
 427      assert {l3 = 3 /\ is_li 3 3  histo};
 428     let l4 = calculeL 4 histo l in
 429      assert {l4 = 2 /\ is_li 4 2 histo};
 430     let l5 = calculeL 5 histo l in
 431      assert {l5 = 2 /\ is_li 5 2 histo};
 432     let l6 = calculeL 6 histo l in
 433      assert {l6 = 0 /\ is_li 6 0 histo};
 434     let l7 = calculeL 7 histo l in
 435      assert {l7 = 7 /\ is_li 7 7 histo};
 436      assert {not is_li 7 6 histo};
 437      assert {not is_li 7 5 histo};
 438      assert {not is_li 7 2 histo};
 439
 440 end
 441
 442 module Histo_loop
 443
 444 use int.Int
 445 use int.Lex2
 446 use ref.Ref
 447 use array.Array
 448
 449 predicate is_li (i j: int) (histo : array int) =
 450   0 <= j <= i < histo.length /\
 451  (forall k. j <= k <= i -> histo[k] >= histo[i]) /\
 452  (j > 0 -> histo[j-1] < histo[i])
 453
 454 let rec calculeL_aux i histo l
 455   requires {l.length = histo.length}
 456   requires {0 <= i < histo.length }
 457   ensures  {is_li i result histo}
 458   ensures  {result = l[i]}
 459   variant { i }
 460   =
 461    let j = ref i in
 462     while !j > 0 && histo[!j-1] >= histo[i] do
 463        variant {!j}
 464        invariant {forall k. !j <= k <= i -> histo[k] >= histo[i]}
 465        invariant {0 <= !j <= i }
 466      j := calculeL_aux (!j-1) histo l
 467     done;
 468     l[i] <- !j; !j
 469
 470 let calculeL i histo l
 471   requires {l.length = histo.length}
 472   requires {0 <= i < histo.length }
 473   ensures  {is_li i result histo}
 474   ensures  {result = l[i]}
 475  = calculeL_aux i histo l
 476
 477 let test () =
 478     let histo = make 8 0 in
 479     let l     = make 8 0 in
 480     histo[0] <- 3; histo[1] <- 1; histo[2] <- 2; histo[3] <- 4;
 481     histo[4] <- 2; histo[5] <- 2; histo[6] <- 0; histo[7] <- 1;
 482     let l0 = calculeL 0 histo l in
 483      assert {l0 = 0 /\ is_li 0 0 histo};
 484     let l1 = calculeL 1 histo l in
 485      assert {l1 = 0 /\ is_li 1 0 histo};
 486     let l2 = calculeL 2 histo l in
 487      assert {histo[1] < histo[2]};
 488      assert {not is_li 2 1 histo};
 489      assert {l2 = 2 /\ is_li 2 2 histo};
 490     let l3 = calculeL 3 histo l in
 491      assert {l3 = 3 /\ is_li 3 3  histo};
 492     let l4 = calculeL 4 histo l in
 493      assert {l4 = 2 /\ is_li 4 2 histo};
 494     let l5 = calculeL 5 histo l in
 495      assert {l5 = 2 /\ is_li 5 2 histo};
 496     let l6 = calculeL 6 histo l in
 497      assert {l6 = 0 /\ is_li 6 0 histo};
 498     let l7 = calculeL 7 histo l in
 499      assert {l7 = 7 /\ is_li 7 7 histo};
 500      assert {not is_li 7 6 histo};
 501      assert {not is_li 7 5 histo};
 502      assert {not is_li 7 2 histo};
 503
 504 end*)