Commit 1b224c62 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example from JC's habilitation defense

parent 54168de0
(* Given a nxn matrix m of nonnegative integers, we want to pick up one element
in each row and each column, so that their sum is maximal.
We generalize the problem as follows: f(i,c) is the maximum for rows >= i
and columns in set c. Thus the solution is f(0,{0,1,...,n-1}).
f is easily defined recursively, as we have
f(i,c) = max{j in c} m[i][j] + f(i+1, C\{j})
As such, it would still be a brute force approach (of complexity n!)
but we can memoize f and then the search space decreases to 2^n-1.
The following code implements such a solution. Sets of integers are
provided in theory Bitset. Hash tables for memoization are provided
in module HashTable (signature) and HashTableImpl (implementation).
Code for f is in module MaxMatrixMemo (mutually recursive functions
maximum and memo).
*)
theory Bitset "sets of small integers"
use import int.Int
function size : int (* elements belong to 0..size-1 *)
type set
(* membership
[mem i s] can be implemented as [s land (1 lsl i) <> 0] *)
predicate mem int set
(* removal
[remove i s] can be implemented as [s - (1 lsl i)] *)
function remove int set : set
axiom remove_def1:
forall x y: int, s: set.
mem x (remove y s) <-> x <> y /\ mem x s
(* the set {0,1,...,n-1}
[below n] can be implemented as [1 lsl n - 1] *)
function below int : set
axiom below_def:
forall x n: int. 0 <= n <= size ->
mem x (below n) <-> 0 <= x < n
function cardinal set : int
axiom cardinal_empty:
forall s: set. cardinal s = 0 <-> (forall x: int. not (mem x s))
axiom cardinal_remove:
forall x: int. forall s: set.
mem x s -> cardinal s = 1 + cardinal (remove x s)
axiom cardinal_below:
forall n: int. 0 <= n <= size ->
cardinal (below n) = if n >= 0 then n else 0
end
module HashTable
use import option.Option
use import int.Int
use import map.Map
type t 'a 'b model {| mutable contents: map 'a (option 'b) |}
function ([]) (h: t 'a 'b) (k: 'a) : option 'b = Map.get h.contents k
val create (n:int) :
{ 0 < n } t 'a 'b { forall k: 'a. result[k] = None }
val clear (h: t 'a 'b) :
{} unit writes h { forall k: 'a. h[k] = None }
val add (h: t 'a 'b) (k: 'a) (v: 'b) :
{}
unit writes h
{ h[k] = Some v /\ forall k': 'a. k' <> k -> h[k'] = (old h)[k'] }
exception Not_found
val find (h: t 'a 'b) (k: 'a) :
{}
'b reads h raises Not_found
{ h[k] = Some result } | Not_found -> { h[k] = None }
end
module HashTableImpl
use import option.Option
use import int.Int
use import int.Abs
use import int.ComputerDivision
use import map.Map
use import list.List
use import list.Mem
use import module array.Array
type t 'a 'b = array (list ('a, 'b))
function get (h: t 'a 'b) (k: 'a) : option 'b
axiom get_None:
forall h: t 'a 'b, k: 'a.
get h k = None <->
(forall i: int. 0 <= i < length h -> forall v: 'b. not (mem (k, v) h[i]))
axiom get_Some:
forall h: t 'a 'b, k: 'a, v: 'b.
get h k = Some v <->
exists i: int. 0 <= i < length h /\ mem (k,v) h[i]
function hash 'a : int
function idx (h: t 'a 'b) (k: 'a) : int =
mod (abs (hash k)) (length h)
predicate inv (h: t 'a 'b) =
length h > 0 /\
forall i: int. 0 <= i < length h ->
forall k: 'a, v: 'b. mem (k,v) h[i] -> idx h k = i
lemma idx_bounds:
forall h: t 'a 'b. inv h -> forall k: 'a. 0 <= idx h k < length h
let create (n:int) =
{ 0 < n }
make n (Nil: list ('a, 'b))
{ inv result /\ forall k: 'a. get result k = None }
let clear (h: t 'a 'b) =
{ inv h }
fill h 0 (length h) Nil
{ inv h /\ forall k: 'a. get h k = None }
let add (h: t 'a 'b) (k: 'a) (v: 'b) =
{ inv h }
let i = idx h k in
h[i] <- Cons (k,v) h[i]
{ inv h &&
get h k = Some v /\ forall k': 'a. k' <> k -> get h k' = get (old h) k' }
exception Not_found
let rec lookup (k: 'a) (l: list ('a, 'b)) : 'b =
{}
match l with
| Nil -> raise Not_found
| Cons (k', v) r -> if k = k' then v else lookup k r
end
{ mem (k, result) l } | Not_found -> { forall v: 'b. not (mem (k, v) l) }
let find (h: t 'a 'b) (k: 'a) =
{ inv h }
let i = idx h k in
lookup k h[i]
{ get h k = Some result } | Not_found -> { get h k = None }
end
module MaxMatrixMemo
use import int.Int
use import int.MinMax
use import map.Map
use import module ref.Ref
function n : int
axiom n_nonneg: 0 <= n
use import Bitset
axiom integer_size: n <= size
function m : map int (map int int)
axiom m_pos: forall i j: int. 0 <= i < n -> 0 <= j < n -> 0 <= m[i][j]
predicate solution (s: map int int) (i: int) =
(forall k: int. i <= k < n -> 0 <= s[k] < n) /\
(forall k1 k2: int. i <= k1 < k2 < n -> s[k1] <> s[k2])
predicate permutation (s: map int int) = solution s 0
type mapii = map int int
function f (s: map int int) (i: int) : int = m[i][s[i]]
clone import sum.Sum with type container = mapii, function f = f
lemma sum_ind:
forall i: int. i < n -> forall j: int.
forall s: map int int. sum s[i <- j] i n = m[i][j] + sum s (i+1) n
use import option.Option
use module HashTable as H
type key = (int, set)
type value = (int, mapii)
predicate pre (k: key) =
let (i, c) = k in
0 <= i <= n /\ cardinal c = n-i /\ (forall k: int. mem k c -> 0 <= k < n)
predicate post (k: key) (v: value) =
let (i, c) = k in
let (r, sol) = v in
0 <= r /\ solution sol i /\
(forall k: int. i <= k < n -> mem sol[k] c) /\
r = sum sol i n /\
(forall s: map int int.
solution s i -> (forall k: int. i <= k < n -> mem s[k] c) ->
r >= sum s i n)
type table = H.t key value
val table: table
predicate inv (t: table) =
forall k: key, v: value. H.([]) t k = Some v -> post k v
let rec maximum (i:int) (c: set) : (int, map int int) variant {2*n-2*i} =
{ pre (i, c) /\ inv table }
if i = n then
(0, const 0)
else begin
let r = ref (-1) in
let sol = ref (const 0) in
for j = 0 to n-1 do
invariant {
inv table /\
( (!r = -1 /\ forall k: int. 0 <= k < j -> not (mem k c))
\/
(0 <= !r /\ solution !sol i /\
(forall k: int. i <= k < n -> mem !sol[k] c) /\
!r = sum !sol i n /\
(forall s: map int int.
solution s i -> (forall k: int. i <= k < n -> mem s[k] c) ->
mem s[i] c -> s[i] < j -> !r >= sum s i n)))
}
if mem j c then
let (r', sol') = memo (i+1) (remove j c) in
let x = m[i][j] + r' in
if x > !r then begin r := x; sol := sol'[i <- j] end
done;
assert { 0 <= !r };
(!r, !sol)
end
{ post (i,c) result /\ inv table }
with memo (i:int) (c: set) : (int, map int int) variant {2*n-2*i+1} =
{ pre (i,c) /\ inv table }
try H.find table (i,c)
with H.Not_found -> let r = maximum i c in H.add table (i,c) r; r end
{ post (i,c) result /\ inv table }
let maxmat () =
{ }
H.clear table;
assert { inv table };
let (r, _) = maximum 0 (below n) in r
{ (exists s: map int int. permutation s /\ result = sum s 0 n) /\
(forall s: map int int. permutation s -> result >= sum s 0 n) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/max_matrix.gui"
End:
*)
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment