% $Id: BNF.lsl,v 1.3 2000/01/17 21:33:40 connolly Exp $
BNF: trait
includes
Grammar,
RegExp
introduces
__ ..= __: Symbol, Exp ® FiniteSet[Rule]
% ..= is poor-man's ::=
sym: Exp ® Symbol
% an arbitrary symbol corresponding to a regexp
symbolsIn: Exp ® FiniteSet[Symbol]
% the set of symbols mentioned in an expression
asserts
" A, B: Symbol, e, f: Exp
A ..= [B] = {A Þ {B}};
A ..= (e \U f) = (A ..= e) \U (A ..= f);
A ..= (e || f) = {A Þ {sym(e)} || {sym(f)}}
\U (sym(e) ..= e)
\U (sym(f) ..= f);
A ..= (e \*) = {A Þ empty} \U { A Þ ({A} || {sym(e)}) };
sym([B]) = B;
symbolsIn([A]) = {A};
symbolsIn(e \U f) = symbolsIn(e) \U symbolsIn(f);
symbolsIn(e || f) = symbolsIn(e) \U symbolsIn(f);
symbolsIn(e\*) = symbolsIn(e);
implies
forall A: Symbol, e: Exp, terminals: FiniteSet[Symbol]
A \notin terminals Ù symbolsIn(e) \subseteq terminals Þ
L([A, terminals, A ..= e]) = L(e);
[Index]
[source]
HTML generated using lsl2html.