This work is concerned with the advantages of using methods for correct software construction in the teaching of Formal Languages Theory. That methods are usually taught in courses of programming and algorithms construction, but in Formal language theory courses the practice traditionally used and also the style followed by the bibliography, consist in: first to present the algorithms and then to construct their correctness proof. As a novel application of the first methodology, we present a method, developed by the authors, to construct finite automata from the characteristic predicate of its accepting set. If this method is followed, the correctness of the obtained finite automata is guaranteed. The method consists of obtaining a family of first order predicates and a set of states from the original predicate, in which each predicate is an invariant of a state. Next, from this predicate's family, the transition function and the initial state are defined. This paper also shows its application to give a constructive proof of several classic Formal Language and Automata theory results, including the LR grammars fundamental theorem. Some samples of the method application to practical cases of automata design are also included.

En éste trabajo se analizan las ventajas de utilizar en la enseñanza de la Teoría de Lenguajes Formales los métodos de construcción de software correcto habitualmente usados en las asignaturas de construcción de algoritmos y programación, en lugar de la práctica habitualmente usada y seguida en la bibliografía, de presentar los algoritmos y luego dar para ellos una demostración de su corrección. Como una aplicación novedosa de ésta metodología se presenta el uso de 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, desarrollado por los autores, garantiza la corrección de los autómatas construidos. El método consiste en obtener a partir del predicado original, una familia de predicados y un conjunto de estados de los cuales los primeros son invariantes. A partir de ésta familia se define la función de transición y el estado inicial. Se incluye la aplicación del método a varias construcciones clásicas de la teoría de lenguajes y autómatas, entre ellas, el autómata que demuestra la propiedad fundamental de las gramáticas LR y a algunos ejemplos prácticos de construcción de Autómatas, tema que generalmente también es abordado en la misma asignatura.