Cliff B. Jones. Formal development of correct algorithms: An example based on earley's recogniser. In Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972. pages 150-169, ACM, 1972. [doi]
Abstract is missing.