Skip to main content

An Operational Semantics for Constraint-Logic Imperative Programming

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10997))

Abstract

Object-oriented (OO) languages such as Java are the dominating programming languages nowadays, among other reasons due to their ability to encapsulate data and operations working on them, as well as due to their support of inheritance. However, in contrast to constraint-logic languages, they are not particularly suited for solving search problems. During development of enterprise software, which occasionally requires some search, one option is to produce components in different languages and let them communicate. However, this can be clumsy.

As a remedy, we have developed the constraint-logic OO language Muli, which augments Java with logic variables and encapsulated search. Its implementation is based on a symbolic Java virtual machine that supports constraint solving and backtracking. In the present paper, we focus on the non-deterministic operational semantics of an imperative core language.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    In other problems the return value could be a symbolic expressions if the accumulated constraints do not reduce the return value’s domain to a concrete value.

  2. 2.

    Nevertheless, Muli’s symbolic JVM supports these features exactly according to the JVM specification [12] (but does not add interesting details w.r.t. non-determinism).

  3. 3.

    In fact they are functions, since we ignore object-orientation in this presentation.

  4. 4.

    A very simple constraint solver could just take equality constraints into account. In this case, \(\gamma \models x == v\), if \(\gamma = b_1 \wedge \ldots \wedge b_k\) and for some \(j\in \{1,\ldots ,k\}~~b_k = (x == v)\).

  5. 5.

    In the implementation, the applicability of these rules will depend on the constraint propagation abilities of the employed constraint solver. We discuss the implications in Sect. 5.

  6. 6.

    https://github.com/wwu-pi/muli-env.

References

  1. Albert, E., Hanus, M., Huch, F., Oliver, J., Vidal, G.: An operational semantics for declarative multi-paradigm languages. Electron. Notes Theor. Comput. Sci. 70(6), 65–86 (2002)

    Article  Google Scholar 

  2. Bogdanas, D., Rosu, G.: K-Java: a complete semantics of Java. In: POPL 2015, pp. 1–12 (2015)

    Google Scholar 

  3. Cimadamore, M., Viroli, M.: A Prolog-oriented extension of Java programming based on generics and annotations. In: Amaral, V., et al. (eds.) Proceedings PPPJ, ACM ICPS, vol. 272, pp. 197–202. ACM (2007)

    Google Scholar 

  4. Cimadamore, M., Viroli, M.: Integrating Java and Prolog through generic methods and type inference. In: Wainwright, R.L., Haddad, H. (eds.) Proceedings of the 2008 SAC, pp. 198–205. ACM (2008). https://doi.org/10.1145/1363686

  5. Frühwirth, T., Abdennadher, S.: Essentials of Constraint Programming. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-662-05138-2

    Book  MATH  Google Scholar 

  6. Gosling, J., Joy, B., Steele, G., Bracha, G., Buckley, A.: The Java® Language Specification - Java SE 8 Edition (2015). https://docs.oracle.com/javase/specs/jls/se8/jls8.pdf

  7. Hainry, E., Péchoux, R.: Objects in polynomial time. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 387–404. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26529-2_21

    Chapter  Google Scholar 

  8. Hooker, J.N.: Operations research methods in constraint programming (Chap. 15). In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of CP. Elsevier, Amsterdam (2006)

    Google Scholar 

  9. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001)

    Article  Google Scholar 

  10. Kondoh, G., Onodera, T.: Finding bugs in Java native interface programs. In: ISSTA 2008, p. 109 (2008)

    Google Scholar 

  11. Kuchcinski, K.: Constraints-driven scheduling and resource assignment. ACM Trans. Des. Autom. Electron. Syst. 8(3), 355–383 (2003)

    Article  Google Scholar 

  12. Lindholm, T., Yellin, F., Bracha, G., Buckley, A.: The Java® Virtual Machine Specification - Java SE 8 Edition (2015). https://docs.oracle.com/javase/specs/jvms/se8/jvms8.pdf

  13. Louden, K.C.: Programming Languages: Principles and Practice. Wadsworth Publ. Co., Belmont (1993)

    MATH  Google Scholar 

  14. Majchrzak, T.A., Kuchen, H.: Logic Java: combining object-oriented and logic programming. In: Kuchen, H. (ed.) WFLP 2011. LNCS, vol. 6816, pp. 122–137. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22531-4_8

    Chapter  Google Scholar 

  15. Moss, C.: Prolog++ - The Power of Object-Oriented and Logic Programming. International Series in Logic Programming. Addison-Wesley, Boston (1994)

    Google Scholar 

  16. Ostermayer, L.: Seamless cooperation of Java and Prolog for rule-based software development. In: Proceedings of the RuleML 2015, Berlin (2015)

    Google Scholar 

  17. Scott, R.: A Guide to Artificial Intelligence with Visual Prolog. Outskirts Press (2010)

    Google Scholar 

  18. Shapiro, E., Takeuchi, A.: Object oriented programming in concurrent Prolog. New Gener. Comput. 1(1), 25–48 (1983)

    Article  Google Scholar 

  19. Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine - Definition, Verification, Validation. Springer, Heidelberg (2001). https://doi.org/10.1007/978-3-642-59495-3

    Book  MATH  Google Scholar 

  20. Triska, M.: The finite domain constraint solver of SWI-Prolog. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 307–316. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29822-6_24

    Chapter  MATH  Google Scholar 

  21. Van Roy, P., Brand, P., Duchier, D., Haridi, S., Schulte, C., Henz, M.: Logic programming in the context of multiparadigm programming: the Oz experience. Theory Pract. Log. Program. 3(6), 717–763 (2003)

    Article  Google Scholar 

  22. Warren, D.H.D.: An abstract Prolog instruction set. Technical report, SRI International, Menlo Park (1983)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Jan C. Dageförde .

