We start a series of four introductory articles regarding the axiomatic verification of programs, in the context of imperative input/output programs. In this article, we introduce the axiomatic verification method for deterministic sequential programs, and we show some application examples. Although program verification is presented as an a posteriori activity (given a program and a specification, verify that the program satisfies the specification), the main idea sustained in the article, and in the entire series, is to take into account the method axioms and rules both for programming as well as verifying, in order to obtain correct programs by construction. With this perspective, a systematic development of a program based on the studied axiomatics is presented at the end.  Iniciamos una serie de cuatro artículos introductorios sobre la verificación axiomática de programas, en el marco de los programas imperativos de entrada/salida. En este artículo introducimos el método axiomático de verificación para los programas secuenciales determinísticos, y desarrollamos ejemplos de aplicación. Si bien la verificación de programas se expone como una actividad a posteriori (dados un programa y una especificación, verificar que el programa satisface la especificación), la idea que se sostiene en el artículo, y en toda la serie, es tener en cuenta los axiomas y reglas del método para programar al mismo tiempo que verificar, de modo tal de obtener programas correctos por construcción. Con esta perspectiva, al final se ejemplifica un desarrollo sistemático de programa basado en la axiomática presentada.