×

zbMATH — the first resource for mathematics

An extended account of contract monitoring strategies as patterns of communication. (English) Zbl 06913643
Summary: Contract systems have come to play a vital role in many aspects of software engineering. This has resulted in a wide variety of approaches to enforcing contracts – ranging from the straightforward pre-condition and post-condition checking of Eiffel to lazy, optional, and parallel enforcement strategies. Each of these approaches has its merits, but each has required ground-up development of an entire contract monitoring system. We present a unified approach to understanding this variety, while also opening the door to as-yet-undiscovered strategies. By observing that contracts are fundamentally about communication between a program and a monitor, we reframe contract checking as communication between concurrent processes. This brings out the underlying relations between widely studied enforcement strategies, including strict and lazy enforcement as well as concurrent approaches, including new contracts and strategies. We show how each of these can be embedded into a core calculus, and demonstrate a proof (via simulation) of correctness for one such encoding. Finally, we show that our approach suggests new monitoring approaches and contracts not previously expressible.
MSC:
68N18 Functional programming and lambda calculus
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ahmed, A., Findler, R. B., Siek, J. G. & Wadler, P. (2011) Blame for all. In Proceedings of the 38th Annual Symposium on Principles of Programming Languages, POPL ’11. ACM. · Zbl 1284.68156
[2] Ahmed, A., Jamner, D., Siek, J. G. & Wadler, P. (2017) Theorems for free for free: Parametricity, with and without types. In Proceedings of the 22th International Conference on Functional Programming, ICFP ’17. ACM.
[3] Ambler, A. L., Good, D. I., Browne, J. C., Burger, W. F., Choen, R. M., Hoch, C. G., & Wells, R. E. (1977) Gypsy: A language for specification and implementation of verifiable programs. In Proceedings of the ACM Conference on Language Design for Reliable Software, Sigplan, pp. 1-10.
[4] Barnett, M., Leino, K. R. M. & Schulte, W. (2005) The spec# programming system: An overview. In Proceedings of the 2004 International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS ’04. Springer-Verlag.
[5] Blume, M. & Mcallester, D. (2004) A sound (and complete) model of contracts. In Proceedings of the 9th International Conference on Functional Programming, ICFP ’04. ACM. · Zbl 1323.68353
[6] Chen, F. & Roşu, G. (2007) Mop: An efficient and generic runtime verification framework. In Proceedings of the 22nd Annual Conference on Object-Oriented Programming Systems and Applications, OOPSLA ’07. ACM.
[7] Chitil, O. (2012) Practical typed lazy contracts. In Proceedings of the 17th International Conference on Functional Programming, ICFP ’12. ACM. · Zbl 1291.68112
[8] Chitil, O., & Huch, F. (2006) A pattern logic for prompt lazy assertions in haskell. In Proceedings of the Symposium on Implementation and Application of Functional Languages, IFL ’06. Springer.
[9] Chitil, O., Mcneill, D. & Runciman, C. (2003) Lazy assertions. In Proceedings of the Symposium on Implementation and Application of Functional Languages, IFL ’03. Springer-Verlag. · Zbl 1108.68346
[10] Degen, M., Thiemann, P. & Wehr, S. (2009) True Lies: Lazy contracts for lazy languages (faithfulness is better than laziness) In Proceedings of the Arbeitstagung Programmiersprachen (ATPS), ATPS ’09. Springer.
[11] Degen, M.; Thiemann, P.; Wehr, S., Eager and delayed contract monitoring for call-by-value and call-by-name evaluation, J. Log. Algebr. Program., 79, 515-549, (2010) · Zbl 1204.68071
[12] Degen, M., Thiemann, P. & Wehr, S. (2012) The interaction of contracts and laziness. In Proceedings of the 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM ’12. ACM. · Zbl 1360.68325
[13] Dimoulas, C.; Felleisen, M., On contract satisfaction in a higher-order world, ACM Trans. Program. Lang. Syst., 33, 16:1-16:29, (2011)
[14] Dimoulas, C., Findler, R. B., Flanagan, C. & Felleisen, M. (2011) Correct blame for contracts: No more scapegoating. In Proceedings of the 38th Annual Symposium on Principles of Programming Languages, POPL ’11. ACM. · Zbl 1284.68176
[15] Dimoulas, C., Findler, R. B. & Felleisen, M. (2013) Option contracts. In Proceedings of the 2013 International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA ’13. ACM. · Zbl 1284.68176
[16] Dimoulas, C., Pucella, R. & Felleisen, M. (2009) Future contracts. In Proceedings of the 11th Conference on Principles and Practice of Declarative Programming, PPDP ’09. ACM.
[17] Dimoulas, C., Tobin-Hochstadt, S. & Felleisen, M. (2012) Complete monitors for behavioral contracts. In Proceedings of the European Symposium on Programming, ESOP ’12. Springer-Verlag. · Zbl 1352.68031
[18] Disney, T., Flanagan, C. & Mccarthy, J. (2011) Temporal higher-order contracts. In Proceedings of the 16th International Conference on Functional Programming, ICFP ’11. ACM. · Zbl 1323.68068
[19] Ergün, F., Kannan, S., Kumar, S. R., Rubinfeld, R. & Viswanathan, M. (1998) Spot-checkers. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing, STOC ’98. ACM. · Zbl 1027.68514
[20] Findler, R. B. (2014) Behavioral software contracts. In Proceedings of the 19th International Conference on Functional Programming, ICFP ’14. ACM.
[21] Findler, R. B. & Blume, M. (2006) Contracts as pairs of projections. In Proceedings of the 8th International Conference on Functional and Logic Programming, FLOPS ’06. Springer-Verlag. · Zbl 1185.68193
[22] Findler, R. B & Felleisen, M. (2002) Contracts for higher-order functions. In Proceedings of the 7th International Conference on Functional Programming, ICFP ’02. ACM. · Zbl 1322.68039
[23] Findler, R. B., Guo, S.-Y. & Rogers, A. (2008) Lazy contract checking for immutable data structures. In Proceedings of the Implementation and Application of Functional Languages. Springer-Verlag.
[24] Flanagan, C. (2006) Hybrid type checking. In Proceedings of the Conference Record of the 33rd Symposium on Principles of Programming Languages, POPL ’06. ACM. · Zbl 1370.68202
[25] Flatt, M. & . (2010) Reference: Racket. Technical Report, PLT-TR-2010-1. PLT Inc. http://racket-lang.org/tr1/.
[26] Freeman, Tim. (1994) Refinement Types for ML. (Ph.D. Thesis), Carnegie Mellon University.
[27] Friedman, D. & Wise, D. (1976) The Impact of Applicative Programming on Multiprocessing. Technical Report 52. Indiana University, Computer Science Department.
[28] Greenberg, M. (2015) Space-efficient manifest contracts. In Proceedings of the 42nd Symposium on Principles of Programming Languages, POPL ’15. ACM. · Zbl 1345.68054
[29] Greenberg, M., Pierce, B. C. & Weirich, S. (2010) Contracts made manifest. In Proceedings of the 37th Symposium on Principles of Programming Languages, POPL ’10. ACM. · Zbl 1312.68133
[30] Guha, A., Matthews, J., Findler, R. B. & Krishnamurthi, S. (2007) Relationally-parametric polymorphic contracts. In Proceedings of the 2007 Symposium on Dynamic Languages, DLS ’07. ACM.
[31] Havelund, K. & Rosu, G. (2001) Monitoring Java Programs with Java Pathexplorer. Technical Report, NASA Ames Research Center. · Zbl 1073.68549
[32] Herman, D., Tomb, A. & Flanagan, C (2007 April) Space-efficient gradual typing. In Trends in Functional Prog, Page XXVIII. TFP ’07. · Zbl 1232.68025
[33] Hickey, R. (2018) Clojure core.spec Documentation [online]. Accessed February 18, 2018. Available at: https://clojure.org/guides/spec.
[34] Hinze, R., Jeuring, J. & Löh, A. (2006) Typed contracts for functional programming. In Proceedings of the 8th International Conference on Functional and Logic Programming, FLOPS ’06. Springer-Verlag. · Zbl 1185.68195
[35] Ingerman, P. Z., Thunks: A way of compiling procedure statements with some comments on procedure declarations, Commun. ACM, 4, (1961) · Zbl 0098.10208
[36] Jeffrey, A., Higher Order Operational Techniques in Semantics, Semantics for core Concurrent ML using computation types, (1998), Cambridge University Press
[37] Keil, M. & Thiemann, P. (2015) Blame assignment for higher-order contracts with intersection and union. In Proceedings of the 20th International Conference on Functional Programming, ICFP ’15. ACM. · Zbl 1360.68365
[38] Meyer, B., Eiffel: The Language, (1992), Prentice-Hall, Inc. · Zbl 0779.68013
[39] Moore, S., Dimoulas, C., Findler, R. B., Flatt, M. & Chong, S. (2016) Extensible access control with authorization contracts. In Proceedings of the 2016 International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA ’16. ACM.
[40] Nguyen, P. C., Tobin-Hochstadt, S. & Van Horn, D. (2014) Soft contract verification. In Proceedings of the 19th International Conference on Functional Programming, ICFP ’14. ACM. · Zbl 1346.68062
[41] Ou, X., Tan, G., Mandelbaum, Y., & Walker, D. (2004) Dynamic typing with dependent types. Exploring New Frontiers of Theoretical Informatics, Levy, J.-J., Mayr, E. W., & Mitchell, J. C. (eds), Boston, MA: Springer, US, pp. 437-450. · Zbl 1088.68531
[42] Owens, Z. (2012) Contract monitoring as an effect. Proceedings of the 1st ACM SIGPLAN Workshop on Higher-Order Programming with Effects. HOPE ’12. ACM.
[43] Pierce, B. C., Types and Programming Languages, (2002), MIT Press
[44] Reppy, J. H. (1993) Concurrent ML: Design, application and semantics. In Proceedings of the Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992, McMaster University, Hamilton, Ontario, Canada. Springer-Verlag.
[45] Reppy, J. H., Concurrent Programming in ML, (1999), Cambridge University Press · Zbl 0900.68214
[46] Sekiyama, T., Nishida, Y. & Igarashi, A. (2015) Manifest contracts for datatypes. In Proceedings of the 42nd Symposium on Principles of Programming Languages, POPL ’15. ACM. · Zbl 1345.68072
[47] Shinnar, A. (2011) Safe and Effective Contracts. Technical Report, Harvard University.
[48] Siek, J. G. & Taha, W. (2006) Gradual typing for functional languages. Scheme and Functional Programming Workshop.
[49] Siek, J. G., Garcia, R. & Taha, W. (2009) Exploring the design space of higher-order casts. In Proceedings of the European Symposium on Programming, ESOP ’09. Springer-Verlag. · Zbl 1234.68060
[50] Strickland, T. S., Tobin-Hochstadt, S., Findler, R. B. & Flatt, M. (2012) Chaperones and impersonators: Run-time support for reasonable interposition. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’12. ACM.
[51] Swords, C., Sabry, A. & Tobin-Hochstadt, S. (2015) Expressing contract monitors as patterns of communication. In Proceedings of the 20th International Conference on Functional Programming, ICFP ’15. ACM. · Zbl 1360.68370
[52] Vitousek, M. M., Siek, J. G., Kent, A. & Baker, J. (2014) Design and evaluation of gradual typing for Python. In Proceedings of the Dynamic Languages Symposium, DLS ’14.
[53] Wadler, P. & Findler, R. B. (2009) Well-typed programs can’t be blamed. In Proceedings of the 18th European Symposium on Programming Languages and Systems. ESOP ’09. Springer-Verlag. · Zbl 1234.68063
[54] Xu, D. N., Peyton Jones, S. & Claessen, K. (2009) Static contract checking for haskell. In Proceedings of the 36th Annual Symposium on Principles of Programming Languages, POPL ’09. ACM. · Zbl 1315.68107
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.