Hacia la prueba de corrección de clases

Abstract

La actividad de desarrollar programas orientados a objetos, los cuales involucran referencias a memoria, pueden introducir errores difíciles de identificar con el uso de un razonamiento operacional. Esto da lugar a la necesidad de contar con un marco teórico para la prueba de corrección de clases. A partir de esta motivación y basándonos en la idea propuesta por B. Meyer en [Meyer 03a], trabajamos en el desarrollo de una semántica formal para probar, matemáticamente, que clases equipadas con contratos satisfacen los mismos.

The activity of object oriented program development, which may involve references variables, is prone to errors which are hard to find by operational reasoning. Hence the need for a theoretical framework for proving class correctness. Given this motivation and based on ideas proposed by B. Meyer in [Meyer 03a] we develop a formal semantics for mathematically proving that contract equipped classes satisfy their specifications.