Verified Decision Procedures on Context-Free
Grammars
Yasuhiko Minamide
Department of Computer Science
University of Tsukuba
minamide@cs.tsukuba.ac.jp

Abstract. We verify three decision procedures on context-free grammars utilized in a program analyzer for a server-side programming language. One of the procedures decides inclusion between a context-freelanguage and a regular language. The other two decide decision problems related to the well-formedness and validity of XML documents.
From its formalization, we generate executable code for a balancedness
checking procedure and incorporate it into an existing program analyzer.

1

Introduction

We have been developing a program analyzer for the server-side scripting language PHP, which approximates the string output of a program with a contextfree grammar [8]. We adopted and developed several advanced decision procedures on context-free grammars to check properties of a program with theanalyzer [9, 17]. Although the correctness of those decision procedures is often
intuitively clear, their detailed proofs can be rather complicated. That motivatedus to verify them by using a proof assistant.
In this paper, we verify three procedures on context-free grammars used in
our analyzer in Isabelle/HOL [13]. They decide the following three problems:– inclusion between a context-free language and a regular language;– whether a context-free language is balanced or not;– inclusion between a context-free language and a regular hedge language.
The second and third procedures are used to check the well-formedness andvalidity, respectively, of dynamically generated XML documents in the analyzer.
Of the three decision procedures, we generated executable code of the second,
the balancedness checking procedure, with Isabelle’s code generator. Although
the formalization of the procedure is almost executable, the formalization must
be revised to obtain executable code and achieve reasonable eﬃciency. We incorporated the generated code into the PHP string analyzer by replacing thecorresponding handwritten code. The analyzer with the generated code has been
applied successfully to real PHP programs.
Our formalization and veriﬁcation were conducted using the development
version of Isabelle. We made positive use of new features introduced in thedevelopment version, such as a new function deﬁnition package by Krauss [7]and the revised locale mechanism, which make it possible to write proof scripts
in a more natural manner. The proof scripts of the formalization in this paper
are available from http://www.score.cs.tsukuba.ac.jp/~minamide/cfgv/.

2

Context-Free Grammars

In this section, we formalize context-free grammars (CFGs) and several basic
procedures on them. The decision procedures in this paper are based on interpretation of a CFG over a monoid. The interpretation can be naturally formalized
by considering a CFG over the monoid. Thus, we extend the notion of CFGs
and formalize CFGs over a monoid.
2.1

Formalization of CFGs

To simplify our formalization, we only consider a grammar in a normal form
such that each production has one of the forms: x → a and x → yz where x,y, and z are nonterminals (variables) and a is a terminal. A CFG is represented
with the following record type:
record ( v , a) cfg =prod1 :: ( v × a) set
prod2 :: ( v × v × v ) set
start :: v

where v and a are the types of nonterminals and terminals, respectively. Thisdeclaration introduces a record type with three ﬁelds prod1, prod2, and start.
The ﬁelds prod1 and prod2 contain productions of the form x → a and x → yz,
respectively. A component of a record can be accessed with the ﬁeld name, e.g.;
prod1 r accesses the prod1 ﬁeld of a record r. A CFG over strings is modeledwith type ( v , a list) cfg. Note that this type permits a production of the formx → w for any sting w. Thus, the normal form above is not as strict as Chomsky
normal form.
Although a grammar itself can be given without considering a monoid operation, the operation is necessary to deﬁne the language of the grammar. The setof monoid elements generated from a nonterminal is deﬁned as an inductively
deﬁned relation: (x ,v ) ∈ derive cfg opr formalizes “v is derived from nonterminal
x ”.
derive :: [( v , a) cfg, [ a, a] ⇒ a] ⇒ ( v × a) set
inductive derive cfg opr(x ,v ) ∈ prod1 cfg =⇒ (x ,v ) ∈ derive cfg opr[[(y,v ) ∈ derive cfg opr ; (z ,w ) ∈ derive cfg opr ; (x ,y,z ) ∈ prod2 cfg ]] =⇒(x ,opr v w ) ∈ derive cfg opr

For a CFG over strings, concatenation of lists, the inﬁx operator @ in Isabelle,
is used for opr. Although this relation is deﬁned even if opr does not satisfy thelaws of monoids, we only use opr satisfying the laws in this paper. The languageof a CFG is the set of monoid elements derived from the start symbol.

lang-of :: [( v , a) cfg, [ a, a] ⇒ a] ⇒ a set
lang-of cfg opr ≡ { v . (start cfg, v ) ∈ derive cfg opr }2.2

Computing the Language of a CFG over a Finite Monoid

