## 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

Obligations | Alt-Ergo (0.99.1) |

dyck_word_first | 0.02 |

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

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | ||

VC for same_prefix | 0.04 | --- | --- | --- | ||

VC for is_dyck_rec | --- | --- | --- | --- | ||

split_goal_wp | ||||||

1. variant decrease | 0.02 | --- | --- | --- | ||

2. assertion | --- | --- | --- | --- | ||

split_goal_wp | ||||||

1. assertion | --- | 0.49 | --- | --- | ||

2. assertion | 0.55 | --- | --- | --- | ||

3. assertion | --- | 0.04 | --- | --- | ||

3. variant decrease | 0.05 | --- | --- | --- | ||

4. postcondition | --- | --- | --- | --- | ||

split_goal_wp | ||||||

1. VC for is_dyck_rec | 0.38 | --- | --- | --- | ||

2. VC for is_dyck_rec | 0.01 | --- | --- | --- | ||

3. VC for is_dyck_rec | 0.12 | --- | --- | --- | ||

4. VC for is_dyck_rec | --- | --- | 0.88 | --- | ||

5. VC for is_dyck_rec | 0.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_rec | 0.01 | --- | --- | --- | ||

2. VC for is_dyck_rec | 0.01 | --- | --- | --- | ||

3. VC for is_dyck_rec | 0.01 | --- | --- | --- | ||

4. VC for is_dyck_rec | 1.21 | --- | --- | --- | ||

5. VC for is_dyck_rec | 0.02 | --- | --- | --- | ||

9. postcondition | --- | --- | --- | --- | ||

split_goal_wp | ||||||

1. VC for is_dyck_rec | 0.01 | --- | --- | --- | ||

2. VC for is_dyck_rec | 0.01 | --- | --- | --- | ||

3. VC for is_dyck_rec | 0.00 | --- | --- | --- | ||

4. VC for is_dyck_rec | 0.02 | --- | --- | --- | ||

5. VC for is_dyck_rec | 0.02 | --- | --- | --- | ||

VC for is_dyck | --- | --- | --- | --- | ||

split_goal_wp | ||||||

1. postcondition | 0.02 | --- | --- | --- | ||

2. postcondition | --- | --- | --- | --- | ||

3. postcondition | --- | --- | --- | 0.02 |