Finite automata and various extensions of them, such as transducers,
are used in areas as
diverse as compilers, spelling checking, natural language grammar checking,
communication
protocol design, digital circuit simulation, digital flight control,
speech recognition and synthesis, genetic sequencing, and Java program
verification. Unfortunately, as the number of
applications has grown, so has the variety of implementations and
implementation techniques.
Typically, programmers will be confused enough to resort to their
text books for the most
elementary algorithms. Recently, advances have been made in
taxonomizing algorithms for
constructing and minimizing automata and in evaluating various
implementation strategies
Watson 1995. Armed with this, a number of general-purpose toolkits
have been developed
at universities and companies. One of these, FIRE Lite, was developed
at the Eindhoven
University of Technology, while its commercial successor, FIRE
Engine II, has been developed
at Ribbit Software Systems Inc. Both of these toolkits provide
implementations of all of the
known algorithms for constructing automata from regular expressions,
and all of the known
algorithms for minimizing deterministic finite automata. While the two
toolkits have a great
deal in common, we will concentrate on the structure and use of
the noncommercial FIRE
Lite. The prototype version of FIRE Lite was designed with compilers
in mind. More recently, computation linguists and communications protocol
designers have become interested
in using the toolkit. This has led to the development of a much more
general interface to
FIRE Lite, including the support of both Mealy and Moore regular
transducers. While such
a toolkit may appear extremely complex, there are only a few choices
to be made. We also
consider a ‘recipe’ for making good use of the toolkits.
Lastly, we consider the future of FIRE
Lite. While FIRE Engine II has obvious commercial value, we are
committed to maintaining
a version which is freely available for academic use.
Java Program Verification Challenges
