PROOF OF CORRECTNESS OF A DIRECT CONSTRUCTION OF DFA FROM REGULAR EXPRESSION

We present a proof of correctness of an algorithm for directly constru cting a deterministic finite automaton (DFA) from a regular expression . We do this in a functional framework by introducing a structure call ed dot annotated regular expression (dare). A dare acts as an implicit representation of a state in a DFA. State transitions in a DFA corres pond to dot movements in a dare. We investigate and identify certain a lgebraic properties of dare's which are then used to prove the correct ness of the algorithm. The proof is algebraic and presented in the sam e framework as that of the algorithm itself.