El temprano desarrollo de la teoría de Lenguajes Formales y Autómatas dentro de las Ciencias de Computación hizo que su cuerpo de conocimientos y algoritmos se conformara antes de que se contara con métodos de diseño que garanticen corrección, que permitan derivar algoritmos a partir de especificaciones o verificarlos usando técnicas especiales para ello. Como consecuencia el enfoque usual de la bibliografía consiste en presentar los algoritmos o autómatas y luego demostrar que satisfacen el problema a resolver. En esta línea de trabajo se pretende reformular la presentación de los resultados usando métodos de diseño que garanticen la corrección. Un resultado de ésta línea ya obtenido es un método para la construcción de autómatas finitos a partir del predicado que define su conjunto de aceptación. Dicho método garantiza la corrección de los autómatas construidos, que ha sido usado tanto para rehacer todas las construcciones de autómatas finitos requeridos en el cuerpo de la teoría de Lenguajes Formales, incluyendo el teorema fundamental del análisis LR como para probar su aplicación a la construcción de diversos casos de estudio con objetivos prácticos.