×

The lattice of data refinement. (English) Zbl 0790.68028

Summary: We define a general notion of data refinement that comprises the traditional notion of data refinement as a special case. Using the concepts of duals and adjoints, we define converse commands and find a symmetry between ordinary data refinement and a dual (backward) data refinement. We show how ordinary and backward data refinement are interpreted as simulation, and we derive rules for the piecewise data refinement of programs. Our results are valid for a general language, including domonic and angelic nondeterminism as well as nontermination and micracles.

MSC:

68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)
68N01 General topics in the theory of software
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M., Lamport, L.: The existence of refinement mappings. In: Proc 3rd Annual IEEE Symp. on Logic in Computer Science, pp. 165-175, Edinburgh 1988
[2] Back, R.J.R.: Correctness Preserving Program Refinements: Proof Theory and Applications, vol. 131 of Mathematical Center Tracts. Amsterdam: Mathematical Centre 1980 · Zbl 0451.68018
[3] Back, R.J.R.: A calculus of refinements for program derivations. Acta Inf.25, 593-624 (1988) · Zbl 0658.68018 · doi:10.1007/BF00291051
[4] Back, R.J.R.: Changing data representation in the refinement calculus. In: 21st Hawaii International Conference on System Sciences 1989
[5] Back, R.J.R.: Refinement calculus, part II: parallel and reactive programs. In: Bakker, J.W. de, Roever, W.P., Rozenberg, G. (eds.) Stepwise refinement of distributed systems. Models, formalisms, correctness. REX Workshop, Mook, The Netherlands (Lect. Notes Comput. Sci., vol. 430, pp. 67-93) Berlin, Heidelberg, New York: Springer 1989
[6] Back, R.J.R.: Refining atomicity in parallel algorithms. In: Odijk, E., Rem, M., Syre, J.C. (eds.) PARLE’89. Conference on Parallel Architectures and Languages Europe, Eindhoven, The Netherlands (Lect. Notes Comput. Sci., vol. 366, pp. 199-216) Berlin, Heidelberg, New York: Springer 1989
[7] Back, R.J.R., Wright, J. von: Refinement calculus, part I: Sequential non deterministic programs. In: Bakker, J.W. de, Roever, W.P., Rozenberg, G. (eds.) Stepwise refinement of distributed systems. Models, formalisms, correctness. REX Workshop, Mook, The Netherlands (Lect. Notes Comput. Sci., vol. 430, pp. 42-66) Berlin, Heidelberg, New York: Springer 1989
[8] Back, R.J.R., Wright, J. von: Duality in specification languages: a lattice-theoretical approach. Acta Inf.27, 583-625 (1990) · Zbl 0699.68038 · doi:10.1007/BF00259469
[9] Back, R.J.R., Wright, J. von: Statement inversion and strongest postcondition. Sci. Comput. Program.20, 223-251 (1993) · Zbl 0780.68010 · doi:10.1016/0167-6423(93)90015-H
[10] Chen, W., Udding, J.T.: Towards a calculus of data refinement. In: Shepscheut, J.L. van de (ed.) Mathematics of program construction. International Conference, Groningen, The Netherlands (Lect. Notes Comput. Sci., vol. 375, pp. 197-218) Berlin, Heidelberg, New York: Springer 1989
[11] Dijkstra, E.W.: A discipline of programming. Englewood Cliffs, NJ: Prentice-Hall 1976 · Zbl 0368.68005
[12] Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics (Texts Monogr. Comput. Sci.) Berlin, Heidelberg, New York: Springer 1990 · Zbl 0698.68011
[13] Gardiner, P.H., Morgan, C.C.: A single complete rule for data refinement. Manuscript, 1991 · Zbl 0774.68081
[14] Gardiner, P.H., Morgan, C.C.: Data refinement of predicate transformers. Theor. Comput. Sci.87(1), 143-162 (1991) · Zbl 0736.68060 · doi:10.1016/0304-3975(91)90029-2
[15] He, J., Hoare, C.A.R., Sanders, J.W.: Prespecification in data refinement. Inf. Process. Lett.25, 71-76 (1987) · Zbl 0624.68027 · doi:10.1016/0020-0190(87)90224-9
[16] Hoare, C.A.R.: Proofs of correctness of data representation. Acta Inf.1(4), 271-281 (1972) · Zbl 0244.68009 · doi:10.1007/BF00289507
[17] Jonsson, B.: On decomposing and refining specifications of distributed systems. In: Bakker, J.W. de, Roever, W.P., Rozenberg, G. (eds.) Stepwise refinement of distributed systems. Models, formalisms, correctness. REX Workshop, Mook, The Netherlands (Lect. Notes Comput. Sci., vol. 430, pp. 361-385) Berlin, Heidelberg, New York: Springer 1989
[18] Jonsson, B.: Simulations between specifications of distributed systems. In: Baeten, J.C., Groote, J.F. (eds.) CONCUR’91. Proceedings of 2nd International Conference on Concurrency Theory (Lect. Notes Comput Sci., vol. 527, pp. 346-360) Berlin, Heidelberg, New York: Springer 1991
[19] Morgan, C.C., Gardiner, P.H.: Data refinement by calculation. Acta Inf.27, 481-503 (1990) · Zbl 0699.68029 · doi:10.1007/BF00277386
[20] Morgan, C.C.: Data refinement by miracles. Inf. Process. Lett.26, 243-246 (1988) · doi:10.1016/0020-0190(88)90147-0
[21] Morgan, C.C.: The specification statement. ACM Trans. Program. Lang. Syst.10(3), 403-419 (1988) · Zbl 0825.68302 · doi:10.1145/44501.44503
[22] Morgan, C.C., Woodcock, J.: Of wp and CSP. In: Proceedings of VDM-91, 1991
[23] Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Programm.9, 287-306 (1987) · Zbl 0624.68017 · doi:10.1016/0167-6423(87)90011-6
[24] Morris, J.M.: Laws of data refinement. Acta Inf.26, 287-308 (1989) · Zbl 0661.68018
[25] Nelson, G.: A generalization of Dijkstra’s calculus. ACM Trans. Program. Lang. Syst.11 (4), 517-562 (1989) · doi:10.1145/69558.69559
[26] Wright, J. von: A lattice-theoretical basis for program refinement. PhD thesis, Åbo Akademi University, Turku, Finland 1990
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.