Document Open Access Logo

TreatJS: Higher-Order Contracts for JavaScripts

Authors Matthias Keil, Peter Thiemann

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2015.28.pdf
  • Filesize: 0.6 MB
  • 24 pages

Document Identifiers

Author Details

Matthias Keil
Peter Thiemann

Cite As Get BibTex

Matthias Keil and Peter Thiemann. TreatJS: Higher-Order Contracts for JavaScripts. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 28-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.ECOOP.2015.28

Abstract

TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of non-interfering contract execution, its systematic approach to blame assignment, its support for contracts in the style of union and intersection types, and its notion of a parameterized contract scope, which is the building block for composable run-time generated contracts that generalize dependent function contracts.
 
TreatJS is implemented as a library so that all aspects of a contract can be specified using the full JavaScript language. The library relies on JavaScript proxies to guarantee full interposition for contracts. It further exploits JavaScript's reflective features to run contracts in a sandbox environment, which guarantees that the execution of contract code does not modify the application state. No source code transformation or change in the JavaScript run-time system is required. The impact of contracts on execution speed is evaluated using the Google Octane benchmark.

Subject Classification

Keywords
  • Higher-Order Contracts
  • JavaScript
  • Proxies

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Parker Abercrombie and Murat Karaorman. jContractor: Design by contract for Java. http://jcontractor.sourceforge.net/, 2003.
  2. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for all. In Thomas Ball and Mooly Sagiv, editors, Proceedings 38th Annual ACM Symposium on Principles of Programming Languages, pages 201-214, Austin, TX, USA, January 2011. ACM Press. Google Scholar
  3. Jean-Baptiste Arnaud, Marcus Denker, Stéphane Ducasse, Damien Pollet, Alexandre Bergel, and Mathieu Suen. Read-only execution for dynamic languages. In Jan Vitek, editor, Objects, Models, Components, Patterns, 48th International Conference, TOOLS 2010, Málaga, Spain, June 28 - July 2, 2010. Proceedings, volume 6141 of Lecture Notes in Computer Science, pages 117-136, Málaga, Spain, June 2010. Springer. Google Scholar
  4. Thomas H. Austin, Tim Disney, and Cormac Flanagan. Virtual values for language extension. In Cristina Videira Lopes and Kathleen Fisher, editors, OOPSLA, pages 921-938, Portland, OR, USA, 2011. ACM. Google Scholar
  5. Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de' Liguoro. Intersection and union types: Syntax and semantics. Information and Computation, 119(2):202-230, 1995. Google Scholar
  6. Nuel Belnap. A useful four-valued logic. In J. Michael Dunn and George Epstein, editors, Modern Uses of Multiple-Valued Logic, volume 2 of Episteme, pages 5-37. Springer Netherlands, 1977. Google Scholar
  7. João Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C. Pierce. Polymorphic contracts. In Gilles Barthe, editor, Proceedings of the 20th European Symposium on Programming, volume 6602 of Lecture Notes in Computer Science, pages 18-37, Saarbrücken, Germany, March 2011. Springer-Verlag. Google Scholar
  8. Matthias Blume and David McAllester. Sound and complete models of contracts. Journal of Functional Programming, 16:375-414, July 2006. Google Scholar
  9. Gilad Bracha and David Ungar. Mirrors: Design principles for meta-level facilities of object-oriented programming languages. In John M. Vlissides and Douglas C. Schmidt, editors, OOPSLA, pages 331-344. ACM, 2004. Google Scholar
  10. Lorenzo Caminiti. Contract++, contract programming library for C++. http://sourceforge.net/projects/contractpp/, August 2012.
  11. Giuseppe Castagna, Nils Gesbert, and Luca Padovani. A theory of contracts for Web services. ACM Transactions on Programming Languages and Systems, 31(5), 2009. Google Scholar
  12. Olaf Chitil. Practical typed lazy contracts. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP 2012). ACM, September 2012. Google Scholar
  13. Mario Coppo and M. Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv. Math. Logik, 19(139-156), 1978. Google Scholar
  14. Christos Dimoulas and Matthias Felleisen. On contract satisfaction in a higher-order world. ACM Transactions on Programming Languages and Systems, 33(5):16, 2011. Google Scholar
  15. Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, and Matthias Felleisen. Correct blame for contracts: No more scapegoating. In Thomas Ball and Mooly Sagiv, editors, Proceedings 38th Annual ACM Symposium on Principles of Programming Languages, pages 215-226, Austin, TX, USA, January 2011. ACM Press. Google Scholar
  16. Christos Dimoulas, Riccardo Pucella, and Matthias Felleisen. Future contracts. In António Porto and Francisco J. López-Fraguas, editors, Principles and Practice of Declarative Programming, PPDP 2009, pages 195-206, Coimbra, Portugal, September 2009. ACM. Google Scholar
  17. Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Complete monitors for behavioral contracts. In European Symposium on Programming, volume 7211 of Lecture Notes in Computer Science, Tallinn, Estland, April 2012. Springer-Verlag. Google Scholar
  18. Tim Disney. contracts.js. https://github.com/disnet/contracts.js, April 2013.
  19. Tim Disney, Nathan Faubion, David Herman, and Cormac Flanagan. Sweeten your JavaScript: Hygienic macros for ES5. In Andrew P. Black and Laurence Tratt, editors, DLS, pages 35-44, Portland, OR, USA, October 2014. ACM. Google Scholar
  20. Tim Disney, Cormac Flanagan, and Jay McCarthy. Temporal higher-order contracts. In Olivier Danvy, editor, Proceedings International Conference on Functional Programming 2011, pages 176-188, Tokyo, Japan, September 2011. ACM Press, New York. Google Scholar
  21. ECMAScript Language Specification, December 2009. ECMA International, ECMA-262, 5th edition. Google Scholar
  22. Manuel Fähndrich, Michael Barnett, and Francesco Logozzo. Embedded contract languages. In Sung Y. Shin, Sascha Ossowski, Michael Schumacher, Mathew J. Palakal, and Chih-Cheng Hung, editors, Proceedings of the 2010 ACM Symposium on Applied Computing, pages 2103-2110, Sierre, Switzerland, 2010. ACM. Google Scholar
  23. Robert Bruce Findler and Matthias Blume. Contracts as pairs of projections. In Philip Wadler and Masami Hagiya, editors, Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, pages 226-241, Fuji Susono, Japan, April 2006. Springer-Verlag. Google Scholar
  24. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In Simon Peyton-Jones, editor, Proceedings International Conference on Functional Programming 2002, pages 48-59, Pittsburgh, PA, USA, October 2002. ACM Press, New York. Google Scholar
  25. Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Proceedings of the 2002 Conference on Programming Language Design and Implementation, pages 234-245, Berlin, Germany, June 2002. ACM Press. Google Scholar
  26. Matthew Flatt, Robert Bruce Findler, and PLT. The Racket Guide, v.6.0 edition, March 2014. URL: http://docs.racket-lang.org/guide/index.html.
  27. Joseph A. Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11-20, 1982. Google Scholar
  28. google-caja: A source-to-source translator for securing JavaScript-based web content. http://code.google.com/p/google-caja/, (as of 2011).
  29. Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts made manifest. In Proceedings 37th Annual ACM Symposium on Principles of Programming Languages, pages 353-364, Madrid, Spain, January 2010. ACM Press. Google Scholar
  30. David R. Hanson and Todd A. Proebsting. Dynamic variables. In Proceedings of the 2001 Conference on Programming Language Design and Implementation, pages 264-273, Snowbird, UT, USA, June 2001. ACM Press, New York, USA. Google Scholar
  31. Phillip Heidegger, Annette Bieniusa, and Peter Thiemann. Access permission contracts for scripting languages. In John Field and Michael Hicks, editors, Proceedings 39th Annual ACM Symposium on Principles of Programming Languages, pages 111-122, Philadelphia, USA, January 2012. ACM Press. Google Scholar
  32. Richard Helm, Ian M. Holland, and Dipayan Gangopadhyay. Contracts: specifying behavioral compositions in object-oriented systems. In Norman K. Meyrowitz, editor, Conference Object Oriented Programming, Systems, Languages, and Applications / European Conference on Object-Oriented Programming, pages 169-180, Ottawa, Canada, October 1990. Google Scholar
  33. Ralf Hinze, Johan Jeuring, and Andres Löh. Typed contracts for functional programming. In Philip Wadler and Masami Hagiya, editors, Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, pages 208-225, Fuji Susono, Japan, April 2006. Springer-Verlag. Google Scholar
  34. Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann. Transparent object proxies for JavaScript. In John Boyland, editor, ECOOP, volume ?, Prague, Czech Repulic, July 2015. LIPICS. to appear. Google Scholar
  35. Matthias Keil and Peter Thiemann. Efficient dynamic access analysis using JavaScript proxies. In Proceedings of the 9th Symposium on Dynamic Languages, DLS '13, pages 49-60, New York, NY, USA, 2013. ACM. Google Scholar
  36. Matthias Keil and Peter Thiemann. TreatJS: Higher-order contracts for JavaScript. Technical report, Institute for Computer Science, University of Freiburg, 2015. Google Scholar
  37. Reto Kramer. iContract - the Java design by contract tool. In Proceedings of the Technology of Object-Oriented Languages and Systems, pages 295-307, Santa Barbara, CA, USA, 1998. IEEE Computer Society. Google Scholar
  38. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175-188, Norwell, MA, USA, 1999. Kluwer Academic Publishers. Google Scholar
  39. Bertrand Meyer. Object-Oriented Software Construction. Prentice-Hall, 1988. Google Scholar
  40. Mark S. Miller, Tom Van Cutsem, and Bill Tulloh. Distributed electronic rights in JavaScript. In Matthias Felleisen and Philippa Gardner, editors, ESOP, volume 7792 of Lecture Notes in Computer Science, pages 1-20, Rome, Italy, March 2013. Springer. Google Scholar
  41. Mark S. Miller, Mike Samuel, Ben Laurie, Ihab Awad, and Mike Stay. Caja: Safe active content in sanitized JavaScript. http://google-caja.googlecode.com, 2008. Google White Paper.
  42. Mark Samuel Miller. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, Baltimore, MD, USA, 2006. AAI3245526. Google Scholar
  43. John C. Reynolds. Gedanken - a simple typeless language based on the principle of completeness and the reference concept. Commun. ACM, 13(5):308-319, 1970. Google Scholar
  44. T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. Chaperones and impersonators: Run-time support for reasonable interposition. In Gary T. Leavens and Matthew B. Dwyer, editors, OOPSLA, pages 943-962. ACM, 2012. Google Scholar
  45. Sam Tobin-Hochstadt and David Van Horn. Higher-order symbolic execution via contracts. In Gary T. Leavens and Matthew B. Dwyer, editors, OOPSLA, pages 537-554. ACM, 2012. Google Scholar
  46. Jesse A. Tov and Riccardo Pucella. Stateful contracts for affine types. In Andrew D. Gordon, editor, ESOP 2010, volume 6012 of Lecture Notes in Computer Science, pages 550-569. Springer-Verlag, 2010. Google Scholar
  47. Tom Van Cutsem and Mark S. Miller. Proxies: Design principles for robust object-oriented intercession APIs. In William D. Clinger, editor, DLS, pages 59-72. ACM, 2010. Google Scholar
  48. Tom Van Cutsem and Mark S. Miller. Trustworthy proxies - virtualizing objects with invariants. In Giuseppe Castagna, editor, ECOOP, volume 7920 of Lecture Notes in Computer Science, pages 154-178, Montpellier, France, July 2013. Springer. Google Scholar
  49. Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In Proceedings 18th European Symposium on Programming, volume 5502 of Lecture Notes in Computer Science, pages 1-16, York, UK, March 2009. Springer. Google Scholar
  50. Dana N. Xu, Simon L. Peyton Jones, and Koen Claessen. Static contract checking for Haskell. In Benjamin Pierce, editor, Proceedings 36th Annual ACM Symposium on Principles of Programming Languages, pages 41-52, Savannah, GA, USA, January 2009. ACM Press. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact