Wiki Agenda Contact Version française

Koda-Ruskey's algorithm


Authors: Jean-Christophe Filliâtre / Mário Pereira

Topics: Trees

Tools: Why3

see also the index (by topic, by tool, by reference, by year)



Koda-Ruskey's algorithm

Authors: Mário Pereira (Université Paris Sud) Jean-Christophe Filliâtre (CNRS)

module KodaRuskey_Spec

  use import map.Map
  use import list.List
  use import list.Append
  use import int.Int

  type color = White | Black

  type forest =
    | E
    | N int forest forest

  type coloring = map int color

  function size_forest (f: forest) : int = match f with
    | E -> 0
    | N _ f1 f2 -> 1 + size_forest f1 + size_forest f2
    end

  lemma size_forest_nonneg : forall f.
    size_forest f >= 0

  predicate mem_forest (n: int) (f: forest) = match f with
    | E -> false
    | N i f1 f2 -> i = n || mem_forest n f1 || mem_forest n f2
    end

  predicate between_range_forest (i j: int) (f: forest) =
    forall n. mem_forest n f -> i <= n < j

  predicate disjoint (f1 f2: forest) =
    forall x. mem_forest x f1 -> mem_forest x f2 -> false

  predicate no_repeated_forest (f: forest) = match f with
    | E -> true
    | N i f1 f2 ->
      no_repeated_forest f1 && no_repeated_forest f2 &&
      not (mem_forest i f1) && not (mem_forest i f2) &&
      disjoint f1 f2
    end

  predicate valid_nums_forest (f: forest) (n: int) =
    between_range_forest 0 n f &&
    no_repeated_forest f

  predicate white_forest (f: forest) (c: coloring) = match f with
    | E -> true
    | N i f1 f2 ->
      c[i] = White && white_forest f1 c && white_forest f2 c
  end

  predicate valid_coloring (f: forest) (c: coloring) =
    match f with
    | E -> true
    | N i f1 f2 ->
      valid_coloring f2 c &&
      match c[i] with
      | White -> white_forest f1 c
      | Black -> valid_coloring f1 c
      end
    end

  function count_forest (f: forest) : int = match f with
    | E         -> 1
    | N _ f1 f2 -> (1 + count_forest f1) * count_forest f2
    end

  lemma count_forest_nonneg:
    forall f. count_forest f >= 1

  predicate eq_coloring (n: int) (c1 c2: coloring) =
    forall i. 0 <= i < n -> c1[i] = c2[i]

end