The language of a CFG can also be characterized as a ﬁxed point of a monotonefunction over v ⇒ a set below.
onestep :: [( v , a) cfg, [ a, a] ⇒ a, v ⇒ a set] ⇒ v ⇒ a set
onestep cfg opr m x ≡ m x ∪ {v . (x ,v ) ∈ prod1 cfg} ∪{opr v w | v w . ∃ y z . (x ,y,z ) ∈ prod2 cfg ∧ v ∈ m y ∧ w ∈ m z }The ﬁxed point of this function can be computed if we consider a CFG over afinite monoid. The procedure can be formalized as follows using the predeﬁned
while-combinator in Isabelle.
compute-langs :: [( v , a) cfg, [ a, a] ⇒ a, v ] ⇒ a set
compute-langs cfg opr ≡while (λx . onestep cfg opr x = x ) (onestep cfg opr ) (λx . {})The following equality is proved by the rule of Hoare logic for while formalized
in Isabelle.
theorem fixes cfg::( v ::finite, a::finite) cfg
shows compute-langs cfg opr x = {v . (x ,v ) ∈ derive cfg opr }To guarantee that the while loop terminates, both the sets of nonterminals andterminals must be ﬁnite. The constraints are given as the type class finite of v
and a.
2.3

Image of a Context-Free Language

An interpretation of a CFG with a monoid is considered as an image of its
language under a homomorphism to the monoid.
Let us consider a homomorphism h between monoids a and b. A standard
result of the theory of CFGs is that the image of a context-free language (CFL)
over a under the homomorphism h is a CFL over b. This is shown by constructing a grammar over b as follows:
image-of :: [( v , a) cfg, a ⇒ b] ⇒ ( v , b) cfg
image-of cfg f ≡(| prod1 = prod1 cfg
rel-of f , prod2 = prod2 cfg, start = start cfg |)where s  t is the composition1 of two relations and rel-of converts a function
into a relation.
s1t ≡ {(x ,z ). ∃ y. (x ,y) ∈ s ∧ (y,z ) ∈ t}

rel-of f ≡ {(x ,y). f x = y}

The order of the arguments is diﬀerent from the standard composition operator in
Isabelle/HOL.

Then, the following formalizes the result above.
theorem assumes ∀ v w . h (opr v w ) = opr  (h v ) (h w )shows lang-of (image-of cfg h) opr  = h ‘ lang-of cfg opr

where h ‘ xs is the image of the set xs under the function h.
2.4

Reachable and Generating Nonterminals

We formalize two basic procedures on CFGs: computing the set of reachable
nonterminals and computing the set of generating nonterminals. The latter procedure is then extended to generate a witness for each generating nonterminal.
∗

We say a nonterminal X is reachable if there exists a derivation S ⇒ αXβwhere α and β are strings over terminals and nonterminals, and S is the startsymbol. The standard procedure to compute the set of reachable nonterminals
applies depth-ﬁrst search by considering production rules as a graph.
A CFG is converted into a graph with next-rel and, we formalize reachability
based on the graph as follows.
next-rel cfg ≡ {(x ,y). ∃ z . (x ,y,z ) ∈ prod2 cfg} ∪ {(x ,z ). ∃ y. (x ,y,z ) ∈ prod2 cfg}
reachable cfg xs ≡ (next-rel cfg)∗ ‘‘ xs

