The Community for Technology Leaders
Formal Engineering Methods, International Conference on (2000)
York, England
Sept. 4, 2000 to Sept. 7, 2000
ISBN: 0-7695-0822-7
pp: 157
Ali E. Abdallah , South Bank University
ABSTRACT
In recent years, there have been growing interests in systematic methods for refining Z specifications into programs. In this paper, we consider a transformational programming strategy known as filter promotion and examine its use for refining a class of Z specifications into sequential as well as parallel programs. This strategy is particularly useful for transforming specifications of generate and test problems into efficient algorithms. We find it convenient to use different notations at different level of abstractions: Z to capture the starting specification, Bird-Meertens functional notation to express algorithms and Hoare's CSP to describe parallelism and communications. The basic ideas are illustrated by systematic transformational developments of sequential and parallel algorithms for sorting and searching problems.
INDEX TERMS
Specification, refinement, program transformation, filter promotion, accumulation, parallelism, communicating processes
CITATION

A. E. Abdallah, "Filter Promotion Transformation Strategies for Deriving Efficient Programs from Z Specifications," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 157.
doi:10.1109/ICFEM.2000.873816
84 ms
(Ver 3.3 (11022016))