Earley's parsing algorithm is an O(n3) algorithm for parsing according to any context-

free grammar. Its theoretical importance stems from the fact that it was one of the

first algorithms to achieve this time bound, but it has also seen success in compiler-

compilers, theorem provers and natural language processing. It has an elegant struc-

ture, and its time complexity on restricted classes of grammars is often as good as

specialized algorithms. Grammars with  -productions, however, require special con-

sideration, and have historically lead to inefficient and inelegant implementations.

In this thesis, we develop the algorithm from specification using the B-Method.

Through refinement steps, we arrive at a list-processing formulation, in which the

problems with  epsilon-productions emerge and can be understood. The development high-

lights the essential properties of the algorithm, and has also lead to the discovery of

an implementation optimization. We end by giving a concept-test of the algorithm

as a literate Pascal program.