Wiki Agenda Contact Version française

Checking that a word is a Dyck word


Authors: Jean-Christophe Filliâtre / Martin Clochard

Topics: Graph Algorithms

Tools: Why3

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



Checking that a word is a Dyck word

Authors: Martin Clochard (École Normale Supérieure) Jean-Christophe Filliâtre (CNRS)

theory Dyck

  use export list.List
  use export list.Append

  type paren = L | R

  type word = list paren

  (* D -> eps | L D R D *)
  inductive dyck word =
  | Dyck_nil:
      dyck Nil
  | Dyck_ind:
      forall w1 w2. dyck w1 -> dyck w2 -> dyck (Cons L (w1 ++ Cons R w2))

  (* the first letter, if any, must be L *)
  lemma dyck_word_first:
    forall w: word. dyck w ->
    match w with Nil -> true | Cons c _ -> c = L end

end

module Check

  use import Dyck
  use import list.Length
  use import ref.Ref

  exception Failure

  (* A fall of a word is a decomposition p ++ s with p a dyck word
     and s a word not starting by L. *)
  predicate fall (p s: word) = dyck p /\
    match s with Cons L _ -> false | _ -> true end

  let rec lemma same_prefix (p s s2: word) : unit
    requires { p ++ s = p ++ s2 }
    ensures { s = s2 }
    variant { p }
  = match p with Nil -> () | Cons _ q -> same_prefix q s s2 end

  (* Compute the fall decomposition, if it exists. As a side-effect,
     prove its unicity. *)
  let rec is_dyck_rec (ghost p: ref word) (w: word) : word
    ensures { w = !p ++ result && fall !p result &&
      (forall p2 s: word. w = p2 ++ s /\ fall p2 s -> p2 = !p && s = result) }
    writes { p }
    raises  { Failure -> forall p s: word. w = p ++ s -> not fall p s }
    variant { length w }
  =
    match w with
    | Cons L w0 ->
      let ghost p0 = ref Nil in
      match is_dyck_rec p0 w0 with
      | Cons _ w1 ->
        assert { forall p s p1 p2: word.
          dyck p /\ w = p ++ s /\ dyck p1 /\ dyck p2 /\
          p = Cons L (p1 ++ Cons R p2) ->
          w0 = p1 ++ (Cons R (p2 ++ s)) && p1 = !p0 && w1 = p2 ++ s };
        let ghost p1 = ref Nil in
        let w = is_dyck_rec p1 w1 in
        p := Cons L (!p0 ++ Cons R !p1);
        w
      | _ ->
        raise Failure
      end
    | _ ->
      p := Nil; w
    end

  let is_dyck (w: word) : bool
    ensures { result <-> dyck w }
  =
    try match is_dyck_rec (ref Nil) w with
      | Nil -> true
      | _ -> false
    end with Failure -> false end

end


download ZIP archive

Why3 Proof Results for Project "dyck"

Theory "dyck.Dyck": fully verified in 0.02 s

ObligationsAlt-Ergo (0.99.1)
dyck_word_first0.02

Theory "dyck.Check": fully verified in 10.51 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)
VC for same_prefix0.04---------
VC for is_dyck_rec------------
split_goal_wp
  1. variant decrease0.02---------
2. assertion------------
split_goal_wp
  1. assertion---0.49------
2. assertion0.55---------
3. assertion---0.04------
3. variant decrease0.05---------
4. postcondition------------
split_goal_wp
  1. VC for is_dyck_rec0.38---------
2. VC for is_dyck_rec0.01---------
3. VC for is_dyck_rec0.12---------
4. VC for is_dyck_rec------0.88---
5. VC for is_dyck_rec0.39---------
5. exceptional postcondition---1.02------
6. exceptional postcondition------1.87---
7. exceptional postcondition------1.32---
8. postcondition------------
split_goal_wp
  1. VC for is_dyck_rec0.01---------
2. VC for is_dyck_rec0.01---------
3. VC for is_dyck_rec0.01---------
4. VC for is_dyck_rec1.21---------
5. VC for is_dyck_rec0.02---------
9. postcondition------------
split_goal_wp
  1. VC for is_dyck_rec0.01---------
2. VC for is_dyck_rec0.01---------
3. VC for is_dyck_rec0.00---------
4. VC for is_dyck_rec0.02---------
5. VC for is_dyck_rec0.02---------
VC for is_dyck------------
split_goal_wp
  1. postcondition0.02---------
2. postcondition------------
3. postcondition---------0.02