Deriving Applicative Programs from Formal Specifications
Abstract
We introduce a notation to write functional (declarative, applicative) programs and consider ways in which to derive applicative implementations of formal specifications written using the Z formalism. In this paper we consider Z as the ulmost level of abstraction, and A, the functional language, as the most operational formalism available to the programmer. Our goal is to consider the properties of a formal programming environment in which to derive functional programs from mathematical specifications of their properties, as a (first step) of building reliable pieces of software. We also consider the intricacies of automating (parts of) the process.References
Programming Denotational Semantics. Computer J., 1983.
On the Use of Formal Methods in Software Development. 9th. Intl. Conf. on Softw. Eng., Monterey, CA, Apr. 1967.
On Understanding Types, Data Abstraction and Polymorphism. Comp. Surv. 17 (4), Dec. 1985.
Cohen, B., Harwood, W. T., Jackson, M. I.: The Specification of Complex Systems. Addison-Wesley, Wokingham, (UK), 1986.
Croft, S.: Implementation of Functional Languages. MSc Thesis, Rutherford College, University of Kent at Canterbury, 1985.
Darlington, J, Field, A. J., Pull, H.: The Unification of Functional and Logic Languages. IC-CS Internal Report, Imperial College, London, (UK), 1986.
Goguen, J., Mesequer, J. A.: Rapid Prototyping in the OBJ Executable Specification Language, SRI Intl., TR CSL-137, Aug. 1982.
Hayes, I. (ed): Specification Case Studies. Prentice Hall Intl (UK), 1987.
Henderson, P., Minkovitz, C.: The me too method of software design. ICL Tech. J., May 1986.
Jones, C. B.: Systematic Sofware Development Using VDM, Prentice Hall Intl (UK), 1986.
Lins, R.D.: Categorical Multi-Combinators. Computing Lab Report 41, University of Kent at Centerbury, 1986.
Meira, S.: On The Efficiency of Applicative Algorithms. PhD Thesis, Rutherford College, University of Kent at Canterbury, 1985.
Meira, S.: Grafos de Desenvolvimento de Software, Z e a Especificacao do Arco-Iris. In portuguese. To appear.
Meira, S.: A Linguagem de Programacao Funcional. In portuguese. To appear.
Meira, S.: From Z to A: Deriving Applicative Programs from Formal Specifications. Outline of the SPIone project. To appear.
Meira, S.: Hipertexto. Projeto de Pesquisa Submetido ao CNPq. Personal Communication.
Meira, S., Sampaio, A, Salazar, C., Sombra, M. and Souto Maior, R.: Z: Notacao Computacional e Especificacoes. In portuguese. To appear.
Melo Neto, C.: Orto, Um Revisor Ortográfico. Proc. Semish 1987, SBC, Salvador, 1987.
Turner, D. A: Miranda: A non strict functional language with polymorphic types. Proc. Semish 1986, SBC, Recife, 1986.
Wadler, P.: An introduction to ORWELL PRG Internal Report, Oxford University, (UK), 1986.
Wirth, N.: Programing in Modula-2 Springer-Verlag, Heidelberg 1983.
Zove, P.: The Operational versus the Conventional Approach to Software Development. CACM, Feb. 1984
On the Use of Formal Methods in Software Development. 9th. Intl. Conf. on Softw. Eng., Monterey, CA, Apr. 1967.
On Understanding Types, Data Abstraction and Polymorphism. Comp. Surv. 17 (4), Dec. 1985.
Cohen, B., Harwood, W. T., Jackson, M. I.: The Specification of Complex Systems. Addison-Wesley, Wokingham, (UK), 1986.
Croft, S.: Implementation of Functional Languages. MSc Thesis, Rutherford College, University of Kent at Canterbury, 1985.
Darlington, J, Field, A. J., Pull, H.: The Unification of Functional and Logic Languages. IC-CS Internal Report, Imperial College, London, (UK), 1986.
Goguen, J., Mesequer, J. A.: Rapid Prototyping in the OBJ Executable Specification Language, SRI Intl., TR CSL-137, Aug. 1982.
Hayes, I. (ed): Specification Case Studies. Prentice Hall Intl (UK), 1987.
Henderson, P., Minkovitz, C.: The me too method of software design. ICL Tech. J., May 1986.
Jones, C. B.: Systematic Sofware Development Using VDM, Prentice Hall Intl (UK), 1986.
Lins, R.D.: Categorical Multi-Combinators. Computing Lab Report 41, University of Kent at Centerbury, 1986.
Meira, S.: On The Efficiency of Applicative Algorithms. PhD Thesis, Rutherford College, University of Kent at Canterbury, 1985.
Meira, S.: Grafos de Desenvolvimento de Software, Z e a Especificacao do Arco-Iris. In portuguese. To appear.
Meira, S.: A Linguagem de Programacao Funcional. In portuguese. To appear.
Meira, S.: From Z to A: Deriving Applicative Programs from Formal Specifications. Outline of the SPIone project. To appear.
Meira, S.: Hipertexto. Projeto de Pesquisa Submetido ao CNPq. Personal Communication.
Meira, S., Sampaio, A, Salazar, C., Sombra, M. and Souto Maior, R.: Z: Notacao Computacional e Especificacoes. In portuguese. To appear.
Melo Neto, C.: Orto, Um Revisor Ortográfico. Proc. Semish 1987, SBC, Salvador, 1987.
Turner, D. A: Miranda: A non strict functional language with polymorphic types. Proc. Semish 1986, SBC, Recife, 1986.
Wadler, P.: An introduction to ORWELL PRG Internal Report, Oxford University, (UK), 1986.
Wirth, N.: Programing in Modula-2 Springer-Verlag, Heidelberg 1983.
Zove, P.: The Operational versus the Conventional Approach to Software Development. CACM, Feb. 1984
Published
1987-10-22
How to Cite
MEIRA, Silvio Lemos.
Deriving Applicative Programs from Formal Specifications. In: BRAZILIAN SYMPOSIUM ON SOFTWARE ENGINEERING (SBES), 1. , 1987, Rio de Janeiro/RJ.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1987
.
p. 109-119.
ISSN 2833-0633.
DOI: https://doi.org/10.5753/sbes.1987.25222.
