Menu Content/Inhalt
Home
Cálculo de Refinamiento

Docente: Javier Blanco

Introducción:

El cálculo de refinamiento es un framework para razonar sobre la corrección y refinamiento de programas. La aplicación principal es la derivación de programas imperativos tradicionales a través de una metodología paso a paso. Cada paso de refinamiento debe preservar la corrección de la versión previa del programa, garantizada por reglas que vinculan aserciones de especificación y una implementación.

El cálculo de refinamiento se funda en la teoría de reticulados y lógica de alto orden, junto a una teoría simple sobre variables de programas.

La intención de este curso es poner énfasis en las bases matemáticas y lógicas del refinamiento de programas, y no tanto en como construir programas en la práctica, aunque se presentarán diversos ejemplos y casos de estudio.

Un conocimiento profundo de los fundamentos de este cálculo es necesario para poder extender la aplicación del mismo a otros dominios, por ejemplo, los programas que manejan dinámicamente la memoria, o los programas concurrentes.

Programa:

  1. Introducción: contratos; aserciones; especificaciones;   corrección; refinamiento de programas.
  2. Fundamentos matemáticos: conjuntos parcialmente ordenados;   reticulados; categorías; lógica de alto orden; funciones.
  3. Transformadores de estado: atributos y variables de programa;   programas straight-line; procedimientos; bloques y parámetros;   cálculo de predicados.
  4. Transformadores de predicados: transformadores básicos;  dualidad; contratos; precondiciones y guardas; transformadores monótonos;   transformadores asociados a sentencias.
  5. No determinismo: semántica; refinamiento de la elección no   determinística. No determinismo angélico y demónico.
  6. Refinamiento: corrección; refinamiento paso a paso; leyes de   refinamiento; procedimientos; contextos; datos.
  7. Recursión: conjuntos bien formados; punto fijo; reglas de introducción y eliminación.
  8. Iteración: propiedades; correccion; loops.
  9. Tipo de datos complejos: manipulación de arreglos; manipulación de punteros.

Bibliografía:

  • R.J. Back and J. von Wright. Refinement Calculus. A Systematic Introduction. Graduate texts in computer science, Springer Verlag, 1998.
  • R.J. Back, X. Fan, and V. Preoteasa. Reasoning about pointers in refinement calculus. In 10th Asia Pacific Software Engineering Conference (APSEC'03), 2003.
  • R.C. Backhouse. Program Construction and Verication. Prentice Hall International, 1986.
  • M.J. Butler, J. Grundy, T. Langbacka, R. Ruksenas, and J. von Wright. The refinement calculator: proof support for program refinement. In L. Groves and S. Reeves, editors, Formal Methods Pacific'97, Series in Discrete Mathematics and Theoretical Computer Science, Springer, 1997.
  • B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge mathematical textbooks. Cambridge University Press, 1990.
  • E. W. Dijkstra. A Discipline of Programming. Series in Automatic Computation, Prentice-Hall International, 1976.
  • E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science, Springer Verlag, 1990.
  • D. Gries and F. Schneider. A Logical Introduction to Discrete Mathematics. Springer Verlag, 1993.
  • C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the Association for Computing Machinery, 1969.
  • C.A.R. Hoare. Proofs of correctness of data representation. Acta Informatica, 1972.
  • C.C. Morgan. Programming from specifications. Prentice Hall, 1990.
  • G. Nelson. A generalization of Dijkstra's calculus. ACM Transactions on Programming Languages and Systems, 1989.
  • J.L.A. van de Snepscheut. What computing is all about. Springer Verlag, 1994. 
 
< Anterior
Content Management System: Joomla!
Template based on an original designed by www.madeyourweb.com