Abstract
Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we explore approaches to provably correct code generation based on programming language semantics, particularly Horn logical semantics, and partial evaluation. We show that the definite clause grammar (DCG) notation can be used for specifying both the syntax and semantics of imperative languages. We next show that continuation semantics can also be expressed in the Horn logical framework.
The authors have been partially supported by NSF grants CCR 9900320, INT 9904063, and EIA 0130847, by the Department of Education and the Environmental Protection Agency, and by the Information Society Technologies programme of the European Commission, Future and Emerging Technologies under the IST-2001-38059 ASAP project.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Brogi, A., Contiero, S.: Specializing Meta-Level Compositions of Logic Programs. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207. Springer, Heidelberg (1997)
Debray, S.: Resource bounded partial evaluation. In: PEPM 1997, pp. 179–192 (1997)
Dold, A., Gaul, T., Zimmermann, W.: Mechanized Verification of Compiler Backends. In: Proc. Software Tools for Technology Transfer, Denmark (1998)
Faulk, S.R.: State Determination in Hard-Embedded Systems. Ph.D. Thesis. Univ. of NC, Chapel Hill, NC (1989)
Futamura, Y.: Partial Evaluation of Computer Programs: An approach to compilercompiler. J. Inst. Electronics and Comm. Engineers, Japan (1971)
Gupta, G.: Horn Logic Denotations and Their Applications. In: The Logic Programming Paradigm: A 25 year perspective, pp. 127–160. Springer, Heidelberg (1999)
Gupta, G., Pontelli, E.: A Constraint-based Denotational Approach to Specification and Verification of Real-time Systems. In: Proc. IEEE Real-time Systems Symposium, December 1997, pp. 230–239 (1997)
Gupta, G., Pontelli, E.: A Logic Programming Framework for Specification and Implementation of Domain Specific Languages. In: Essays in Honor of Robert Kowalski, vol. LNAI. Springer, Heidelberg (2003)
Henninger, K.L.: Specifying software requirements for complex systems: New techniques and their application. IEEE Trans. on Software Engg. 5(1), 2–13
Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated Consistency Checking of Requirements Specifications. ACM TOSEMÂ 5(3) (1996)
Hoare, C.A.R.: The Verifying Compiler: A Grand Challenge for Computing Research. J. ACM 50(1), 63–69 (2003)
Jones, N.: Introduction to Partial Evaluation. ACM Computing Surveys 28(3), 480–503
King, L., Gupta, G., Pontelli, E.: Verification of BART Controller. In: High Integrity Software. Kluwer Academic, Dordrecht (2001)
Leuschel, M., Jørgensen, J., Vanhoof, W., Bruynooghe, M.: Offline specialization in Prolog using a hand-written compiler generator. Theory and Practice of Logic Programming 4(1), 139–191 (2004)
Leuschel, M., Martens, B., De Schreye, D.: Controlling Generalization and Polyvariance in Partial Deduction of Normal Logic Programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 20(1), 208–258
Leonard, E.I., Heitmeyer, C.L.: Program Synthesis from Requirements Specifications Using APTS. Kluwer Academic Publishers, Dordrecht (2002)
Lloyd, J.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987)
McCarthy, J., Painter, J.: Correctness of a Compiler for Arithmetic Expressions. MIT AI Lab Memo (1967)
Owen, S.: Issues in the Partial Evaluation of Meta-Interpreters. In: Proceedings Meta 1988, pp. 319–339. MIT Press, Cambridge (1988)
Paige, R.: Viewing a Program Transformation System at Work. In: Proc. Programming Language Implementation and Logic Programming. LNCS, vol. 844. Springer, Heidelberg (1994)
Pnueli, A., Siegel, M., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 151. Springer, Heidelberg (1998)
Sahlin, D.: An Automatic Partial Evaluator for Full Prolog. Ph.D. Thesis. 1994. Royal Institute of Tech., Sweden., Available at http://www.sics.se
Schmidt, D.: Denotational Semantics: a Methodology for Language Development. W.C. Brown Publishers (1986)
Sterling, L., Shapiro, S.: The Art of Prolog. MIT Press, Cambridge (1994)
Wang, Q., Gupta, G., Leuschel, M.: Horn Logical Continuation Semantics. UT Dallas Technical Report (2004)
Wang, Q., Gupta, G.: Resource Bounded Compilation via Constrained Partial Evaluation. UTD Technical Report. Forthcoming
Winter, V.L.: Program Transformation in HATS. Software Transformation Systems Workshop (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, Q., Gupta, G., Leuschel, M. (2005). Towards Provably Correct Code Generation via Horn Logical Continuation Semantics. In: Hermenegildo, M.V., Cabeza, D. (eds) Practical Aspects of Declarative Languages. PADL 2005. Lecture Notes in Computer Science, vol 3350. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30557-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-30557-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24362-5
Online ISBN: 978-3-540-30557-6
eBook Packages: Computer ScienceComputer Science (R0)