Editor information

Editors and Affiliations

Appendix: Full Example Evaluation

Appendix: Full Example Evaluation

In addition to \(\rho _0\), \(\sigma _0\), and \(\gamma _1\) defined in section Sect. 4, the following auxiliary definitions will be needed as intermediate results: \(\rho _1 = \rho _0[x/\alpha _1, y/\alpha _2]\), \(\rho _2 = \rho _0[b/\alpha _3, y/\alpha _4]\), \(\rho _3 = \rho _2[i/\alpha _5,r/\alpha _6]\), \(\rho _4 = \rho _3[i/\alpha _7, r/\alpha _8]\), \(\sigma _1 = \sigma _0[\alpha _1/1, \alpha _2/\alpha _2]\), \(\sigma _2 = \sigma _1[\alpha _3/2, \alpha _4/\alpha _2]\), \(\sigma _3 = \sigma _2[\alpha _7/0, \alpha _8/1]\), \(\sigma _4 = \sigma _3[\alpha _0/1]\), \(\sigma _5 = \sigma _4[\alpha _0/\!\perp ]\), \(\sigma _6 = \sigma _5[\alpha _0/0]\), \(\gamma _2 = \gamma _1 \wedge \alpha _2 \le 0\), and \(\gamma _3 = \gamma _2 \wedge \alpha _2 == 0 \). To simplify the understanding of the full computation provided in Sect. 4, we have decomposed it into a couple of lemmas. We present the computation in a top-down fashion. If you prefer a bottom-up fashion, just read the lemmas in reverse order. The names of the applied rules are specified in each step.

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dageförde, J.C., Kuchen, H. (2018). An Operational Semantics for Constraint-Logic Imperative Programming. In: Seipel, D., Hanus, M., Abreu, S. (eds) Declarative Programming and Knowledge Management. WFLP WLP INAP 2017 2017 2017. Lecture Notes in Computer Science(), vol 10997. Springer, Cham. https://doi.org/10.1007/978-3-030-00801-7_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-00801-7_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-00800-0

  • Online ISBN: 978-3-030-00801-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics