El objetivo de este libro es argumentar los elementos de juicio de los programadores y afinar su intuición a fin y efecto de que puedan producir programas más correctos, por medio del entrenamiento en la programación y verificación de mecanismos de computación sencillos, como los autómatas finitos y con pila y los programas en un lenguaje de programación muy simple, pero suficiente para simular cualquier otro lenguaje. Este libro cubre las nociones básicas de la teoría de autómatas y lenguajes formales, como los autómatas finitos, las expresiones regulares, las gramáticas incontextuales, los autómatas con pila, los programas deterministas e indeterministas y la indecibilidad. Los temas y el nivel son similares a los de otros libros orientados a introducir estas materias en una asignatura de ingeniería informática. Ahora bien, este libro no es un libro típico de autómatas y lenguajes formales, por tres motivos: el énfasis en verificación, la sintaxis estructurada para programas y autómatas con pila y aplicación del paradigma indeterminista en los programas.