Hostname: page-component-cd9895bd7-gxg78 Total loading time: 0 Render date: 2024-12-19T01:45:15.107Z Has data issue: false hasContentIssue false
  • English
  • Français

Calculating modules in contextual logic program refinement

Published online by Cambridge University Press:  01 January 2008

ROBERT COLVIN ,
IAN J. HAYES  and
PAUL STROOPER
ROBERT COLVIN
Affiliation:
School of Information Technology and Electrical Engineering, University of Queensland, Brisbane, Australia (email: [email protected], [email protected], [email protected])
IAN J. HAYES
Affiliation:
School of Information Technology and Electrical Engineering, University of Queensland, Brisbane, Australia (email: [email protected], [email protected], [email protected])
PAUL STROOPER
Affiliation:
School of Information Technology and Electrical Engineering, University of Queensland, Brisbane, Australia (email: [email protected], [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

The refinement calculus for logic programs is a framework for deriving logic programs from specifications. It is based on a wide-spectrum language that can express both specifications and code, and a refinement relation that models the notion of correct implementation. In this paper we extend and generalise earlier work on contextual refinement. Contextual refinement simplifies the refinement process by abstractly capturing the context of a subcomponent of a program, which typically includes information about the values of the free variables. This paper also extends and generalises module refinement. A module is a collection of procedures that operate on a common data type; module refinement between a specification module A and an implementation module C allows calls to the procedures of A to be systematically replaced with calls to the corresponding procedures of C. Based on the conditions for module refinement, we present a method for calculating an implementation module from a specification module. Both contextual and module refinement within the refinement calculus have been generalised from earlier work and the results are presented in a unified framework.

Keywords

Logic programsrefinementmodulescontext
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 8 , Issue 1 , January 2008 , pp. 1 - 31
Copyright
Copyright © Cambridge University Press 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Back, R. J. R. 1988. A calculus of refinements for program derivations. Acta Informatica 25, 593–624.CrossRefGoogle Scholar
Bancroft, P. and Hayes, I. J. 1993. Refining a module with opaque types. In Proceedings, 16th Australian Computer Science Conference, Brisbane, Gupta, G., Mohay, G., and Topor, R., Eds. Australian Computer Science Communications 15(1), 615–624.Google Scholar
Basin, D., Deville, Y., Flener, P., Hamfelt, A. and Nilsson, J. F. 2004. Synthesis of programs in computational logic. In Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, M. Bruynooghe and Lau, K.-K., Eds. Lecture Notes in Computer Science, vol. 3049. Springer Verlag, pp. 30–65.Google Scholar
Colvin, R. 2002. Contextual and data refinement for the refinement calculus for logic programs. Ph.D. thesis, School of Information Technology and Electrical Engineering, University of Queensland.Google Scholar
Colvin, R., Groves, L., Hayes, I. J., Hemer, D., Nickson, R. and Strooper, P. 2004. Developing logic programs from specifications using stepwise refinement. In Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, Bruynooghe, M. and Lau, K.-K., Eds. Lecture Notes in Computer Science, vol. 3049. Springer Verlag, pp. 66–89.Google Scholar
Colvin, R., Hayes, I. J., Hemer, D. and Strooper, P. 2002. Translating refined logic programs to Mercury. In Proceedings of the Twenty-Fifth Australasian Computer Science Conference, Oudshoorn, M., Ed. Conferences in Research and Practice in Information Technology, vol. 4. Australian Computer Society, pp. 33–40.Google Scholar
Colvin, R., Hayes, I. J. and Strooper, P. 1998. Data refining logic programs. In International Refinement Workshop and Formal Methods Pacific 1998, Grundy, J., Schwenke, M., and Vickers, T., Eds. Discrete Mathematics and Theoretical Computer Science. Springer Verlag, pp. 100–116.Google Scholar
Colvin, R., Hayes, I. J. and Strooper, P. 2000. Refining logic programs using types. In Australasian Computer Science Conference (ACSC 2000), Edwards, J., Ed. IEEE Computer Society, pp. 43–50.Google Scholar
Colvin, R., Hayes, I. J. and Strooper, P. 2001. A technique for modular logic program refinement. In Logic Based Program Synthesis and Transformation (LOPSTR 2000), Selected Papers, Lau, K.-K., Ed. LNCS, vol. 2402. Springer, pp. 38–56.Google Scholar
Dijkstra, E. 1976. A Discipline of Programming. Prentice-Hall.Google Scholar
Hayes, I. J., Colvin, R., Hemer, D., Nickson, R. and Strooper, P. A. 2002. A refinement calculus for logic programs. Theory and Practice of Logic Programming 2, 4–5 (July–September), 425–460.Google Scholar
Hayes, I. J., Nickson, R. and Strooper, P. 1997. Refining specifications to logic programs. In Logic Program Synthesis and Transformation. Proc. of the 6th Int. Workshop, LOPSTR'96, Stockholm, Sweden, August 1996, Gallagher, J., Ed. LNCS, vol. 1207. Springer, pp. 1–19.Google Scholar
Hayes, I. J., Nickson, R., Strooper, P. and Colvin, R. 2000. A declarative semantics for logic program refinement. Tech. Rep. 00-30, Software Verification Research Centre, The University of Queensland.Google Scholar
Hemer, D., Colvin, R., Hayes, I. J. and Strooper, P. 2002. Don't care non-determinism in logic program refinement. In Proceeding of Computing: the Australasian Theory Symposium, Harland, J., Ed. Electronic Notes in Computer Science (ENTCS), vol. 61. Elsevier Science. http://www.elsevier.nl/locate/entcs/volume61.html.CrossRefGoogle Scholar
Hemer, D., Hayes, I. J. and Strooper, P. 2001. Refinement Calculus for Logic Programming in Isabelle/HOL. In Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Boulton, R. and Jackson, P., Eds. LNCS, vol. 2152. Springer, pp. 249–264.Google Scholar
Hill, P. and Lloyd, J. 1994. The Gödel Programming Language. MIT Press.Google Scholar
Lau, K.-K. and Ornaghi, M. 1997a. Forms of logic specifications: A preliminary study. In Logic Program Synthesis and Transformation. Proc. of the 6th Int. Workshop, LOPSTR'96, Stockholm, Sweden, August 1996, Gallagher, J., Ed. LNCS, vol. 1207. Springer, pp. 295–312.Google Scholar
Lau, K.-K. and Ornaghi, M. 1997b. The relationship between logic programs and specifications – the subset example revisited. J. Logic Programming 30, 3 (March), 239–257.Google Scholar
Lau, K.-K., Ornaghi, M. and Tärnlund, S.-Å. 1999. Steadfast logic programs. J. Logic Programming 38, 3 (March), 259–294.CrossRefGoogle Scholar
Liskov, B. and Guttag, J. 1986. Abstraction and Specification in Program Development. MIT Press.Google Scholar
Marriot, K. and Søndergaard, H. 1988. Prolog program transformation by introduction of difference-lists. In In Proceedings International Computer Science Conference '88. IEEE Computer Society, pp. 206–213.Google Scholar
Morgan, C. 1994. Programming from Specifications, Second ed.Prentice Hall.Google Scholar
Morgan, C. and Gardiner, P. 1990. Data refinement by calculation. Acta Informatica 27, 481–503.Google Scholar
Nickson, R. and Hayes, I. J. 1997. Supporting contexts in program refinement. Science of Computer Programming 29, 3, 279–302.Google Scholar
Partsch, H. A. 1990. Specification and Transformation of Programs. Springer-Verlag.CrossRefGoogle Scholar
Read, M. and Kazmierczak, E. 1992. Formal program development in modular Prolog. In Logic Program Synthesis and Transformation. Proc. of LOPSTR'91, University of Manchester, July 1991, Clement, T. and Lau, K.-K., Eds. LNCS, vol. 1207. Springer-Verlag, pp. 69–93.Google Scholar
Seres, S. and Spivey, M. 2000. Higher-order transformation of logic programs. In Proceedings of the Tenth International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2000), Lau, K.-K., Ed. LNCS, vol. 2042. Springer-Verlag, pp. 57–68.Google Scholar
Shapiro, E. 1989. The family of concurrent logic programming languages. ACM Comput. Surv. 21, 3, 413–510.CrossRefGoogle Scholar
Somogyi, Z., Henderson, F. and Conway, T. 1995. Mercury, an efficient purely declarative logic programming language. In Proceedings of the Eighteenth Australasian Computer Science Conference, Kotagiri, R., Ed. Australian Computer Science Communications, Glenelg, South Australia, 499–512.Google Scholar
Srinivas, Y. V. and Jullig, R. 1995. Specware: Formal support for composing software. In Mathematics of Program Construction, Möller, B., Ed. Lecture Notes in Computer Science, vol. 947. Springer, pp. 399–422.CrossRefGoogle Scholar
Sterling, L. and Shapiro, E. 1986. Second edition 1994. The Art of Prolog. MIT Press.Google Scholar
Turski, W. M. and Maibaum, T. S. E. 1987. Specification of Computer Programs. Addison-Wesley.Google Scholar