Enseñando métodos formales con Coq
DOI:
https://doi.org/10.24215/18509959.0.10%20p.Palabras clave:
Enseñanza de la Programación, Métodos Formales, Teoría de Tipos, Coq, Especificación y Verificación de CorrecciónResumen
En este trabajo presentamos una propuesta para apoyar la enseñanza de métodos formales en una currícula de grado, y postgrado, usando el asistente de pruebas Coq y conceptos del área de Teoría de Tipos. Proponemos un taller de especificación, construcción y verificación de sistemas en los paradigmas de programación funcional e imperativo, que también abarca el análisis de sistemas críticos: sistemas reactivos y de tiempo real. Describimos algunas experiencias en el desarrollo del taller y planteamos cambios y extensiones.
Descargas
Los datos de descargas todavía no están disponibles.
Citas
[1] B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, H. Laulhère, C. Muñoz, Ch. Murthy, C. Parent-Vigouroux, P. Loiseleur, Ch. Paulin-Mohring, A. Saïbi, and B. Werner. “The Coq Proof Assistant. Reference Manual, Versión 7.4”. INRIA, 2003.
[2] G. Barthe, J. Cederquist, and S. Tarento. "A MachineChecked Formalization of the Generic Model and the Random Oracle Model". In D. Basin and M. Rusinowitch, editors, Proceedings of IJCAR'04, volume 3097 of Lecture Notes in Computer Science, pages 385-399, Cork, Ireland, 2004.
[3] G. Barthe and G. Dufay. "A Tool-Assisted Framework for Certified Bytecode Verification". In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages 99-113, Barcelona, Spain, 2004.
[4] G. Barthe and S. Stratulat. "Validation of the JavaCard Platform with Implicit Induction Techniques". In R. Nieuwenhuis, editor, Proceedings of RTA'03, LNCS, 2003.
[5] Y. Bertot and P. Castéran. “Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions”. Series: Texts in Theoretical Computer Science. An EATCS Series, ISBN: 3-540-20854-2, 2004.
[6] C. Breunesse, N. Cataño, M. Huisman, and B. Jacobs. "Formal methods for smart cards: an experience report". Science of Computer Programming, 55(1-3):53-80, 2005.
[7] T. Coquand and G. Huet. “Constructions: A higher order proof system for mechanizing mathematics”. In EUROCALL´85, LNCS 203, Linz, 1985, SpringerVerlag, 1985.
[8] T. Coquand and G. Huet. “The calculus of constructions”. Information and Computation, 76(2/3), 1988.
[9] T. Coquand. “Metamathematical investigations of a calculus of constructions”. INRIA and Cambridge, University, 1986.
[10] T. Coquand. “Infinite objects in type theory”. In H. Barendregt and T. Nipkow, editors, Workshop on Types for Proofs and Programs, number 806 in LNCS, pages 62-78. Springer-Verlag, 1993.
[11] E. Dijkstra, “A Discipline of Programming”. PrenticeHall, Englewood Cliffs, NJ, 1976.
[12] J.C. Filliatre. “Proof of imperative programs”. In Chapter 18 of The Coq Proof Assistant Reference Manual, Version 7.0, 2001.
[13] A. Ferreira, C. Luna y R. Medel. “Manual-Guía de Aprendizaje de Programación Avanzada”, publicado por la Editorial de la Fundación de la Universidad Nacional de Río Cuarto –miembro de la Red de Editoriales Universitarias Argentinas– en Marzo de 1998.
[14] E. Giménez. “An application of Co-inductive Types in Coq: Verification of the Alternating Bit Protocol”. In BRA Workshop on Types for Proofs and Programs (TYPES’95), LNCS 1158, pages 135-152, SpringerVerlag, 1995.
[15] E. Giménez. A Calculus of Infinite Constructions and its application to the verification of communicating systems. PhD thesis, Ecole Normale Supérieure de Lyon, 1996, Unité de Recherche Associée au CNRS No. 1398, 1996.
[16] E. Gimenez and P. Casteran. A Tutorial on [Co- ]Inductive Types in Coq, Technical Report, INRIA (accesible en http://coq.inria.fr/), 2005.
[17] E. Giménez. “Two Approaches to the Verification of Concurrent Programs in Coq”, 1999.
[18] M. Gordon. Introduction to HOL: a theorem proving environment based for higher order logic. Cambridge University, Press, 1993.
[19] D. Gries. The science of programming, Springer-Verlag New York Inc., 1981.
[20] G. Huet, G. Kahn and C. Paulin-Mohring. The Coq Proof Assistant: A Tutorial (accesible desde el sitio web http://coq.inria.fr/), 2004.
[21] W. Howard. “The formulae-as-types notion of construction”. In J. Seldin and J. Hindley, editors, To H. Curry: Essays on combinatory logic, lambda calculus and formalism. Academic Press, 1980. A reprint of an unpublished manuscript from 1969.
[22] C. Luna. “Verificación de Sistemas de Tiempo Real en Teoría de Tipos. Un Caso de Estudio: The RailRoad Crossing example in Coq”. En proceedings de la Conferencia Latinoamericana de Informática: CLEI'2002, Montevideo, Noviembre de 2002.
[23] C. Luna. "Especificación y análisis de sistemas de tiempo real en teoría de tipos". Vol VIII No. 1, JulioSetiembre de 2004, Revista Iberoamericana Computación y Sistemas, ISSN 1405-5546. Centro de Investigación en Computación, Instituto Politécnico Nacional, México, D.F., 2004.
[24] C. Luna. "Enseñando Métodos Formales con COQ". I Congreso de Tecnología en Educación y Educación en Tecnología (TE&ET’06), La Plata, Argentina, Agosto de 2006.
[25] C. Luna, P. Martellotto, M. M. Novaira. “Teoría de Tipos y Coq en la Enseñanza de Programación Funcional e Imperativa. Taller de Construcción Formal de Programas”. En proceedings de la Conferencia Latinoamericana de Informática: CLEI'2002 – CIESC’2002. Montevideo, Uruguay, 2002.
[26] Z. Luo and R. Pollack. “Lego proof development system: User’s manual”. Technical Report ECS-LFCS92-211, LFCS, 1992.
[27] L. Magnusson. The implementation of ALF – a proof editor based on Matin Löf’s Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Göteborg, 1994.
[28] D. Mandrioli, Carlo Ghezzi, and Mehdi Jazayeri. Fundamentals of Software Engineering. Prentice Hall, 1991.
[29] L. Paulson. “Co-induction and Co-recursion in Higherorder Logic”. Technical Report 304, Computer Laboratory, University of Cambridge, 1993.
[30] C. Paulin-Mohring. “Extracting Fω’s programs from proofs in the calculus of constructions”. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, ACM, 1989.
[31] C. Paulin-Mohring. Extraction de programmes dans le calcul des constructions. Thèse de doctorat, Université de Paris VII, 1989.
[32] C. Paulin-Mohring. “Inductive definitions in the system Coq – rules and properties”. In M. Bezem and J. Groote, editors, Proceeedings of the conference Typed Lambda Calculi and Aplications, LNCS 664, 1993.
[33] P. Weis et X. Leroy. “Le Langage CAML”. Second edition, Dunod, Paris, 1999. First edition, InterEditions, Paris, 1993.
[34] S. Zanella Béguelin, G. Betarte, and C. Luna. “A formal specification of the MIDP 2.0 security model”. In Proc. 4th International Workshop on Formal Aspects in Security and Trust, FAST 2006, Hamilton, Canada, August 26-27 2006, Lectures Notes in Computer Science. Springer 2006. To appear.
[2] G. Barthe, J. Cederquist, and S. Tarento. "A MachineChecked Formalization of the Generic Model and the Random Oracle Model". In D. Basin and M. Rusinowitch, editors, Proceedings of IJCAR'04, volume 3097 of Lecture Notes in Computer Science, pages 385-399, Cork, Ireland, 2004.
[3] G. Barthe and G. Dufay. "A Tool-Assisted Framework for Certified Bytecode Verification". In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages 99-113, Barcelona, Spain, 2004.
[4] G. Barthe and S. Stratulat. "Validation of the JavaCard Platform with Implicit Induction Techniques". In R. Nieuwenhuis, editor, Proceedings of RTA'03, LNCS, 2003.
[5] Y. Bertot and P. Castéran. “Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions”. Series: Texts in Theoretical Computer Science. An EATCS Series, ISBN: 3-540-20854-2, 2004.
[6] C. Breunesse, N. Cataño, M. Huisman, and B. Jacobs. "Formal methods for smart cards: an experience report". Science of Computer Programming, 55(1-3):53-80, 2005.
[7] T. Coquand and G. Huet. “Constructions: A higher order proof system for mechanizing mathematics”. In EUROCALL´85, LNCS 203, Linz, 1985, SpringerVerlag, 1985.
[8] T. Coquand and G. Huet. “The calculus of constructions”. Information and Computation, 76(2/3), 1988.
[9] T. Coquand. “Metamathematical investigations of a calculus of constructions”. INRIA and Cambridge, University, 1986.
[10] T. Coquand. “Infinite objects in type theory”. In H. Barendregt and T. Nipkow, editors, Workshop on Types for Proofs and Programs, number 806 in LNCS, pages 62-78. Springer-Verlag, 1993.
[11] E. Dijkstra, “A Discipline of Programming”. PrenticeHall, Englewood Cliffs, NJ, 1976.
[12] J.C. Filliatre. “Proof of imperative programs”. In Chapter 18 of The Coq Proof Assistant Reference Manual, Version 7.0, 2001.
[13] A. Ferreira, C. Luna y R. Medel. “Manual-Guía de Aprendizaje de Programación Avanzada”, publicado por la Editorial de la Fundación de la Universidad Nacional de Río Cuarto –miembro de la Red de Editoriales Universitarias Argentinas– en Marzo de 1998.
[14] E. Giménez. “An application of Co-inductive Types in Coq: Verification of the Alternating Bit Protocol”. In BRA Workshop on Types for Proofs and Programs (TYPES’95), LNCS 1158, pages 135-152, SpringerVerlag, 1995.
[15] E. Giménez. A Calculus of Infinite Constructions and its application to the verification of communicating systems. PhD thesis, Ecole Normale Supérieure de Lyon, 1996, Unité de Recherche Associée au CNRS No. 1398, 1996.
[16] E. Gimenez and P. Casteran. A Tutorial on [Co- ]Inductive Types in Coq, Technical Report, INRIA (accesible en http://coq.inria.fr/), 2005.
[17] E. Giménez. “Two Approaches to the Verification of Concurrent Programs in Coq”, 1999.
[18] M. Gordon. Introduction to HOL: a theorem proving environment based for higher order logic. Cambridge University, Press, 1993.
[19] D. Gries. The science of programming, Springer-Verlag New York Inc., 1981.
[20] G. Huet, G. Kahn and C. Paulin-Mohring. The Coq Proof Assistant: A Tutorial (accesible desde el sitio web http://coq.inria.fr/), 2004.
[21] W. Howard. “The formulae-as-types notion of construction”. In J. Seldin and J. Hindley, editors, To H. Curry: Essays on combinatory logic, lambda calculus and formalism. Academic Press, 1980. A reprint of an unpublished manuscript from 1969.
[22] C. Luna. “Verificación de Sistemas de Tiempo Real en Teoría de Tipos. Un Caso de Estudio: The RailRoad Crossing example in Coq”. En proceedings de la Conferencia Latinoamericana de Informática: CLEI'2002, Montevideo, Noviembre de 2002.
[23] C. Luna. "Especificación y análisis de sistemas de tiempo real en teoría de tipos". Vol VIII No. 1, JulioSetiembre de 2004, Revista Iberoamericana Computación y Sistemas, ISSN 1405-5546. Centro de Investigación en Computación, Instituto Politécnico Nacional, México, D.F., 2004.
[24] C. Luna. "Enseñando Métodos Formales con COQ". I Congreso de Tecnología en Educación y Educación en Tecnología (TE&ET’06), La Plata, Argentina, Agosto de 2006.
[25] C. Luna, P. Martellotto, M. M. Novaira. “Teoría de Tipos y Coq en la Enseñanza de Programación Funcional e Imperativa. Taller de Construcción Formal de Programas”. En proceedings de la Conferencia Latinoamericana de Informática: CLEI'2002 – CIESC’2002. Montevideo, Uruguay, 2002.
[26] Z. Luo and R. Pollack. “Lego proof development system: User’s manual”. Technical Report ECS-LFCS92-211, LFCS, 1992.
[27] L. Magnusson. The implementation of ALF – a proof editor based on Matin Löf’s Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Göteborg, 1994.
[28] D. Mandrioli, Carlo Ghezzi, and Mehdi Jazayeri. Fundamentals of Software Engineering. Prentice Hall, 1991.
[29] L. Paulson. “Co-induction and Co-recursion in Higherorder Logic”. Technical Report 304, Computer Laboratory, University of Cambridge, 1993.
[30] C. Paulin-Mohring. “Extracting Fω’s programs from proofs in the calculus of constructions”. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, ACM, 1989.
[31] C. Paulin-Mohring. Extraction de programmes dans le calcul des constructions. Thèse de doctorat, Université de Paris VII, 1989.
[32] C. Paulin-Mohring. “Inductive definitions in the system Coq – rules and properties”. In M. Bezem and J. Groote, editors, Proceeedings of the conference Typed Lambda Calculi and Aplications, LNCS 664, 1993.
[33] P. Weis et X. Leroy. “Le Langage CAML”. Second edition, Dunod, Paris, 1999. First edition, InterEditions, Paris, 1993.
[34] S. Zanella Béguelin, G. Betarte, and C. Luna. “A formal specification of the MIDP 2.0 security model”. In Proc. 4th International Workshop on Formal Aspects in Security and Trust, FAST 2006, Hamilton, Canada, August 26-27 2006, Lectures Notes in Computer Science. Springer 2006. To appear.
Descargas
Publicado
2006-12-01
Cómo citar
[1]
C. D. Luna, «Enseñando métodos formales con Coq», TEyET, n.º 1, p. 10 p., dic. 2006.
Número
Sección
Artículos originales
Licencia
Derechos de autor y licencias
Los artículos aceptados para publicación tendrán la licencia de Creative Commons BY-NC. Los autores deben firmar un acuerdo de distribución no exclusiva después de la aceptación del artículo.