where r ‘‘ xs is the image of the set xs under the relation r.
We formalize a depth-ﬁrst search to compute the set of reachable nonterminals as follows.
functiondfs :: [( v ::finite, a) cfg, v list, v set] ⇒ v set where
dfs cfg [] ys = ys
dfs cfg (x #xs) ys =(if x ∈ ys then dfs cfg xs ys else dfs cfg (nexts cfg x @xs) (insert x ys))

The function nexts cfg x computes a list of nodes adjacent to x. This formalization is almost identical to a depth-ﬁrst search we write in a functional programming language. It is shown that this function always terminates by a lexicographic order similar to that used by Moore in his formalization of a graphsearch algorithm [10]. The correctness of this procedure is veriﬁed as the following theorem.
theorem dfs cfg (nexts cfg x ) {x } = reachable cfg {x }∗We say a nonterminal X is generating if X ⇒ w where w is a terminal string.
The following is a formalization of a standard algorithm to compute generating
nonterminals, which is considered as a ﬁxed-point computation.
genv-onestep :: [( v , a) cfg, v set] ⇒ v set
genv-onestep cfg m ≡ m ∪ {x . ∃ y z . (x ,y,z ) ∈ prod2 cfg ∧ y ∈ m ∧ z ∈ m}
genv :: ( v , a) cfg ⇒ v set
genv cfg ≡while (λx . genv-onestep cfg x = x ) (genv-onestep cfg) {x . ∃ v . (x ,v ) ∈ prod1 cfg}

Each iteration adds the nonterminals that are shown to be generating by genvonestep from the nonterminals obtained in the previous iteration. The correctness of the function is proved as follows.
lemma fixes cfg::( v ::finite, a) cfg
shows genv cfg = {x . ∃ w . (x ,w ) ∈ derive cfg opr }The function genv is extended to obtain a map of type s  t, which gives
a witness for each generating nonterminal, i.e., a string generated from it. Types  t is a synonym of s ⇒ t option. The extended procedure is used in thebalancedness checking procedure in Section 4.
To extend genv naturally, we use the function choose deﬁned below
choose xs ≡ if xs = {} then Some (SOME x . x ∈xs) else None

The expression SOME x . P x represents an arbitrary element x satisfying P x.
If there is no such element, it is an arbitrary element.
We thus obtain the following function that gives a witness for each generating
nonterminal.
genv-onestep  :: [( v , a) cfg, [ a, a] ⇒ a, v  a] ⇒ v  agenv-onestep  cfg opr m ≡(λx . if x ∈ dom m then m xelse choose {opr w1 w2 | w1 w2 . ∃ y z . (x ,y,z ) ∈ prod2 cfg ∧ m y = Some w1 ∧m z = Some w2 })genv  :: [( v , a) cfg, [ a, a] ⇒ a] ⇒ v  agenv  cfg opr ≡ while (λx . genv-onestep  cfg opr x = x ) (genv-onestep  cfg opr )(λx . choose {v . (x ,v ) ∈ prod1 cfg})

The structures of genv and genv  are almost identical, and thus we can easily
show the following lemma.
lemma fixes cfg::( v ::finite, a) cfg shows dom (genv  cfg opr ) = genv cfg

3

Decision Procedure for Inclusion between a CFL and a
Regular Language

We verify a decision procedure checking inclusion L(G) ⊆ L(M ) for a CFG G anda nondeterministic ﬁnite automaton M . Textbooks on formal languages usuallydescribe a decision procedure for this problem based on product construction of apushdown automaton and a ﬁnite automaton. On the other hand, the procedurein this section directly operates on a grammar. It is a variant of the contextfree graph reachability algorithm of Reps [15]. We use Nipkow’s formalization of
automata in Isabelle [12].

3.1

Nipkow’s Formalization of Automata

We review Nipkow’s formalization of nondeterministic automata. Nipkow formalized an automaton as a triple of a start state, a transition function, and a
predicate deﬁning ﬁnal states. The following is its reformulation with a record
type:
record ( a, s) na =start :: snext :: [ a, s] ⇒ s set
fin :: s ⇒ boolwhere a and s are the types of an alphabet and states, respectively. The formalization itself allows the set of states to be inﬁnite.
Then, the extended transition function delta over lists and the function accepts describing accepted strings are deﬁned in the standard manner:delta A [] p = {p}delta A (a#w ) p = Union(delta A w ‘ next A a p)
accepts A w ≡ ∃ q ∈ delta A w (start A). fin A q

where the function Union gives the union of a set of sets and has type a set set⇒ a set.
3.2

Transition Monoid

The following theorem states that a regular language is characterized by a ﬁnite
monoid [4].
Theorem 1. Let Σ be a finite alphabet. The following are equivalent for L ⊆Σ∗.
1. L is regular.
2. There exist a finite monoid M, a homomorphism h : Σ ∗ → M, a subset
B ⊆ M such that L = h−1 (B).
One of the easiest ways to construct the monoid, the homomorphism, and thesubset in the theorem is to consider a monoid of relations over states, where thecomposition of relations plays the role of the monoid operation. This monoid ofrelations over states and the homomorphism associated with it implicitly appear
in Nipkow’s formalization. The function steps in the formalization translates astring into a relation and has the following property.
steps A w = {(p,q). q ∈ delta A w p}

This function plays the role of the homomorphism in the theorem.
In addition to Nipkow’s formalization, we introduce the following function,
where final-of na plays the role of B in the theorem for the nondeterministic
automaton na.

final-of :: ( a, s) na ⇒ ( s × s) set set
final-of na ≡ {r . ∃ q. (start na, q) ∈ r ∧ fin na q}

Then, the following is a formalization of the theorem in Isabelle, which can beeasily proved with the lemmas provided in Nipkow’s formalization.
theorem steps na w ∈ final-of na ←→ accepts na w

3.3

Decision Procedure

With the formalization of CFGs and automata, it is quite easy to formalize adecision procedure to check inclusion between the languages of a CFG and anondeterministic ﬁnite automaton. The inclusion can be checked by interpretinga grammar with the monoid characterizing the regular language. We obtain theexpression to compute the interpretation over ( s × s) set as follows.
(steps na) ‘ lang-of cfg (op @)= lang-of (image-of cfg (steps na)) (op )= compute-langs (image-of cfg (steps na)) (op) (start cfg)

This can then be used as the decision procedure as follows.
theorem fixes cfg :: ( v ::finite, a list) cfg and na :: ( a, s::finite) na
shows lang-of cfg (op @) ⊆ {w . accepts na w } ←→compute-langs (image-of cfg (steps na)) (op ) (start cfg) ⊆ final-of na

The type system of Isabelle recognizes that the type ( s × s) set is an instanceof finite from s::finite. Hence, we can compute the language and decide inclusion
between ﬁnite sets of type ( s × s) set.

4

Balancedness Checking Procedure

We introduce a CFG over a paired alphabet and verify a balancedness checking
procedure that decides whether the language of a grammar is balanced or not.
The procedure was developed by Berstel and Boasson [2] and the formalizationin this paper is based on [9].
4.1Balanced Strings

For a base alphabet A, we consider a paired alphabet consisting of two sets Á
and À:Á = { á | a ∈ A }À = { à | a ∈ A }The elements of Á and À are considered as left and right parentheses: á and àmatch. The fundamental notion on a string over a paired alphabet is whether it
is balanced. For example, áb́b̀ćc̀à and áàb́b̀ are balanced, but áb̀ and áb́b̀ are not.
We call the set of all balanced strings the Dyck set [1]. A language L is balanced
if all φ ∈ L are balanced.
We formalize strings over a paired alphabet as lists over the following data
type.

datatype

a balphabet = L a | R aThen, the set of balanced strings, the Dyck set, is formalized as the following
inductively deﬁned set.
dyckset :: a balphabet list set
inductive dyckset[] ∈ dycksetxs ∈ dyckset =⇒ [L x ]@xs@[R x ] ∈ dyckset[[xs ∈ dyckset; ys ∈ dyckset ]] =⇒ xs@ys ∈ dyckset

4.2

Monoid for Balancedness Checking

The Dyck set is not regular and thus cannot be characterized with a ﬁnite
monoid. However, there is an inﬁnite monoid, that makes it possible to decide
whether the language of a CFG is balanced or not.
We say a string φ is partially balanced if it is a substring of some balanced
string. Each partially balanced φ can be uniquely factorized into the followingform:
φ = φ1 à1 φ2 à2 . . . φn àn ϕb́m ψm · · · b́2 ψ2 b́1 ψ1
where φi , ψi , and ϕ are all balanced. We say à1 à2 . . . àn b́m · · · b́2 b́1 the reduced
form of the string and write ρ(φ) for it. The set of reduced forms À∗ Á∗ with ⊥constitute a monoid, where ⊥ represents the reduced form of unbalanced strings.
The balancedness checking procedure is developed based on this monoid.
We formalize the monoid over À∗ Á∗ ∪ { ⊥ } with the following data type:
datatype a bmonoid =B a list a list | Bot

where B [a1 , a2 , . . . , an ] [b1 , b2 , . . . , bm ] represents à1 à2 . . . àn b́m · · · b́2 b́1 , and B [][] is the unit of the monoid.
Let φ and ψ be partially balanced strings. The monoid operation between
their reduced forms is deﬁned by considering that of their concatenation φψ. It
is formalized as follows.
functionconcat :: [ a bmonoid , a bmonoid ] ⇒ a bmonoid (infixr ♦ 65 ) whereB cs1 [] ♦ B cs2 ss2 = B (cs1 @cs2 ) ss2
B cs1 ss1 ♦ B [] ss2 = B cs1 (ss2 @ss1 )B cs1 (s#ss1 ) ♦ B (c#cs2 ) ss2 = (if s = c then B cs1 ss1 ♦ B cs2 ss2 else Bot)
Bot ♦ y = Botx ♦ Bot = Bot

Intuitively, it is clear that this operation is associative. On the other hand, theproof of this is not straightforward. We derive an equivalent deﬁnition of thefunction using the preﬁx relation of lists and prove associativity based on thedeﬁnition.
With the monoid laws of a bmonoid, it is straightforward to show thath deﬁned below is a homomorphism from lists over a paired alphabet to themonoid.

hom-of :: [ a ⇒ b bmonoid , a list] ⇒ b bmonoid
hom-of h [] = B [] []hom-of h (x #xs) = h x ♦ hom-of h xs
h ≡ hom-of (λx . case x of L x ⇒ B [] [x ] | R x ⇒ B [x ] [])Finally, we show that the Dyck set is characterized by this monoid.
theorem xs ∈ dyckset ←→ h xs = B [] []The implication from left to right is easily proved by induction on the derivationof xs ∈ dyckset. The other direction is rather diﬃcult to prove. We introduce a
notion similar to the partially balanced string as an inductively deﬁned set andprove: xs ∈/ dyckset −→ h xs = B [] [].
For balancedness checking, we also introduce an ordering over reduced forms,
which was used to improve the time complexity of a balancedness checking procedure in [9]. The ordering is deﬁned as follows.
à1 · · · àn ćm · · · ć1 ≤ à1 · · · àn b̀1 · · · b̀j b́j · · · b́1 ćm · · · ć1This is formalized as the following order over bmonoid.
b1 ≤ b2 ≡ (∃ cs ss zs. b1 = B cs ss ∧ b2 = B (cs@zs) (ss@zs))∨ (b1 = Bot ∧ b2 = Bot)

4.3

Decision Procedure

Because the monoid introduced in the previous subsection is inﬁnite, it does notdirectly give rise to a balancedness checking procedure. However, it is shownthat balancedness can be checked by generating the monoid elements derived
from each nonterminal to some bound.
In this section, we assume that a CFG is reduced. This means that every
nonterminal is accessible from the start symbol and every nonterminal produces
at least one terminal string. This condition is expressed with the following conditions on cfg in Isabelle.
∀ x . x ∈ reachable cfg {start cfg}

∀ x . ∃ w . (x , w ) ∈ derive cfg opr

Because we assume that a grammar is reduced, for each nonterminal X, we∗∗
can ﬁnd terminal strings φ1 and φ2 such that S ⇒ φ1 Xφ2 . We then have S ⇒∗φ1 ψφ2 for any ψ such that X ⇒ ψ. For φ1 ψφ2 to be balanced, the reduced formsof φ1 and φ2 must be the following forms: ρ(φ1 ) = án . . . á1 and ρ(φ2 ) = b̀1 · · · b̀m .
Furthermore, we have ρ(ψ) ≤ àn . . . à1 b́1 · · · b́m . This observation is formalized
as the following lemmas for bmonoid.
lemma assumes b1 ♦ b2 ♦ b3 = B [] []shows (∃ ss. b1 = B [] ss) ∧ (∃ cs. b3 = B cs [])lemma assumes B [] ss ♦ b ♦ B cs [] = B [] [] shows b ≤ B ss cs

These properties enable us to use àn . . . à1 b́1 · · · b́m above as a bound when wecheck the balancedness of the language of a grammar.
We have the following decision procedure based on the observation so far byconsidering the interpretation of a CFG over the monoid.
∗

1. Compute φ1 and φ2 such that S ⇒ φ1 Xφ2 for each nonterminal X.
2. Generate the monoid elements derived from each nonterminal to the bounddetermined by φ1 and φ2 .
3. If the bound is exceeded for some nonterminal, then the language is notbalanced. Otherwise, the language is balanced iﬀ the start symbol only generates the unit element, i.e., B [] [] in Isabelle.
The ﬁrst step of the procedure is based on the procedures to compute reachable and generating nonterminals. First, we must compute a witness for eachgenerating nonterminal by the procedure in Section 2.4. Then, we apply a depthﬁrst search procedure to compute φ1 and φ2 above. Then, from φ1 and φ2 , thebound is constructed by the following function.
mkbound (B [] ss, B cs []) = B ss cs

The depth-ﬁrst search procedure computes paths from the start symbol to all
the reachable nonterminals, where a path corresponds to a pair φ1 and φ2 above.
Please refer to the proof script for details.
The second step of the procedure is easily formalized as follows, where thebound is given as a function bounds.
compute-langs  :: [( v , a) cfg, [ a, a] ⇒ a, v ⇒ a set, v ] ⇒ a set
compute-langs  cfg opr bounds ≡while (λm. onestep cfg opr m = m ∧ (∀ x . m x ⊆ bounds x ))(onestep cfg opr ) (λx . {})If bounds x is ﬁnite for all x, the function terminates.
The following is the formalization of the whole decision procedure, where
mkcon is the depth-ﬁrst search procedure and ﬁnds a bound, a pair of φ1 and φ2
above, for each nonterminal by using a function gf giving a generated monoid
element for each nonterminal.
bcheck cfg ≡(let gf = λx . the (genv  cfg (op ♦) x );con = λx . the (mkcon (op ♦) (B [] []) cfg gf (start cfg) x ) in(∀ x . ∃ ss cs. con x = (B [] ss, B cs [])) ∧(let bounds = λx . {b. b ≤ mkbound (con x )};result = compute-langs  cfg (op ♦) bounds in∀ x . result x ≤ bounds x ∧ result (start cfg) = {B [] []}))

The correctness of this procedure is veriﬁed in the following sense.
theorem fixes cfg::( v ::finite, a balphabet list) cfg
assumes ∀ x . ∃ w . (x , w ) ∈ derive cfg (op @)∀ x . x ∈ reachable cfg {start cfg}
shows bcheck (image-of cfg h) ←→ lang-of cfg (op @) ⊆ dyckset

5

Decision Procedure for Inclusion between a
Context-Free Language and a Regular Hedge Language

We formalize a decision procedure deciding inclusion between a context-freelanguage and a regular hedge language [11]. The procedure can be considered
as a combination of the previous two decision procedures, and was developed byMinamide and Tozawa [9].
5.1Hedges and Balanced Strings

We call a sequence of trees over the unranked alphabet Σ a hedge. The sets oftrees and hedges denoted by t and h are deﬁned as follows:t ::= a hh ::= | t hwhere a ∈ Σ. We write H(Σ) for the set of hedges over Σ. By expanding t in
the deﬁnition of hedges, hedges can also be deﬁned as follows.
h ::= | a h h
We formalize this deﬁnition as the following datatype in Isabelle.
datatype a hedge = Empty | Br a a hedge a hedge

Hedges can be considered as balanced strings by the following function.
hedge2word :: a hedge ⇒ a balphabet list
hedge2word Empty = []hedge2word (Br a xs ys) = [L a]@hedge2word xs@[R a]@hedge2word ys

It is shown that this function is injective and its range is the set of balanced
strings. The key to proving these properties is the following property of balanced
strings. It is proved by using the monoid in Section 4.
lemma assumes [L a]@xs1 @[R a]@xs2 = [L a]@ys1 @[R a]@ys2
xs1 ∈ dyckset ys1 ∈ dyckset
shows xs1 =ys1 ∧ xs2 = ys2

5.2

Regular Hedge Grammars and Binoids

A regular hedge grammar (RHG) is a grammar over hedges with production
rules of the following forms.
X→

X→a Y ZThe set of hedges generated by a RHG is called a regular hedge language (RHL).
It is basically a regular tree language over an unranked alphabet.
RHGs are formalized with the following record type as CFGs, and the derivation and the language of a RHG are formalized in the same manner as those of
CFGs.

record ( v , a) rhg =prod1 :: v set
prod2 :: ( v × a × v × v ) set
start :: v

Pair and Quere showed that a RHL is characterized with an algebra calledbinoid [14]. A binoid B over Σ is a monoid with the following additional operation.
ˆ( ) : Σ × B → B
For example, the set of hedges itself constitutes a binoid, where the monoid
operation is the concatenation of two hedges and the additional operation above
is one that builds a h from a and h.
The following shows that a RHL can be characterized with a finite binoid.
Theorem 2. The following are equivalent for a set of hedges L ⊆ H(Σ).
1. L is regular.
2. There exist a finite binoid B, a homomorphism h : H(Σ) → B, a subset
B ⊆ B such that L = h−1 (B).
The binoid satisfying the theorem above can be obtained by considering a
monoid of relations over nonterminals. The additional operation ˆ( ) is deﬁned
as up rhg a b for a and b below.
up :: [( v , a) rhg, a, ( v × v ) set] ⇒ ( v × v ) set
up rhg a b ≡ {(x ,y) |x y. ∃ (z , f ) ∈ b. f ∈ prod1 rhg ∧ (x ,a,z ,y) ∈ prod2 rhg}

Although this binoid is used in the decision procedure for CFL-RHL inclusion, any binoid that satisﬁes the theorem is also suitable for the procedure.
Thus, we introduce the locale binoid below and describe the main part of theprocedure in the locale. Finally, we obtain our decision procedure by instantiating it to the binoid above.
locale binoid =fixes up :: [ a, b] ⇒ bfixes prod :: [ b, b] ⇒ b (infixr ˚ 70 )fixes unit :: bassumes assoc: (x ˚ y) ˚ z = x ˚ y ˚ zassumes unitl : unit ˚ x = x
assumes unitr : x ˚ unit = x

5.3

Monoid for CFL-RHL Inclusion

Let us assume that a RHL is characterized with a binoid B, a homomorphism◦, and a set B. The idea of the decision procedure is to interpret a set of
strings generated from each nonterminal by using elements of the B. However,∗each string φ such that X ⇒ φ is not necessarily balanced, but rather partiallybalanced. Therefore, we again use the factorization of φ:
φ = φ1 à1 φ2 à2 . . . φn àn ϕb́m ψm · · · b́2 ψ2 b́1 ψ1

where φi , ψi , and ϕ are all balanced. Then, we interpret φ with an element of(BΣ)∗ B(ΣB)∗ as follows:◦φ◦1 à1 φ◦2 à2 . . . φ◦n àn ϕ◦ b́m ψm· · · b́2 ψ2◦ b́1 ψ1◦

where ◦ is applied to balanced strings by considering them hedges. This is theideas of the decision procedure.
The elements of the set (BΣ)∗ B(ΣB)∗ ∪ { ⊥ } constitute a monoid, and it isrepresented by the following datatype:
datatype ( b, a) bmonoid = B ( b × a) listb ( b × a) list | Bot

where b and a are the types for B and Σ, respectively.
Then, by using the locale binoid we formalize the monoid operation with thefollowing function, where concat x y z is written as x yz with Isabelle’s mixﬁx
annotation.
function (in binoid )concat :: [( b, a) bmonoid , b, ( b, a) bmonoid ] ⇒ ( b, a) bmonoid whereB cs1 b1 [] Cx B B [] b2 ss2 = B cs1 (b1 ˚x ˚b2 ) ss2
B cs1 b1 [] Cx B B ((cb2 ,c2 )#cs2 ) b2 ss2 = B (cs1 @(b1 ˚x ˚cb2 ,c2 )#cs2 ) b2 ss2
B cs1 b1 ((sb1 ,s1 )#ss1 ) Cx B B [] b2 ss2 = B cs1 b1 (ss2 @(sb1 ˚x ˚b2 ,s1 )#ss1 )B cs1 b1 ((sb1 ,s)#ss1 ) Cx B B ((cb2 ,c)#cs2 ) b2 ss2 =(if s = c then B cs1 b1 ss1 C up s (sb1 ˚x ˚cb2 ) B B cs2 b2 ss2 else Bot)
Bot Cx B b = Botb Cx B Bot = Bot

The monoid operation is then λxy.x unity, where unit is the unit of the binoid.
The rest of the decision procedure is quite similar to the balancedness checking procedure and is formalized in the same manner.

6

Executing a Verified Decision Procedure

We generated executable code of the balancedness checking procedure from ourformalization with Isabelle’s code-generating facility [6]. The generated procedure was incorporated into the PHP string analyzer [8] by replacing the corresponding handwritten procedure. The analyzer checks whether a PHP program
always generates a well-formed XHTML document with the procedure. The revised analyzer was tested on real PHP programs. We describe issues that arose
during this experiment.
The formalization of the balancedness checking procedure we have describedis almost executable, but still requires some revisions to obtain executable code.
We have formalized decision procedures as abstractly as possible by using set
and s  t instead of concrete data structures. They are barriers to generatingcode and making it eﬃcient.
Isabelle has the library ExecutableSet, which allows us to generate code forﬁnite sets using lists. We generated executable code for sets with this library, butsome revisions of the formalization and an extension of the library were required.
We explain the issues with the procedure for computing the set of generating
nonterminals with a witness.
genv-onestep  cfg opr m ≡(λx . if x ∈ dom m then m xelse choose {opr w1 w2 | w1 w2 . ∃ y z . (x ,y,z ) ∈ prod2 cfg ∧ m y = Some w1 ∧m z = Some w2 })genv  cfg opr ≡ while (λx . genv-onestep  cfg opr x = x ) (genv-onestep  cfg opr )(λx . choose {v . (x ,v ) ∈ prod1 cfg})

The ﬁrst issue is the set comprehension in the formalization. The deﬁnition
includes the following set comprehension: {v . (x ,v ) ∈ prod1 cfg}. Although thisset is ﬁnite if prod1 is ﬁnite, this is not explicit in the expression and executablecode cannot be directly generated from it. To obtain executable code, we must
revise the formalization by using the following property.
{v . (x , v ) ∈ prod1 cfg} =S(x , v )∈prod1 cfg. if x = x  then {v } else {}The second problem concerns the choose function in the deﬁnition. The definition of choose uses SOME, i.e., Hilbert’s , for which code generation is notsupported by the library. Furthermore, it appears that the code of choose cannot
be implemented faithfully with lists. If choose is implemented with choosel over alist, then choosel xs = choosel ys should hold for lists xs and ys representing thesame set. This property cannot be satisﬁed without any additional structure on
its elements. To overcome this issue, we revised our formalization so that choose
is used only for sets over types that are instances of linorder. The deﬁnition ofchoose was also revised so that it chooses the minimum element in a set.
We could generate code with these revisions. However, to obtain code withreasonable eﬃciency, more revisions were required. In our experiments, we represented nonterminals with type int in the ML side. Because the set of elements
of int is ﬁnite and linearly ordered, the type satisﬁes the required conditions to
use it as the type of nonterminals. However, the following two issues arise.
We veriﬁed the correctness of our decision procedures under the assumptionthat all nonterminals are generating and reachable. This simpliﬁed our veriﬁcation, but it is not reasonable to assume it when we represent nonterminals
with type int in ML. Thus, we revised our formalization so that the procedures
assume that only the nonterminals used in a CFG are generating and reachable.
Finally, the evaluation strategy of functional programming languages becomes an issue for eﬃcient execution: they do not evaluate the expression inside
a lambda abstraction. In the decision procedure, type s  t is used to represent ﬁnite maps. The type is actually a function type to option type. Then,
all the computation related to a map is delayed until the map is applied to anargument. That caused an exponential blowup of execution time. To avoid thisblowup, we insert the function reduce-fun with the following type into the places
where evaluation inside a lambda abstraction is desirable.

reduce-fun :: [ a::{finite,linorder } set, a ⇒ b] ⇒ a ⇒ b

An expression reduce-fun f s forces the evaluation of f for the values in the sets and reconstructs the function. For the deﬁnition of the function, please referto the proof script.
By applying these revisions, we could run the analyzer with the code generated by Isabelle for real PHP programs. We tested it on two PHP programs, forwhich the analyzer generated CFGs with 170 and 70 production rules. With the
handwritten code, the balancedness can be checked very quickly, taking 0.016
and 0.003 seconds for the two programs. On the other hand, the generated code
was quite slow, taking 32.6 and 16.7 seconds. We checked execution times foreach part of the procedure and found that the depth-ﬁrst search is eﬃcient, but
the ﬁxed-point computations used in genv  and compute-langs  are very slow.
We think that this is because the formalization of depth-ﬁrst search is very close
to a standard implementation, but the formalization of the ﬁxed-point computation is rather abstract. It will be necessary to revise its formalization and adopt
a more eﬃcient data structure to represent ﬁnite maps to obtain more eﬃcient
code.

7

Related Work

Our formalization is strongly inﬂuenced by Nipkow’s formalization of automata,which formalizes automata and regular expressions, and veriﬁes a lexical analyzer
obtained from a regular expression [12]. There have been several other attempts
to formalize the theory of formal languages in a proof assistant. Courant andFilliâtre formalized regular and context-free languages in Coq [3]. The formalization includes some standard theory of context-free languages such as transformation between a context-free grammar and a pushdown automaton. Rival
and Goubault-Larrecq formalized tree automata in Coq [16] and executed someprocedures on tree automata in Coq.
We have described several issues in obtaining an (eﬃcient) executable balancedness checking procedure in Section 6. The importance of obtaining eﬃcient
executable code from an elegant formalization is recognized in the context of
ACL2. Greve et al. reviewed issues there and described the features in ACL2 tosupport it [5]. This will be good guide to obtain really eﬃcient executable codefor our decision procedures.

8

Conclusion

We have veriﬁed three precision procedures on context-free grammars. The formalization and veriﬁcation of the procedures went smoothly and took me about
non-intensive two months. On the other hand, the revisions to generate executable code for the balancedness checking procedure required more time thanwe expected.

We plan to generate code for the other two procedures. Although code will
be generated in the same manner as the balancedness checking procedure, we
expect a more severe problem with eﬃciency. It is because the relations overstates or nonterminals used there will become too large if int are used in theML side.

References
1. Jean Berstel. Transductions and Context-Free Languages. Teubner Studienbucher,1979.
2. Jean Berstel and Luc Boasson. Formal properties of XML grammars and languages.
Acta Informatica, 38(9):649–671, 2002.
3. Judicael Courant and Jean-Christophe Filliâtre. Beginning of formal language
theory, 1993. http://coq.inria.fr/contribs-eng.html.
4. Samuel Eilenberg. Automata, Languages, and Machines, chapter 3. Academic
Press, 1974.
5. David A. Greve, Matt Kaufmann, et al. Eﬃcient execution in an automated reasoning environment. Journal of Functional Programming, 2007. to appear.
6. Florian Haftmann. Code generation from Isabelle/HOL theories, 2007. available
in the Isabelle distribution.
7. Alexander Krauss. Partial recursive functions in higher-order logic. In AutomatedReasoning, Third International Joint Conference, volume 4130 of LNCS, pages
589–603, 2006.
8. Yasuhiko Minamide. Static approximation of dynamically generated Web pages. In
Proceedings of the 14th International World Wide Web Conference, pages 432–441.
ACM Press, 2005.
9. Yasuhiko Minamide and Akihiko Tozawa. XML validation for context-free grammars. In Proc. of The Fourth ASIAN Symposium on Programming Languages andSystems, volume 4279 of LNCS, pages 357–373, 2006.
10. J Strother Moore. An exercise in graph theory. In Matt Kaufmann, Panagiotis
Manolios, and J Strother Moore, editors, Computer-Aided Reasoning: ACL2 Case
Studies, chapter 5, pages 41–74. Kluwer Academic Publishers, 2000.
11. Makoto Murata. Hedge automata: a formal model for XML schemata, 1999.
http://www.xml.gr.jp/relax/hedge nice.html.
12. Tobias Nipkow. Veriﬁed lexical analysis. In Theorem Proving in Higher Order
Logics, volume 1479 of LNCS, pages 1–15, 1998.
13. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof
Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
14. C. Pair and A. Quere. Déﬁnition et étude des bilangages réguliers. Information
and Control, 13(6):565–593, 1968.
15. Thomas Reps. Program analysis via graph reachability. Information and Software
Technology, 40(11–12):701–726, 2000.
16. Xavier Rival and Jean Goubault-Larrecq. Experiments with ﬁnite tree automata
in Coq. In Proc. 14th Int. Conf. Theorem Proving in Higher Order Logics(TPHOL’01), volume 2152 of LNCS, pages 362–377, 2001.
17. Akihiko Tozawa and Yasuhiko Minamide. Complexity results on balanced contextfree languages. In Proc. of Tenth International Conference on Foundations ofSoftware Science and Computation Structures, volume 4423 of LNCS, pages 346–
360, 2007.