Finite Sets: A Case Study on Formal Program Development in the Extended ML Framework
Resumo
Estudamos o desenvolvimento formal de programas funcionais, usando especificações algébricas, em Extended ML. Apresentamos um estudo de caso em especificação modular e refinamento de operações de conjuntos (finitos) usando a linguagem de especificação/programação Extended ML. Nosso principal objetivo é apresentar a linguagem de módulos e a metodologia de desenvolvimento Extended ML, suas aplicações em problemas práticos e sua adequação para o desenvolvimento formal de programas (modulares) em Standard ML.
Referências
R. M. Burstall, D. B. MacQueen, and D. T. Sannella. Hope: an experimental applicative language. Technical Report CSR-62-80, Department of Computer Science, University of Edinburgh, Edinburgh, EH9 3JZ, Scotland, 1980.
Cláudia J. A. da Silva and Fabio Q. B. da Silva. Conjuntos finitos: Um estudo de caso em desenvolvimento formal de programas em extended ml. Revista Brasileira de Computação, 1993. To appear.
J. A. Goguen and R. M. Burstall. Introducing institutions. In Proceedings Logics of Programming Workshop, Carnegie-Mellon University, pages 221-256. Springer-Verlag, 1984. Lecture Notes in Computer Science, 164.
Robert Harper. Introduction to Standard ML. Technical Report ECS-LFCS-86-14, LFCS, Department of Computer Science, University of Edinburgh, Edinburgh, EH9 3JZ, Scotland, 1986.
Robert Harper, Robin Milner, and Mads Tofte. The definition of Standard ML. MIT Press, 1990.
S. Kahrs, D. Sannella, and A. Tarlecki. The definition of Extended ML. Draft report, Univ. of Edinburgh, 1993.
S. Kabrs, D. Sannella, and A. Tarlecki. The semantics of Extended ML: a gentle introduction. Draft report, Univ. of Edinburgh, 1993.
Edmund Kazmierczak. Modularizing the specification of a small data base system in Extended ML. Technical Report ECS-LFCS-91-177, LFCS, Department of Computer Science, University of Edinburgh, Edinburgh, EH9 3JZ, Scotland, 1991.
L. C. Paulson. ML for the Working Programmer, Cambridge University Press, 1992.
D. Sannella. Formal specification of ML programs. In Jornadas Rank Xeroz Sobre Inteligencia Artificial Razionamento Automatizado, Blanes, Spain, pages 79-98, 1987.
D. Sannella. Formal program development in Extended ML for the working programmer. In rd Workshop on Refinement, Hursley Park, January 1990. BCS/FACS. To appear.
D. Sannella, Fabio Q. B. da Silva, and A. Tarlecki. Syntax, typechecking and dynamic semantics for extended ML (version 2). Technical report, LFCS, Department of Computer Science, University of Edinburgh, 1990. Version 1 appeared as Report ECS-LFCS-89-101, Univ. of Edinburgh (1989).
D. Sannella and A. Tarleck. On observational equivalence and algebraic specification. Journal of Computer and System Sciences, 34:150-178, 1987.
D. Sannella and A. Tarleck. Extended ML: present, past and future. Technical Report ECS-LFCS-91-138, LFCS, Department of Computer Science, University of Edinburgh, Edinburgh, EH9 3JZ, Scotland, 1991. Also in Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen, GDR (Springer Lecture Notes in Computer Science).
D. Sannella and A. Tarlecki. Extended ML: an institution-independent framework for formal program development. In Workshop on Category Theory and Computer Programming, pages 364-389, Guildford, September 1986. Springer Lecture Notes in Computer Science, Vol. 240 (1986).
D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. Technical Report ECS-LFCS-89-71, LFCS, Department of Computer Science, University of Edinburgh, February 1989. Extended abstract in Proc. Intl. Colloq. on Current Issues in Programming Languages, Barcelona, Springer Lecture Notes in Computer Science. Vol. 352, 1989.
Oliver Schoett. Behavioural correctness of data representation. Science of Computer Programming, 14:43-57, 1990.
Cláudia J. A. da Silva and Fabio Q. B. da Silva. Conjuntos finitos: Um estudo de caso em desenvolvimento formal de programas em extended ml. Revista Brasileira de Computação, 1993. To appear.
J. A. Goguen and R. M. Burstall. Introducing institutions. In Proceedings Logics of Programming Workshop, Carnegie-Mellon University, pages 221-256. Springer-Verlag, 1984. Lecture Notes in Computer Science, 164.
Robert Harper. Introduction to Standard ML. Technical Report ECS-LFCS-86-14, LFCS, Department of Computer Science, University of Edinburgh, Edinburgh, EH9 3JZ, Scotland, 1986.
Robert Harper, Robin Milner, and Mads Tofte. The definition of Standard ML. MIT Press, 1990.
S. Kahrs, D. Sannella, and A. Tarlecki. The definition of Extended ML. Draft report, Univ. of Edinburgh, 1993.
S. Kabrs, D. Sannella, and A. Tarlecki. The semantics of Extended ML: a gentle introduction. Draft report, Univ. of Edinburgh, 1993.
Edmund Kazmierczak. Modularizing the specification of a small data base system in Extended ML. Technical Report ECS-LFCS-91-177, LFCS, Department of Computer Science, University of Edinburgh, Edinburgh, EH9 3JZ, Scotland, 1991.
L. C. Paulson. ML for the Working Programmer, Cambridge University Press, 1992.
D. Sannella. Formal specification of ML programs. In Jornadas Rank Xeroz Sobre Inteligencia Artificial Razionamento Automatizado, Blanes, Spain, pages 79-98, 1987.
D. Sannella. Formal program development in Extended ML for the working programmer. In rd Workshop on Refinement, Hursley Park, January 1990. BCS/FACS. To appear.
D. Sannella, Fabio Q. B. da Silva, and A. Tarlecki. Syntax, typechecking and dynamic semantics for extended ML (version 2). Technical report, LFCS, Department of Computer Science, University of Edinburgh, 1990. Version 1 appeared as Report ECS-LFCS-89-101, Univ. of Edinburgh (1989).
D. Sannella and A. Tarleck. On observational equivalence and algebraic specification. Journal of Computer and System Sciences, 34:150-178, 1987.
D. Sannella and A. Tarleck. Extended ML: present, past and future. Technical Report ECS-LFCS-91-138, LFCS, Department of Computer Science, University of Edinburgh, Edinburgh, EH9 3JZ, Scotland, 1991. Also in Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen, GDR (Springer Lecture Notes in Computer Science).
D. Sannella and A. Tarlecki. Extended ML: an institution-independent framework for formal program development. In Workshop on Category Theory and Computer Programming, pages 364-389, Guildford, September 1986. Springer Lecture Notes in Computer Science, Vol. 240 (1986).
D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. Technical Report ECS-LFCS-89-71, LFCS, Department of Computer Science, University of Edinburgh, February 1989. Extended abstract in Proc. Intl. Colloq. on Current Issues in Programming Languages, Barcelona, Springer Lecture Notes in Computer Science. Vol. 352, 1989.
Oliver Schoett. Behavioural correctness of data representation. Science of Computer Programming, 14:43-57, 1990.
Publicado
27/10/1993
Como Citar
SILVA, Cláudia J. A. da; SILVA, Fabio Q. B. da.
Finite Sets: A Case Study on Formal Program Development in the Extended ML Framework. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 7. , 1993, Rio de Janeiro/RJ.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1993
.
p. 62-76.
DOI: https://doi.org/10.5753/sbes.1993.24396.
