Cálculo de Precondiciones más Débiles

Resumen

El cálculo comenzó a desarrollarse en el siglo XVII con la intención de conseguir técnicas estándar para resolver problemas referentes a derivadas, integrales y ecuaciones diferenciales. Gracias al desarrollo de esta ciencia y la estandarización de las técnicas de cálculo integral, hoy en dı́a es posible que un estudiante de primer año de universidad pueda aprender a resolver una cantidad enorme de integrales en poco tiempo y aunque el estudiante tenga la sensación de que esta usando el sentido común para hacer dichos cálculos, realmente puede hacerlo porque esta siguiendo un algoritmo de resolución, muy complejo, pero algoritmo en fin. Este algoritmo es el que hace posible que hoy en dı́a, aplicaciones como Mapple o Mathematica puedan resolver simbólicamente integrales y ecuaciones diferenciales. Es decir, el mayor porcentaje del crédito por el éxito de estas aplicaciones, se debe a la existencia de los algoritmos de resolución del cálculo, que han sido desarrollados durante cuatro siglos. Por otro lado en el mundo de la demostración formal de programas, también existen software como en [1][2][3] que intentan hacer cómputos simbólicos para la corrección de programas. Estas aplicaciones para la corrección de programas, no usan un algoritmo de cuatro siglo de desarrollo que estandarizan técnicas del cálculo de los invariantes y obligaciones de prueba, por lo que tienen una desventaja natural con respecto a las aplicaciones de resolución simbólica para el cálculo integral o diferencial.

Por lo argumentado anteriormente se propone que para lograr un avance significativo en las aplicaciones para la corrección de programas, es conveniente crear ahora, en la ciencia de la matemática, un cálculo (al igual como en su tiempo se creó el cálculo integral), para estandarizar los métodos que permiten computar invariantes, obligaciones de prueba y precondiciones más débiles. Este articulo muestra algunos teoremas que tienen la intención de dar un pequeño paso en el desarrollo de este cálculo pero para computar precondiciones más débiles.