Sobre o Teorema da Modularização: Importância e uma Prova por Quociente
Resumo
Especificações são tratadas como apresentação de teorias, ou seja, teorias em linguagens poli-sortidas de primeira ordem definidas por um conjtinto de axiomas. Discutimos o papel fundamental desempenhado pelo Teorema dá Modularização no processo de implementação pelo paradigma do passo canônico e na passagem de parâmetros nas especificações parametrizadas. Apresentamos uma demonstração do Teorema da Modularização que introduz uma nova forma de se construir teorias: a teoria quociente induzida por uma interpretação.
Referências
Ehrich, H. -D. On the Theory of Specification, Implementation and Parametrization of Abstract Data Types. Journal ACM. Vol 29. N 1. 1982.
Ehrig, H. and Mabr, B. Fundamentals of Algebraic Specification 1 Equations and Initial Semantics. Springer-Verlag Berlin Heidelberg. 1985.
Enderton, H. B. A Mathematical Introduction to Logic. Academic Press, INC. 1972.
Haeberer, A. M.; Veloso, P. A. S.; Maibaum, T. S. E. Towards Formal Coherent Meta-Models for the Software Development Process. Mon. Em Ciência da Comp. Dep. de Informática. PUC - RJ. N 18. 1992.
Maibaum, T. S. E.; Turski, W. M. The Specification of Computer Programas. Addison-Wesley, Workingham. 1987.
Manna, Z. The Mathematical Theory of Computation. McGraw-Hill, New York. 1974.
Rodenburg, P. H. and Glabbek, R. J. An interpolation Theorem in Equational Logic. Report CS-R8838, Center for Mathematics and Computer Science PO Box 4079, 1009 AB Amsterdam, The Netherlands.
Shoenfield, J. R. Mathematical Logic. Addison-Wesley, Reading. 1967.
Smith, D. R. Constructing Specification Morphisms. Kestrel Institute, Tech. Rept. KES.U.92.1, Palo Alto. April 1992.
Toscani, L. V. e Veloso, P. A. S. A Programação Dinâmica: um caso particular de divisão e conquista. Revista de Informática Teórica e Aplicada. Vol 1. N 2. Maio 1990. p.53-67.
Toscani, L. V. e Veloso, P. A. S. Uma metodologia para cálculo de complexidade de algoritmos. IV Simp. Bras. de Eng. de Software. Águas de São Pedro, SP. 1990. p. 183-192.
Veloso, P. A. S.; Veloso, S. R. M. Problem Decomposition and Reduction: applicability, soundness, completeness. Trappl, R.; Klir, J.; Pichler, F. (eds) Progress in Cybernetics and Systems Research. Hemisphere, Washington, DC. 1981. p. 199-203.
Veloso, P. A. S.; Maibaum, T. S. E.; Sadler, M. R. Programme Development and Theory Manipulation. Proc. International Workshop on Software Specification and Design. London. Ago 1985. p. 228-232.
Veloso, P. A. S. Verificação e Estruturação de Programas com Tipos Abstratos de Dados. Editora Edgard Blicher, São Paulo, SP. 1987.
Veloso, P. A. S. Problem Solving by Interpretation of Theories. Carnielli, W.A.: Alcântara, L.P. (eds). Methods and Applications of Mathematical Logic. American Mathematical Society, Providence. 1988. p. 241-250. Vol 69.
Veloso, P. A. S. Program Construction (with data abstractions) as transformations on theories. Alcoforado, P. (ed). Lógica, Computação e Epistemologia: ensaios em homenagem ao Prof. Jorge Barbosa. ILTC, RJ. 1991. pag.319 - 371.
Veloso, P. A. S. On the Modularisation Theorem for Logical Specifications: its role and proof. Monografias em Ciência da Computação. n 17/92. Dep. Informática-PUC. Rio de Janeiro.
Veloso, P. A. S. On Interpretations of Logical Specifications and the Modularization Theorem. Kestrel Research Inst. Res. Rept. Fev 1993.