En un paper reciente, Barthe et. al. presentan una lógica de Hoare para razonar sobre la especificación funcional de programas probabilísticos, dada en forma de pre-y pos-condiciones. Para automatizar el razonamiento sobre la especificación de programas usando dicha lógica, presentan además un operador de pre-condición más débil (wp : Prog —> Pos —> Pre) que opera propagando la pos-condición de los programas "hacia atrás" hasta entregar la pre-condición más débil que establece dicha pos-condición. El objetivo general de esta tesis es desarrollar un operador de pos-condición más fuerte (sp : Prog —> Pre —> Pos) que opera de manera dual: dada la pre-condición del programa, la propaga "hacia adelante" hasta derivar los pos-condición más fuerte establecida por dicha pre-condición. Se busca validar el operador sp propuesto en términos prácticos (aplicándolo a algún caso de estudio) y teórico (prueba de soundness y precisión con respecto a la lógica).