Tactics of Refinement
Resumo
The refinement calculus is a modern technique of formal program development. Its application, however, may lead to long and repetitive developments. In this paper we present a language to write refinement tactics, and present examples of useful tactics. They encompass the application of several refinements laws, but can be user as a single transformation rule. Using tactics is not a novel idea, but apparently, in the context of refinement the only existing work uses Prolog as a tactic language. Our language does not depend of any programming language or tool. Also, we are not aware of any presentation of refinement strategies written in the form of tactics as we present here.
Palavras-chave:
Formal methods, program development, refinement calculus, tactic language
Referências
R. J. R. Back, Procedural Abstraction in the Refinement Calculus. Technical report. Department of Computer Science, Abo - Finland, 1987. Ser. A No. 55.
A. L. C. Cavalcanti, A. Sampaio, and J. C. P. Woodcock. Procedures, Parameters, and Substitution in the Refinement Calculus. Technical Report TR-5-97. Oxford University Computing Laboratory, Oxford - UK, February 1997.
A. L. C. Cavalcanti, A. Sampaio, and J. C. P. Woodcock. An Inconsistency in Procedures, Parameters, and Substitution in the Refinement Calculus. Science of Computer Programming, pages 33(1):87-96, 1999.
S. L. Coutinho. T. P. C. Reis, and A. L. C. Cavalcanti. Uma Ferramenta Educacional de Refinamentos. In XIII Simpósio Brasileiro de Engenharia de Software, pages 61-64, 1999.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
J. Goguen. A. Stevenes. K. Hobley, and H. Hilberdink. 2OBJ, A Metalogical Framework Based on Equational Logic. Philosophical Transactions of the Royal Society. Series A, 339:69-86, 1992.
L. Groves, R. Nickson, and M. Utting. A Tactic Driven Refinement Tool. In C. B. Jones, R. C. Shaw, and T. Denvir, editors, 5th Refinement Workshop, Workshops in Computing, pages 272 — 297. Springer-Verlag, 1992.
A. Kaldewaij. Programming: The Derivation of Algorithms. Prentice-Hall, 1990.
A. P. Martin, P. H. B. Gardiner, and J. C. P. Woodcock. A Tactical Calculus. Formal Aspects of Computing, S(1):479-489, 1996.
C. C. Morgan. Programming from Specifications. Prentice-Hall, 2nd edition, 1994.
L. C. Paulson, ML for the Working Programmer. CUP, 1991.
A. L. C. Cavalcanti, A. Sampaio, and J. C. P. Woodcock. Procedures, Parameters, and Substitution in the Refinement Calculus. Technical Report TR-5-97. Oxford University Computing Laboratory, Oxford - UK, February 1997.
A. L. C. Cavalcanti, A. Sampaio, and J. C. P. Woodcock. An Inconsistency in Procedures, Parameters, and Substitution in the Refinement Calculus. Science of Computer Programming, pages 33(1):87-96, 1999.
S. L. Coutinho. T. P. C. Reis, and A. L. C. Cavalcanti. Uma Ferramenta Educacional de Refinamentos. In XIII Simpósio Brasileiro de Engenharia de Software, pages 61-64, 1999.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
J. Goguen. A. Stevenes. K. Hobley, and H. Hilberdink. 2OBJ, A Metalogical Framework Based on Equational Logic. Philosophical Transactions of the Royal Society. Series A, 339:69-86, 1992.
L. Groves, R. Nickson, and M. Utting. A Tactic Driven Refinement Tool. In C. B. Jones, R. C. Shaw, and T. Denvir, editors, 5th Refinement Workshop, Workshops in Computing, pages 272 — 297. Springer-Verlag, 1992.
A. Kaldewaij. Programming: The Derivation of Algorithms. Prentice-Hall, 1990.
A. P. Martin, P. H. B. Gardiner, and J. C. P. Woodcock. A Tactical Calculus. Formal Aspects of Computing, S(1):479-489, 1996.
C. C. Morgan. Programming from Specifications. Prentice-Hall, 2nd edition, 1994.
L. C. Paulson, ML for the Working Programmer. CUP, 1991.
Publicado
04/10/2000
Como Citar
OLIVEIRA, Marcel; CAVALCANTI, Ana.
Tactics of Refinement. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 14. , 2000, João Pessoa/PB.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2000
.
p. 117-132.
DOI: https://doi.org/10.5753/sbes.2000.25924.