module Lemmas

  use import map.Map
  use import list.List
  use import list.Append
  use import int.Int
  use import KodaRuskey_Spec

  type stack = list forest

  predicate mem_stack (n: int) (st: stack) = match st with
    | Nil       -> false
    | Cons f tl -> mem_forest n f || mem_stack n tl
    end

  lemma mem_app: forall n st1 "induction" st2.
    mem_stack n (st1 ++ st2) -> mem_stack n st1 || mem_stack n st2

  function size_stack (st: stack) : int = match st with
    | Nil -> 0
    | Cons f st -> size_forest f + size_stack st
    end

  lemma size_stack_nonneg : forall st.
    size_stack st >= 0

  lemma white_forest_equiv:
    forall f c.
    white_forest f c <-> (forall i. mem_forest i f -> c[i] = White)

  predicate even_forest (f: forest) = match f with
    | E -> false
    | N _ f1 f2 -> not (even_forest f1) || even_forest f2
    end

  predicate final_forest (f: forest) (c: coloring) = match f with
    | E -> true
    | N i f1 f2 ->
      c[i] = Black && final_forest f1 c &&
      if not (even_forest f1) then white_forest f2 c
      else final_forest f2 c
    end

  predicate any_forest (f: forest) (c: coloring) =
    white_forest f c || final_forest f c

  lemma any_forest_frame:
    forall f c1 c2.
    (forall i. mem_forest i f -> c1[i] = c2[i]) ->
    (final_forest f c1 -> final_forest f c2) &&
    (white_forest f c1 -> white_forest f c2)

  predicate unchanged (st: stack) (c1 c2: coloring) =
    forall i. mem_stack i st -> c1[i] = c2[i]

  predicate inverse (st: stack) (c1 c2: coloring) =
    match st with
    | Nil -> true
    | Cons f st' ->
      (white_forest f c1 && final_forest f c2 ||
       final_forest f c1 && white_forest f c2) &&
      if even_forest f then
        unchanged st' c1 c2
      else
        inverse st' c1 c2
    end

  predicate any_stack (st: stack) (c: coloring) = match st with
    | Nil -> true
    | Cons f st -> (white_forest f c || final_forest f c) && any_stack st c
    end

  lemma any_stack_frame:
    forall st c1 c2.
    unchanged st c1 c2 ->
    any_stack st c1 -> any_stack st c2

  lemma inverse_frame:
    forall st c1 c2 c3.
    inverse   st c1 c2 ->
    unchanged st c2 c3 ->
    inverse   st c1 c3

  lemma inverse_frame2:
    forall st c1 c2 c3.
    unchanged st c1 c2 ->
    inverse   st c2 c3 ->
    inverse   st c1 c3

  let lemma inverse_any (st: stack) (c1 c2: coloring)
    requires { any_stack st c1 }
    requires { inverse st c1 c2 }
    ensures  { any_stack st c2 }
  = ()

  lemma inverse_final:
    forall f st c1 c2.
    final_forest f c1 ->
    inverse (Cons f st) c1 c2 ->
    white_forest f c2

  lemma inverse_white:
    forall f st c1 c2.
    white_forest f c1 ->
    inverse (Cons f st) c1 c2 ->
    final_forest f c2

  let lemma white_final_exclusive (f: forest) (c: coloring)
    requires { f <> E }
    ensures  { white_forest f c -> final_forest f c -> false }
  = match f with E -> () | N _ _ _ -> () end

  lemma final_unique:
    forall f c1 c2.
    final_forest f c1 ->
    final_forest f c2 ->
    forall i. mem_forest i f -> c1[i] = c2[i]

  let rec lemma inverse_inverse
    (st: stack) (c1 c2 c3: coloring)
    requires { inverse st c1 c2 }
    requires { inverse st c2 c3 }
    ensures  { unchanged st c1 c3 }
    variant  { st }
  = match st with
    | Nil -> ()
    | Cons E st' -> inverse_inverse st' c1 c2 c3
    | Cons f st' -> if even_forest f then () else inverse_inverse st' c1 c2 c3
    end

  inductive sub stack forest coloring =
  | Sub_reflex:
      forall f, c. sub (Cons f Nil) f c
  | Sub_brother:
      forall st i f1 f2 c.
      sub st f2 c -> sub st (N i f1 f2) c
  | Sub_append:
      forall st i f1 f2 c.
      sub st f1 c -> c[i] = Black ->
      sub (st ++ Cons f2 Nil) (N i f1 f2) c

  lemma sub_not_nil:
    forall st f c. sub st f c -> st <> Nil

  lemma sub_empty:
    forall st f0 c. st <> Nil -> sub (Cons E st) f0 c ->
    sub st f0 c

  lemma sub_mem:
    forall n st f c.
    mem_stack n st -> sub st f c -> mem_forest n f

  lemma sub_weaken1:
    forall st i f1 f2 f0 c.
    sub (Cons (N i f1 f2) st) f0 c ->
    sub (Cons         f2  st) f0 c

  lemma sub_weaken2:
    forall st i f1 f2 f0 c.
    sub (Cons (N i f1 f2) st) f0 c ->
    c[i] = Black ->
    sub (Cons f1 (Cons f2 st)) f0 c

  lemma not_mem_st: forall i f st c.
    not (mem_forest i f) -> sub st f c -> not (mem_stack i st)

  lemma sub_frame:
    forall st f0 c c'.
    no_repeated_forest f0 ->
    (forall i. not (mem_stack i st) -> mem_forest i f0 -> c'[i] = c[i]) ->
    sub st f0 c ->
    sub st f0 c'

  predicate disjoint_stack (f: forest) (st: stack) =
    forall i. mem_forest i f -> mem_stack i st -> false

  lemma sub_no_rep: forall f st' f0 c.
    sub (Cons f st') f0 c ->
    no_repeated_forest f0 ->
    no_repeated_forest f

  lemma sub_no_rep2: forall f st' f0 c.
    sub (Cons f st') f0 c ->
    no_repeated_forest f0 ->
    disjoint_stack f st'

  lemma white_valid: forall f c.
    white_forest f c -> valid_coloring f c

  lemma final_valid: forall f c.
    final_forest f c -> valid_coloring f c

  lemma valid_coloring_frame:
    forall f c1 c2.
    valid_coloring f c1 ->
    (forall i. mem_forest i f -> c2[i] = c1[i]) ->
    valid_coloring f c2

  lemma valid_coloring_set:
    forall f i c.
    valid_coloring f c ->
    not (mem_forest i f) ->
    valid_coloring f c[i <- Black]

  lemma head_and_tail:
    forall f1 f2: 'a, st1 st2: list 'a.
    Cons f1 st1 = st2 ++ Cons f2 Nil ->
    st2 <> Nil ->
    exists st. st1 = st ++ Cons f2 Nil /\ st2 = Cons f1 st

  lemma sub_valid_coloring_f1:
    forall i f1 f2 c i1.
    no_repeated_forest (N i f1 f2) ->
    valid_coloring (N i f1 f2) c ->
    c[i] = Black ->
    mem_forest i1 f1 ->
    valid_coloring f1 c[i1 <- Black] ->
    valid_coloring (N i f1 f2) c[i1 <- Black]

  lemma sub_valid_coloring:
    forall f0 i f1 f2 st c1.
    no_repeated_forest f0 ->
    valid_coloring f0 c1 ->
    sub (Cons (N i f1 f2) st) f0 c1 ->
    valid_coloring f0 c1[i <- Black]

  lemma sub_Cons_N:
    forall f st i f1 f2 c.
    sub (Cons f st) (N i f1 f2) c ->
    f = N i f1 f2 || (exists st'. sub (Cons f st') f1 c) || sub (Cons f st) f2 c

  lemma white_white:
    forall f c i.
    white_forest f c ->
    white_forest f c[i <- White]

  let rec lemma sub_valid_coloring_white
    (f0: forest) (i: int) (f1 f2: forest) (c1: coloring)
    requires { no_repeated_forest f0 }
    requires { valid_coloring f0 c1 }
    requires { white_forest f1 c1 }
    ensures  { forall st. sub (Cons (N i f1 f2) st) f0 c1 ->
               valid_coloring f0 c1[i <- White] }
    variant  { f0 }
  = match f0 with
    | E -> ()
    | N _ f10 f20 ->
       sub_valid_coloring_white f10 i f1 f2 c1;
       sub_valid_coloring_white f20 i f1 f2 c1
    end

  function count_stack (st: stack) : int = match st with
    | Nil        -> 1
    | Cons f st' -> count_forest f * count_stack st'
    end

  lemma count_stack_nonneg:
    forall st. count_stack st >= 1

  use seq.Seq as S

  type visited = S.seq coloring

  predicate stored_solutions
    (f0: forest) (bits: coloring) (st: stack) (v1 v2: visited) =
    let n = size_forest f0 in
    let start = S.length v1 in
    let stop  = S.length v2 in
    stop - start = count_stack st &&
    (forall j. 0 <= j < start ->
      eq_coloring n (S.get v2 j) (S.get v1 j)) &&
    forall j. start <= j < stop ->
      valid_coloring f0 (S.get v2 j) &&
      (forall i. 0 <= i < n -> not (mem_stack i st) ->
        (S.get v2 j)[i] = bits[i]) &&
      forall k. start <= k < stop -> j <> k ->
        not (eq_coloring n (S.get v2 j) (S.get v2 k))

  let lemma stored_trans1
      (f0: forest) (bits1 bits2: coloring) (i: int) (f1 f2: forest) (st: stack)
      (v1 v2 v3: visited)
    requires { valid_nums_forest f0 (size_forest f0) }
    requires { 0 <= i < size_forest f0 }
    requires { forall j. 0 <= j < size_forest f0 ->
               not (mem_stack j (Cons (N i f1 f2) st)) -> bits2[j] = bits1[j] }
    requires { forall j. S.length v1 <= j < S.length v2 ->
               (S.get v2 j)[i] = White }
    requires { forall j. S.length v2 <= j < S.length v3 ->
               (S.get v3 j)[i] = Black }
    requires { stored_solutions f0 bits1 (Cons f2 st) v1 v2 }
    requires { stored_solutions f0 bits2 (Cons f1 (Cons f2 st)) v2 v3 }
    ensures  { stored_solutions f0 bits2 (Cons (N i f1 f2) st) v1 v3 }
  = ()

  let lemma stored_trans2
      (f0: forest) (bits1 bits2: coloring) (i: int) (f1 f2: forest) (st: stack)
      (v1 v2 v3: visited)
    requires { valid_nums_forest f0 (size_forest f0) }
    requires { 0 <= i < size_forest f0 }
    requires { forall j. 0 <= j < size_forest f0 ->
       not (mem_stack j (Cons (N i f1 f2) st)) -> bits2[j] = bits1[j] }
    requires { forall j. S.length v1 <= j < S.length v2 ->
               (S.get v2 j)[i] = Black }
    requires { forall j. S.length v2 <= j < S.length v3 ->
               (S.get v3 j)[i] = White }
    requires { stored_solutions f0 bits1 (Cons f1 (Cons f2 st)) v1 v2 }
    requires { stored_solutions f0 bits2 (Cons f2 st) v2 v3 }
    ensures  { stored_solutions f0 bits2 (Cons (N i f1 f2) st) v1 v3 }
  = ()

end

module KodaRuskey

  use import seq.Seq as S
  use import list.List
  use import KodaRuskey_Spec
  use import Lemmas
  use map.Map as M
  use import array.Array
  use import int.Int
  use import ref.Ref

  val map_of_array (a: array 'a) : M.map int 'a
    ensures { result = a.elts }

  val ghost visited: ref visited

  let rec enum (bits: array color) (ghost f0: forest) (st: list forest) : unit
    requires { size_forest f0 = length bits }
    requires { valid_nums_forest f0 (length bits) }
    requires { sub st f0 bits.elts }
    requires { st <> Nil }
    requires { any_stack st bits.elts }
    requires { valid_coloring f0 bits.elts }
    variant  { size_stack st, st }
    ensures  { forall i.
                 not (mem_stack i st) -> bits[i] = (old bits)[i] }
    ensures  { inverse st (old bits).elts bits.elts }
    ensures  { valid_coloring f0 bits.elts }
    ensures  { stored_solutions f0 bits.elts st (old !visited) !visited }
  = match st with
    | Nil ->
        absurd
    | Cons E st' ->
       match st' with
       | Nil ->
           (* that's where we visit the next coloring *)
           assert { valid_coloring f0 bits.elts };
           ghost visited := S.snoc !visited (map_of_array bits);
           ()
       | _ ->
           enum bits f0 st'
       end
    | Cons (N i f1 f2 as f) st' ->
        assert { disjoint_stack f1 st' };
        assert { not (mem_stack i st') };
        let ghost visited1 = !visited in
        if bits[i] = White then begin
    'A:   enum bits f0 (Cons f2 st');
          assert { sub st f0 bits.elts };
          let ghost bits1 = map_of_array bits in
          let ghost visited2 = !visited in
    'B:   bits[i] <- Black;
          assert { sub st f0 bits.elts };
          assert { white_forest f1 bits.elts };
          assert { unchanged (Cons f2 st') (at bits 'B).elts bits.elts};
          assert { inverse (Cons f2 st') (at bits 'A).elts bits.elts };
    'C:   enum bits f0 (Cons f1 (Cons f2 st'));
          assert { bits[i] = Black };
          assert { final_forest f1 bits.elts };
          assert { if not (even_forest f1)
                   then inverse (Cons f2 st') (at bits 'C).elts bits.elts &&
                        white_forest f2 bits.elts
                   else unchanged (Cons f2 st') (at bits 'C).elts bits.elts &&
                        final_forest f2 bits.elts };
          ghost stored_trans1 f0 bits1 (map_of_array bits)
    i f1 f2 st' visited1 visited2 !visited
        end else begin
          assert { if not (even_forest f1) then white_forest f2 bits.elts
                   else final_forest f2 bits.elts };
    'A:   enum bits f0 (Cons f1 (Cons f2 st'));
          assert { sub st f0 bits.elts };
          let ghost bits1 = map_of_array bits in
          let ghost visited2 = !visited in
    'B:   bits[i] <- White;
          assert { unchanged (Cons f1 (Cons f2 st'))
                     (at bits 'B).elts bits.elts };
          assert { inverse (Cons f1 (Cons f2 st'))
                     (at bits 'A).elts bits.elts };
          assert { sub st f0 bits.elts };
          assert { if even_forest f1 || even_forest f2
                   then unchanged st' (at bits 'A).elts bits.elts
                   else inverse st' (at bits 'A).elts bits.elts };
    'C:   enum bits f0 (Cons f2 st');
          assert { bits[i] = White };
          assert { white_forest f  bits.elts };
          ghost stored_trans2 f0 bits1 (map_of_array bits)
    i f1 f2 st' visited1 visited2 !visited
       end
    end

  let main (bits: array color) (f0: forest)
    requires { white_forest f0 bits.elts }
    requires { size_forest f0 = length bits }
    requires { valid_nums_forest f0 (length bits) }
    ensures  { S.length !visited = count_forest f0 }
    ensures  { let n = S.length !visited  in
               forall j. 0 <= j < n ->
                 valid_coloring f0 (S.get !visited j) &&
                 forall k. 0 <= k < n -> j <> k ->
                   not (eq_coloring (length bits)
                         (S.get !visited j) (S.get !visited k)) }
  = visited := S.empty;
    enum bits f0 (Cons f0 Nil)

end


download ZIP archive

Why3 Proof Results for Project "."

Theory "koda_ruskey.KodaRuskey_Spec": fully verified in 0.00 s

ObligationsAlt-Ergo (1.01)
size_forest_nonneg---
induction_ty_lex
  1.0.00
count_forest_nonneg---
induction_ty_lex
  1.0.00

Theory "koda_ruskey.Lemmas": fully verified in 14.51 s

ObligationsAlt-Ergo (1.01)CVC3 (2.4.1)CVC4 (1.4)Coq (8.4pl6)Z3 (4.4.0)
mem_app---------------
induction_ty_lex
  1.---------------
split_goal_wp
  1.0.00------------
2.0.05------------
size_stack_nonneg---------------
induction_ty_lex
  1.---------------
split_goal_wp
  1.0.00------------
2.0.01------------
white_forest_equiv---------------
induction_ty_lex
  1.0.02------------
any_forest_frame---------------
induction_ty_lex
  1.---------------
split_goal_wp
  1.0.01------------
2.0.01------------
3.0.04------------
4.0.08------------
any_stack_frame---------------
induction_ty_lex
  1.---------------
split_goal_wp
  1.0.01------------
2.---------------
introduce_premises
  1.---------------
compute_in_goal
  1.---------------
split_goal_wp
  1.0.02------------
2.---0.06---------
inverse_frame---------------
induction_ty_lex
  1.0.07------------
inverse_frame2---------------
induction_ty_lex
  1.0.11------------
VC for inverse_any---------------
induction_ty_lex
  1. VC for inverse_any0.02------------
inverse_final---------------
compute_in_goal
  1.0.03------------
inverse_white---------------
compute_in_goal
  1.0.21------------
VC for white_final_exclusive0.01------------
final_unique---------------
induction_ty_lex
  1.---------------
split_goal_wp
  1.0.00------------
2.0.41------------
VC for inverse_inverse---------------
split_goal_wp
  1. postcondition0.01------------
2. variant decrease0.01------------
3. precondition0.01------------
4. precondition0.01------------
5. postcondition0.01------------
6. postcondition0.18------------
7. variant decrease0.01------------
8. precondition0.01------------
9. precondition0.01------------
10. postcondition0.18------------
sub_not_nil---------------
induction_pr
  1.0.00------------
2.------0.01------
3.0.01------------
sub_empty---------------
induction_pr
  1.0.00------------
2.0.01------------
3.------0.69------
sub_mem---------------
induction_pr
  1.0.00------------
2.------0.02------
3.---------------
simplify_trivial_quantification
  1.------0.04------
sub_weaken1---------------
induction_pr
  1.------0.04------
2.------0.02------
3.---------------
induction_ty_lex
  1.1.00------------
sub_weaken2---------------
induction_pr
  1.------0.05------
2.0.01------------
3.---------------
induction_ty_lex
  1.---------------
split_goal_wp
  1.------------0.02
2.------0.20------
not_mem_st---------------
induction_pr
  1.0.01------------
2.0.01------------
3.0.01------------
sub_frame---------------
induction_pr
  1.0.01------------
2.------0.04------
3.------0.03------
sub_no_rep---------------
induction_pr
  1.0.01------------
2.------0.03------
3.------0.13------
sub_no_rep2---------------
induction_pr
  1.---------------
split_goal_wp
  1.------0.02------
2.---------------
split_goal_wp
  1.------0.03------
3.---------------
split_goal_wp
  1.------1.12------
white_valid---------------
induction_ty_lex
  1.---------------
split_goal_wp
  1.0.00------------
2.0.01------------
final_valid---------------
induction_ty_lex
  1.---------------
split_goal_wp
  1.0.01------------
2.0.01------------
valid_coloring_frame---------------
induction_ty_lex
  1.0.04------------
valid_coloring_set---------------
induction_ty_lex
  1.0.02------------
head_and_tail---------------
induction_ty_lex
  1.0.01------------
sub_valid_coloring_f10.02------------
sub_valid_coloring---------------
induction_pr
  1.---------------
introduce_premises
  1.---------------
compute_in_goal
  1.---------------
split_goal_wp
  1.0.03------------
2.0.01------------
3.0.03------------
2.---------------
introduce_premises
  1.---------------
compute_in_goal
  1.------0.10------
3.---------------
introduce_premises
  1.---------------
simplify_trivial_quantification
  1.---------------
compute_in_goal
  1.---------------
split_goal_wp
  1.---------1.55---
2.0.01---0.04------
3.0.61------------
sub_Cons_N---------------
induction_pr
  1.0.01------------
2.------0.08------
3.------0.02------
white_white0.02------------
VC for sub_valid_coloring_white---------------
split_goal_wp
  1. postcondition0.01------------
2. variant decrease0.01------------
3. precondition0.01------------
4. precondition0.02------------
5. precondition0.01------------
6. variant decrease0.02------------
7. precondition0.01------------
8. precondition0.02------------
9. precondition0.01------------
10. postcondition---------3.47---
count_stack_nonneg---------------
induction_ty_lex
  1.0.01------------
VC for stored_trans1---------------
introduce_premises
  1. VC for stored_trans1---------------
inline_goal
  1. VC for stored_trans1---------------
split_goal_wp
  1. postcondition---------------
split_goal_wp
  1. postcondition0.02------------
2. postcondition0.05------------
3. postcondition0.15------------
4. postcondition0.32------------
5. postcondition1.08------------
VC for stored_trans2---------------
introduce_premises
  1. VC for stored_trans2---------------
inline_goal
  1. VC for stored_trans2---------------
split_goal_wp
  1. postcondition---------------
split_goal_wp
  1. postcondition0.02------------
2. postcondition0.04------------
3. postcondition0.14------------
4. postcondition0.24------------
5. postcondition1.04------------

Theory "koda_ruskey.KodaRuskey": fully verified in 48.72 s

ObligationsAlt-Ergo (1.01)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Z3 (4.4.0)
VC for enum---------------
split_goal_wp
  1. unreachable point0.01------------
2. assertion0.01------------
3. postcondition---------------
introduce_premises
  1. postcondition---------------
compute_in_goal
  1. postcondition---------------
split_goal_wp
  1. VC for enum------0.15------
2. VC for enum------0.07------
3. VC for enum------0.17------
4. postcondition0.02------------
5. postcondition0.02------------
6. variant decrease0.02------------
7. precondition0.01------------
8. precondition0.01------------
9. precondition0.02------------
10. precondition0.01------------
11. precondition------0.08------
12. precondition0.01------------
13. postcondition------0.04------
14. postcondition---------------
introduce_premises
  1. postcondition---------------
compute_in_goal
  1. postcondition---------------
split_goal_wp
  1. VC for enum------0.12------
2. VC for enum------0.08------
3. VC for enum------0.06------
15. postcondition0.01------------
16. postcondition0.25------------
17. assertion------0.73------
18. assertion0.04------------
19. index in array bounds---------0.06---
20. variant decrease0.01------------
21. precondition0.01------------
22. precondition0.01------------
23. precondition0.12------------
24. precondition------0.07------
25. precondition------0.06------
26. assertion------2.14------
27. index in array bounds------0.02------
28. assertion0.93------------
29. assertion------3.80------
30. assertion------3.38------
31. assertion------0.04------
32. variant decrease------0.14------
33. precondition0.00------------
34. precondition0.02------------
35. precondition0.14------------
36. precondition0.06------------
37. precondition0.01------------
38. assertion------0.19------
39. assertion------0.06------
40. assertion------0.15------
41. precondition0.01------------
42. precondition0.02------------
43. precondition------0.24------
44. precondition------0.18------
45. precondition------0.21------
46. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. precondition0.03------------
2. precondition0.03------------
3. precondition0.02------------
4. precondition1.80------------
5. precondition0.21------------
47. precondition------0.05------
48. postcondition------0.15------
49. postcondition---------------
introduce_premises
  1. postcondition---------------
compute_in_goal
  1. postcondition---------------
split_goal_wp
  1. VC for enum------0.22------
2. VC for enum8.84---5.08------
3. VC for enum------0.22------
50. postcondition0.01------------
51. postcondition---------------
split_goal_wp
  1. postcondition---------------
inline_goal
  1. postcondition---------------
split_goal_wp
  1. postcondition0.01------------
2. postcondition------------0.02
3. postcondition0.01------------
4. postcondition------0.10------
5. postcondition------------0.02
52. assertion0.38------------
53. variant decrease0.13------------
54. precondition0.01------------
55. precondition0.01------------
56. precondition0.01------------
57. precondition------0.08------
58. precondition------0.15------
59. assertion---0.20---------
60. index in array bounds---------------
introduce_premises
  1. index in array bounds---------------
inline_goal
  1. index in array bounds------0.03------
61. assertion0.14------------
62. assertion0.02------------
63. assertion2.05------------
64. assertion1.80------------
65. variant decrease0.13------------
66. precondition0.01------------
67. precondition0.01------------
68. precondition0.10------------
69. precondition------0.14------
70. precondition------0.15------
71. assertion------0.17------
72. assertion------5.66------
73. precondition0.01------------
74. precondition0.02------------
75. precondition------0.19------
76. precondition------0.31------
77. precondition------0.21------
78. precondition------0.04------
79. precondition------0.04------
80. postcondition------0.24------
81. postcondition------5.32------
82. postcondition0.02------------
83. postcondition0.03------------
VC for main---------------
split_goal_wp
  1. precondition0.01------------
2. precondition0.01------------
3. precondition0.01------------
4. precondition0.00------------
5. precondition0.01------------
6. postcondition0.01------------
7. postcondition0.02------------