How to Use Objects: Code and Concepts (2016)

Part V: Appendix

Appendix B. Bibliography

[1] Martin Abadi and Luca Cardelli. A Theory of Objects. Monographs in Computer Science. Springer, 1996.

[2] Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey Ullman. Compilers: Principles, Techniques and Tools. Addison-Wesley, 2007.

[3] Bowen Alpern, Anthony Cocchi, Stephen Fink, and David Grove. Efficient implementation of Java interfaces: Invokeinterface considered harmless. In Proceedings of the 16th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA ‘01, pages 108–124, New York, NY, 2001. ACM.

[4] Bowen Alpern, Anthony Cocchi, David Grove, and Derek Lieber. Efficient dispatch of Java interface methods. In Proceedings of the 9th International Conference on High-Performance Computing and Networking, HPCN Europe 2001, pages 621–628, London, UK, 2001. Springer.

[5] Pierre America. Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, REX Workshop, volume 489 of Lecture Notes in Computer Science, pages 60–90. Springer, 1990.

[6] Gregory R. Andrews. Concurrent Programming: Principles and Practice. Addison-Wesley, 1991.

[7] Giulio Antoniol, Bruno Caprile, Alessandra Potrich, and Paolo Tonella. Design-code traceability for object-oriented systems. Annals of Software Engineering, 9(1-4):35–58, 2000.

[8] Apache. The Apache Hadoop library. http://hadoop.apache.org.

[9] Apache Struts. http://struts.apache.org/.

[10] Apache. Apache POI: The Java API for Microsoft documents. http://poi.apache.org, 2014.

[11] Apache. Apache Tomcat. http://tomcat.apache.org, 2015.

[12] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step C minor. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, volume 4732 of Lecture Notes in Computer Science. Springer, 2007.

[13] Apple. OS X frameworks. https://developer.apple.com/library/mac/documentation/MacOSX/Conceptual/OSX_Technology_Overview/SystemFrameworks/SystemFrameworks.html, 2015.

[14] Apple. What are frameworks? https://developer.apple.com/library/mac/documentation/MacOSX/Conceptual/BPFrameworks/Concepts/WhatAreFrameworks.html, 2015.

[15] Krysztof R. Apt and Ernst-Rüdiger Olderog. Verification of Sequential and Concurrent Programs. Springer, 2nd edition, 1997.

[16] Joe Armstrong, Robert Virding, Claes Wikstrom, and Mike Williams. Concurrent Programming in Erlang. Prentice Hall, 2nd edition, 1996.

[17] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, Cambridge, 1998.

[18] Ralph-Johan J. Back, Abo Akademi, and J. Von Wright. Refinement Calculus: A Systematic Introduction. Springer, Secaucus, NJ, 1998.

[19] David F. Bacon, Stephen J. Fink, and David Grove. Space- and time-efficient implementation of the Java object model. In Proceedings of the 16th European Conference on Object-Oriented Programming, ECOOP ‘02, pages 111–132, London, UK, 2002. Springer.

[20] Anindya Banerjee, David Naumann, and Stan Rosenberg. Regional logic for local reasoning about global invariants. In Jan Vitek, editor, ECOOP 2008—Object-Oriented Programming, volume 5142 of Lecture Notes in Computer Science, pages 387–411. Springer, 2008.

[21] Michael Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27–56, 2004.

[22] Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In 4th International Symposium on Formal Methods for Components and Objects, volume 4111 of Lecture Notes in Computer Science. Springer, 2006.

[23] Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean, editors, CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart Devices, volume 3362 of Lecture Notes in Computer Science, pages 49–69. Springer, 2005.

[24] Len Bass, Paul Clements, and Rick Kazman. Software Architecture in Practice. Addison-Wesley, 2nd edition, 2003.

[25] Florian Battke, Stephan Symons, and Kay Nieselt. Mayday: Integrative analytics for expression data. BMC Bioinformatics, 11(1), 2010.

[26] Fabian Beck and Stephan Diehl. On the congruence of modularity and code coupling. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ESEC/FSE ‘11, pages 354–364, New York, NY, 2011. ACM.

[27] Kent Beck. SmallTalk Best Practice Patterns. Prentice Hall, 1997.

[28] Kent Beck. Extreme Programming Explained: Embrace Change. Addison-Wesley, 1999.

[29] Kent Beck. Test Driven Development: By Example. Addison-Wesley, 2002.

[30] Kent Beck. JUnit Pocket Guide. O’Reilly, 2004.

[31] Kent Beck. Implementation Patterns. Addison-Wesley, 2007.

[32] Kent Beck and Ward Cunningham. A laboratory for teaching object-oriented thinking. SIGPLAN Notices, 24(10), October 1989.

[33] Kent Beck and Martin Fowler. Planning Extreme Programming. Addison-Wesley, 2001.

[34] Kent Beck and Erich Gamma. JUnit cookbook. http://junit.org, 2014.

[35] Jon Bentley. Programming pearls: Little languages. Communications of the ACM, 29(8):711–721, August 1986.

[36] Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O’Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. In CAV 2007, volume 4590 of Lecture Notes in Computer Science. Springer, 2007.

[37] Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, Formal Methods for Components and Objects, 4th International Symposium (FMCO), volume 4111 of Lecture Notes in Computer Science. Springer, 2005.

[38] Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. Symbolic execution with separation logic. In Kwangkeun Yi, editor, Programming Languages and Systems, Third Asian Symposium (APLAS), volume 3780 of Lecture Notes in Computer Science. Springer, 2005.

[39] James M. Bieman and Josephien Xia Zhao. Reuse through inheritance: A quantitative study of C++ software. In M. H. Samadzadeh and Mansour K. Zand, editors, Proceedings of the ACM SIGSOFT Symposium on Software Reusability (SSR’95), Seattle, WA, ACM SIGSOFT Software Engineering Notes, pages 47–52, August 1995.

[40] The BioJava project. http://www.biojava.org, 2014.

[41] bioKepler: A comprehensive bioinformatics scientific workflow module. http://www.biokepler.org, 2014.

[42] Richard Bird. Introduction to Functional Programming Using Haskell. Prentice Hall, 2nd edition, 1998.

[43] Dines Bjørner. TRain: The railway domain: A “grand challenge” for computing science and transportation engineering. In René Jacquart, editor, IFIP Congress Topical Sessions, pages 607–612. Kluwer, 2004.

[44] Joshua Bloch. Effective Java. Addison-Wesley, 2nd edition, 2006.

[45] Daniel G. Bobrow, Linda G. DeMichiel, Richard P. Gabriel, Sonya E. Keene, Gregor Kiczales, and David A. Moon. Common Lisp object system specification. SIGPLAN Notices, 23(SI):1–142, September 1988.

[46] Sascha Böhme and Michał Moskal. Heaps and data structures: A challenge for automated provers. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, 23nd International Conference on Automated Deduction (CADE 23), volume 6803 of Lecture Notes in Computer Science, pages 177–191. Springer, 2011.

[47] Grady Booch, Ivar Jacobson, and James Rumbaugh. The Unified Modeling Language User Guide. Addison-Wesley, 2nd edition, 2005.

[48] Grady Booch, Robert A. Maksimchuk, Michael W. Engle, Bobbi J. Young, Jim Conallen, and Kelli A. Houston. Object Oriented Design with Applications. Addison-Wesley, 3rd edition, 2007.

[49] Richard Bornat. Proving pointer programs in Hoare logic. In Mathematics of Program Construction, 2000.

[50] Tim Boudreau, Jaroslav Tulach, and Geertjan Wielenga. Rich Client Programming: Plugging into the Netbeans Platform. Prentice Hall, 2007.

[51] Ivan T. Bowman and Richard C. Holt. Software architecture recovery using Conway’s law. In Proceedings of the 1998 Conference of the Centre for Advanced Studies on Collaborative Research. IBM Press, 1998.

[52] Gilad Bracha. Generics in the Java programming language. Tutorial, http://www.oracle.com/technetwork/java/index.html, March 2004.

[53] Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Making the future safe for the past: Adding genericity to the Java programming language. In Craig Chambers, editor, ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), pages 183–200, Vancouver, BC, 1998.

[54] Frederick P. Brooks. The Mythical Man-Month: Essays on Software Engineering, Anniversary Edition. Addison-Wesley, 2001.

[55] Timothy A. Budd. Object-Oriented Programming. Addison-Wesley, 1991.

[56] Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. Software Tools for Technology Transfer, 7(3):212–232, June 2005.

[57] Michael G. Burke, Kathleen Knobe, Ryan Newton, and Vivek Sarkar. The Concurrent Collections Programming Model. Technical Report TR 10–12, Department of Computer Science, Rice University, Houston, TX, December 2010.

[58] R. M. Burstall. Some techniques for proving correctness of programs which alter data stuctures. In B. Meltzer and D. Michie, editors, Machine Intelligence 7. Edinburgh University Press, 1972.

[59] Frank Buschmann, Regine Meunier, Hans Rohnert, Peter Sommerlad, and Michael Stal. Pattern-Oriented Software Architecture: A System of Patterns, volume 1. Wiley & Sons, 1996.

[60] Giuseppe Castagna. Covariance and contravariance: Conflict without a cause. ACM Transactions on Programming Languages and Systems, 17(3):431–447, May 1995.

[61] Raymond Chen. Why is the function SHStripMneumonic misspelled? http://blogs.msdn.com/b/oldnewthing/archive/2008/05/19/8518565.aspx, 2008.

[62] Yoonsik Cheon, Gary Leavens, Murali Sitaraman, and Stephen Edwards. Model variables: Cleanly supporting abstraction in design by contract: Research articles. Software: Practice and Experience, 35(6):583–599, May 2005.

[63] Keith L. Clark and Sten-Ake Tärnlund, editors. Logic Programming. Academic Press, London, UK, 1982.

[64] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.

[65] Eric Clayberg and Dan Rubel. Eclipse Plug-ins. Addison-Wesley, 3rd edition, 2009.

[66] Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. VCC: A practical system for verifying concurrent C. In Theorem Proving in Higher Order Logics, 22nd International Conference (TPHOLs), volume 5674 of Lecture Notes in Computer Science. Springer, 2009.

[67] Ernie Cohen, Michał Moskal, Wolfram Schulte, and Stephan Tobies. A precise yet efficient memory model for C. In 4th International Workshop on Systems Software Verification (SSV 2009), ENTCS. Elsevier Science B.V., 2009.

[68] Melvin Conway. How do committees invent? Datamation, 14:28–31, 1968.

[69] William R. Cook, Walter L. Hill, and Peter S. Canning. Inheritance is not subtyping. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 125–135, San Francisco, CA, 1989. ACM.

[70] James Coplien, Daniel Hoffman, and David Weiss. Commonality and variability in software engineering. IEEE Software, pages 37–45, November 1998.

[71] James O. Coplien. Multi-Paradigm Design for C++. Addison-Wesley, 1998.

[72] Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms. MIT Press, Cambridge, MA, 1990.

[73] Ádám Darvas and K. Rustan M. Leino. Practical reasoning about invocations and implementations of pure methods. In Matthew B. Dwyer and Antónia Lopes, editors, FASE, volume 4422 of Lecture Notes in Computer Science, pages 336–351. Springer, 2007.

[74] Ádám Darvas and Peter Müller. Reasoning about method calls in interface specifications. Journal of Object Technology, 5(5):59–85, June 2006.

[75] Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pages 337–340. Springer, 2008.

[76] David Detlefs, Greg Nelson, and James B. Saxe. Simplify: A theorem prover for program checking. Journal of the ACM, 52:365–473, May 2005.

[77] Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18:453–457, August 1975.

[78] Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976.

[79] Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. A local shape analysis based on separation logic. In Holger Hermanns and Jens Palsberg, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3920 of Lecture Notes in Computer Science, pages 287–302. Springer, 2006.

[80] Robert Eckstein, Marc Loy, and Dave Wood. Swing. O’Reilly, Sebostopol, CA, 2nd edition, 2002.

[81] Performance bloopers. http://wiki.eclipse.org/Performance_Bloopers, 2009.

[82] Eclipse. The EclipseLink project. http://www.eclipse.org/eclipselink/, 2013.

[83] Eclipse SWTBot. http://eclipse.org/swtbot/, 2014.

[84] Eclipse. SWT snippets. http://www.eclipse.org/swt/snippets, 2015.

[85] ECMA. ECMAScript language specification: Edition 5.1, 2011. http://www.ecmainternational.org/publications/standards/Ecma-262.htm.

[86] Ramez Elmasri and Shamkant B. Navathe. Fundamentals of Database Systems. Benjamin/Cummings, 2000.

[87] ESA. Ariane 5: Flight 501 failure. http://esamultimedia.esa.int/docs/esa-x-1819eng.pdf, July 1996.

[88] J.-C. Filliâtre. WHY: A Multi-language Multi-prover Verification Tool. Research Report 1366, LRI, Université Paris Sud, March 2003.

[89] Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Programming Language Design and Implementation, PLDI 2002, 2002.

[90] Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19–32, Providence, RI, 1967. American Mathematical Society.

[91] Internet Engineering Task Force. Rfc 1122: Requirements for Internet hosts—communication layers. http://tools.ietf.org/html/rfc1122, October 1989.

[92] Martin Fowler. Refactoring: Improving the Design of Existing Code. Addison-Wesley, 2000.

[93] Martin Fowler. Reducing coupling. IEEE Software, 18(4):102–104, July 2001.

[94] Martin Fowler. Patterns of Enterprise Application Architecture. Addison-Wesley, 2002.

[95] Martin Fowler. UML Distilled: Applying the Standard Object Modeling Language. Addison-Wesley, 3rd edition, 2004.

[96] Gottlob Frege. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von Louis Nebert, Halle, 1879.

[97] Garry Froehlich, H. James Hoover, Ling Liu, and Paul Sorenson. Designing object-oriented frameworks. In Saba Zamir, editor, Handbook of Object Technology, pages 491–501. CRC Press, 1998.

[98] Eric Gamma. The Extension Objects pattern. In Robert C. Martin, Dirk Riehle, and Frank Buschmann, editors, Pattern Languages of Program Design 3. Addison-Wesley, MA, 1997.

[99] Erich Gamma and Kent Beck. Contributing to Eclipse: Principles, Patterns, and Plugins. Addison-Wesley, 2004.

[100] Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995.

[101] David Garlan and Mary Shaw. An Introduction to Software Architecture. Technical Report CMU-CS-94-166, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 1994.

[102] Holger Gast. Lightweight separation. In O. Ait Mohamed, C. Muñoz, and S. Tahar, editors, Theorem Proving in Higher Order Logics 21st International Conference (TPHOLs 2008), volume 5170 of Lecture Notes in Computer Science. Springer, 2008.

[103] Holger Gast. Reasoning about memory layouts. Formal Methods in System Design, 37(2-3):141–170, 2010.

[104] Holger Gast. Developer-oriented correctness proofs: A case study of Cheney’s algorithm. In Shengchao Qin and Zongyan Qiu, editors, Proceedings of 13th International Conference on Formal Engineering Methods (ICFEM 2011), volume 6991 of Lecture Notes in Computer Science. Springer, 2011.

[105] Holger Gast. Structuring interactive correctness proofs by formalizing coding idioms. In Jörg Brauer, Marco Roveri, and Hendrik Tews, editors, 6th International Workshop on Systems Software Verification, (SSV 2011), volume 24 of OpenAccess Series in Informatics. Schloss Dagstuhl: Leibniz-Zentrum für Informatik, 2011.

[106] Holger Gast. Functional Software Verification by Symbolic Execution in Classical Logic. Habilitationsschrift. Mathematisch-Naturwissenschaftliche Fakultät, Universität Tübingen, Tübingen, Germany, 2012.

[107] Holger Gast. Semi-automatic proofs about object graphs in separation logic. In Stephan Merz and Gerald Lüttgen, editors, Automated Verification of Critical Systems, AVoCS ‘12, 2012.

[108] Carlo Ghezzi and Dino Mandrioli. Incremental parsing. ACM Transactions in Programming Languages and Systems, 1(1):58–70, 1979.

[109] Adele Goldberg and David Robson. Smalltalk-80: The Language and Its Implementation. Addison-Wesley, 1983.

[110] Michael J.C. Gordon. Mechanizing programming logics in higher order logic. In Current Trends in Hardware Verification and Automated Theorem Proving, pages 387–439. Springer, 1989.

[111] James Gosling, Bill Joy, Guy Steele, Gilad Bracha, and Alex Buckley. The Java Language Specification: Java SE 7 Edition. Addison-Wesley, 2013. http://docs.oracle.com/javase/specs/.

[112] Mark Grechanik, Collin McMillan, Luca DeFerrari, Marco Comi, Stefano Crespi, Denys Poshyvanyk, Chen Fu, Qing Xie, and Carlo Ghezzi. An empirical investigation into a large-scale Java open source code repository. In Proceedings of the 2010 ACM-IEEE International Symposium on Empirical Software Engineering and Measurement, ESEM ‘10, pages 11:1–11:10, New York, NY, 2010. ACM.

[113] Philipp Haller and Martin Odersky. Event-based programming without inversion of control. In Proceedings of the 7th Joint Conference on Modular Programming Languages, JMLC’06, pages 4–22, Heidelberg, Germany, 2006. Springer.

[114] Morten Borup Harning. An approach to structured display design: Coping with conceptual complexity. In Jean Vanderdonckt, editor, CADUI, pages 121–140. Presses Universitaires de Namur, 1996.

[115] John L. Hennessey and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Francisco, CA, 2nd edition, 1996.

[116] Joel Henry and Donald Gotterbarn. Coupling and cohesion in object-oriented design and coding. In Proceedings of the 1996 ACM 24th Annual Conference on Computer Science, CSC ‘96, page 149, New York, NY, 1996. ACM.

[117] James Henstridge. GIMP Python documentation. http://www.gimp.org/docs/python, September 2014.

[118] Frederick Herzberg, Bernard Mausner, and Barbara B. Snyderman. The Motivation to Work. Wiley, New York, NY, 2nd edition, 1959.

[119] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580,583, October 1969.

[120] Gerard J. Holzmann. The model checker SPIN. IEEE Transactions in Software Engineering, 23(5):279–295, May 1997.

[121] Peter V. Homeier and David F. Martin. Mechanical verification of mutually recursive procedures. In Proceedings of the 13th International Conference on Automated Deduction, CADE-13, pages 201–215, London, UK, 1996. Springer.

[122] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 2nd edition, 2003.

[123] Daniel H. H. Ingalls. Design principles behind Smalltalk. BYTE Magazine, 6(8), August 1981.

[124] Bart Jacobs and Frank Piessens. Verification of programs using inspector methods. In E. Zucca and D. Ancona, editors, Proceedings of the Eighth Workshop on Formal Techniques for Java-like Programs, pages 1–22, 2006.

[125] Bart Jacobs, Jan Smans, and Frank Piessens. A quick tour of the VeriFast program verifier. In Proceedings of the Eighth ASIAN Symposium on Programming Languages and Systems, APLAS 2010, 2010.

[126] Bart Jacobs, Jan Smans, and Frank Piessens. VeriFast: Imperative programs as proofs. In VS-Tools Workshop at VSTTE 2010. (No formal proceedings), 2010.

[127] java.net. Project JAXB. https://jaxb.java.net, 2013.

[128] JBoss. Hibernate: Getting started guide (version 4.3). http://docs.jboss.org/hibernate/core/4.3/quickstart/en-US/html/, 2014.

[129] JBoss. Hibernate: Relational persistence for idiomatic Java. http://www.hibernate.org/orm/documentation/5.0/, 2013.

[130] Ralph E. Johnson. How to design frameworks. Tutorial Notes OOPSLA, 1993.

[131] Ralph E. Johnson. Components, frameworks, patterns (extended abstract). In Proceedings of the 1997 Symposium on Software Reusability, pages 10–17, Boston, MA, 1997. ACM.

[132] Ralph E. Johnson and Brian Foote. Designing reusable classes. Journal of Object-Oriented Programming, 1(2):22–35, 1988.

[133] Richard Jones and Rafael Lins. Garbage Collection: Algorithms for Automatic Dynamic Memory Management. Wiley & Sons, 1996.

[134] Ioannis T. Kassios. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM, 2006: Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 268–283. Springer, 2006.

[135] Richard Kelsey and Jonathan Rees. A tractable scheme implementation. Lisp and Symbolic Computation, 7(1):315–335, 1994.

[136] Gregor Kiczales and John Lamping. Issues in the design and specification of class libraries. In Conference Proceedings on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA ‘92, pages 435–451, New York, NY, 1992. ACM.

[137] Gavin King, Pete Muir, Jozef Hartinger, Dan Allen, David Allen, Nicola Benaglia, Gladys Guerrero, Eun-Ju Ki, Terry Chuang, Francesco Milesi, and Sean Wu. CDI: Contexts and dependency injection for the Java EE platform.http://docs.jboss.org/weld/reference/latest/en-US/html/, April 2014.

[138] Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. Communications of the ACM (CACM), 53(6):107–115, June 2010.

[139] Donald E. Knuth. Notes on the van Emde Boas construction of priority deques: an instructive use of recursion, March 1977. Classroom notes, Stanford University, Stanford, CA; see http://www-cs-faculty.stanford.edu/~uno/faq.html.

[140] Donald E. Knuth. Structured programming with go to statements. In Edward Nash Yourdon, editor, Classics in Software Engineering, pages 257–321. Yourdon Press, Upper Saddle River, NJ, 1979.

[141] Donald E. Knuth. Literate programming. Computer Journal, 27(2):97–111, May 1984.

[142] Donald E. Knuth. The TEXbook. Addison-Wesley, 1986.

[143] Donald E. Knuth. The Art of Computer Programming, Volume 2: Seminumerical Algorithms. Addison-Wesley, 3rd edition, 1997.

[144] Andrew Koenig and Barbara E. Moo. Accelerated C++: Practical Programming by Example. Addison-Wesley, 2000.

[145] Keith Kowalczykowski, Kian Win Ong, Kevin Keliang Zhao, Alin Deutsch, Yannis Papakonstantinou, and Michalis Petropoulos. Do-it-yourself data driven web applications. In Fourth Biennial Conference on Innovative Data Systems Research, CIDR 2009. http://www.cidrdb.org/, 2009.

[146] Glenn E. Krasner and Stephen T. Pope. A cookbook for using the model-view controller user interface paradigm in Smalltalk-80. Journal of Object Oriented Programming, 1(3):26–49, August 1988.

[147] Philippe Kruchten. The Rational Unified Process: An Introduction. Addison-Wesley, 3rd edition, 2003.

[148] Doug Lea. Concurrent Programming in Java: Design Principles and Patterns. Addison-Wesley, 2nd edition, 1999.

[149] Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and William Harvey, editors, Behavioural Specifications for Business and Systems. Kluwer, 1999.

[150] Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. SIGSOFT Software Engineering Notes, 31(3):1–38, 2006.

[151] Gary T. Leavens and Yoonsik Cheon. Design by contract with JML. http://www.jmlspecs.org/jmldbc.pdf, January 2006.

[152] Gary T. Leavens, K. Rustan M. Leino, and Peter Müller. Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing, 19(2):159–189, 2007.

[153] Dirk Leinenbach and Thomas Santen. Verifying the Microsoft Hyper-V hypervisor with VCC. In Ana Cavalcanti and Dennis Dams, editors, FM 2009: Formal Methods, volume 5850 of Lecture Notes in Computer Science, pages 806–809. Springer, 2009.

[154] K. Rustan M. Leino and Peter Müller. A verification methodology for model fields. In Peter Sestoft, editor, European Symposium on Programming, volume 3924 of Lecture Notes in Computer Science, pages 115–130. Springer, 2006.

[155] K. Rustan M. Leino and G. Nelson. Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems, 24(5), 2002.

[156] T. C. Lethbridge, J. Singer, and A. Forward. How software engineers use documentation: The state of the practice. Software, IEEE, 20(6):35–39, 2003.

[157] Nancy G. Leveson and Clark S. Tyler. An investigation of the Therac-25 accidents. IEEE Computer, 26(7):18–41, 1993.

[158] Karl J. Lieberherr and I. Holland. Assuring good style for object-oriented programs. IEEE Software, pages 38–48, September 1989.

[159] Tim Lindholm, Frank Yellin, Gilad Bracha, and Alex Buckley. The Java Virtual Machine Specification, Java SE 7 Edition. Addison-Wesley, 2013.

[160] Barabara Liskov. Data abstraction and hierarchy. ACM SIGPLAN Notices, 23(5):17–34, 1988.

[161] Barbara H. Liskov. CLU Reference Manual. Number 114 in Lecture Notes in Computer Science. Springer, 1981.

[162] Barbara H. Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(6):1811–1841, November 1994.

[163] Tim Mackinnon, Steve Freeman, and Philip Craig. Endo-testing: Unit testing with mock objects. In Giancarlo Succi and Michele Marchesi, editors, Extreme Programming Examined, pages 287–301. Addison-Wesley, 2001.

[164] David Maier and David S. Warren. Computing with Logic: Logic Programming with Prolog. Benjamin/Cummings, Menlo Park, CA, 1988.

[165] Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, NY, 1992.

[166] Jeremy Manson, William Pugh, and Sarita V. Adve. The Java memory model. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ‘05, pages 378–391, New York, NY, 2005. ACM.

[167] Claude Marché and Christine Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 179–194. Springer, 2005.

[168] Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Formal verification of the heap manager of an operating system using separation logic. In Zhiming Liu and Jifeng He, editors, 8th International Conference on Formal Engineering Methods (ICFEM), volume 4260 of Lecture Notes in Computer Science. Springer, 2006.

[169] Robert C. Martin. Design principles and patterns. http://www.objectmentor.com/resources/articles/Principles_and_Patterns.pdf, 2000.

[170] Robert C. Martin. Agile Software Development: Principles, Patterns, and Practices. Prenctice Hall, 2002.

[171] Robert C. Martin. Professionalism and test-driven development. IEEE Software, 24(3):32–36, May 2007.

[172] Robert C. Martin. Clean Code. Prentice Hall, 2009.

[173] Apache Maven project. http://maven.apache.org/, 2014.

[174] Jeff McAffer, Jean-Michel Lemieux, and Chris Aniszcyk. Eclipse Rich Client Platform. Addison-Wesley, 2010.

[175] Jeff McAffer, Paul VanderLei, and Simon Archer. Equinox and OSGi: The Power Behind Eclipse. Addison-Wesley, 2009.

[176] Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. In F. Baader, editor, Automated Deduction: CADE-19, 19th International Conference on Automated Deduction, volume 2741 of Lecture Notes in Computer Science, pages 121–135. Springer, 2003.

[177] Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. Information and Computing, 199(1–2):200–227, 2005.

[178] Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, pages 124–144, New York, NY, 1991. Springer.

[179] Marjan Mernik, Jan Heering, and Anthony M. Sloane. When and how to develop domain-specific languages. ACM Computing Surveys, 37(4):316–344, December 2005.

[180] Bertrand Meyer. Eiffel: The Language. Prentice Hall, 1992.

[181] Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, 1997.

[182] Betrand Meyer. Applying “design by contract”. IEEE Computer, 25(10):40–51, October 1992.

[183] Scott Meyers. Effective C++: 55 Specific Ways to Improve Your Programs and Designs. Addison-Wesley, 3rd edition, 2005.

[184] Microsoft. .NET compiler platform (“Roslyn”). https://github.com/dotnet/roslyn, 2015.

[185] Leonid Mikhajlov and Emil Sekerinski. A study of the fragile base class problem. In Eric Jul, editor, ECOOP’98—Object-Oriented Programming, 12th European Conference, volume 1445 of Lecture Notes in Computer Science, pages 355–382. Springer, 1998.

[186] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

[187] P. Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of Lecture Notes in Computer Science. Springer, 2002.

[188] Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular specification of frame properties in JML. Concurrency and Computation: Practice and Experience, 15(2):117–154, 2003.

[189] Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, 2001.

[190] Java Source Net. Open source parser generators in Java. http://java-source.net/open-source/parser-generators, 2013.

[191] Tobias Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171–186, 1998.

[192] Tobias Nipkow and Gerwin Klein. Concrete Semantics: A Proof Assistant Approach. Springer, 2014.

[193] James Noble, Jan Vitek, and John Potter. Flexible alias protection. In Eric Jul, editor, ECOOP’98–Object-Oriented Programming, 12th European Conference, volume 1445 of Lecture Notes in Computer Science, pages 158–185. Springer, 1998.

[194] Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala. Artima, Walnut Creek, CA, 2nd edition, 2010.

[195] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic, number 2142 in Lecture Notes in Computer Science, pages 1–19. Springer, 2001.

[196] Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999.

[197] Kenneth Ölwing. How to correctly and uniformly use progress monitors. https://www.eclipse.org/articles/Article-Progress-Monitors/article.html, January 2006.

[198] OMG. OMG unified modeling language, superstructure: Version 2.4.1. Technical report, Object Management Group (OMG), August 2011. http://www.omg.org/spec/UML/2.4.1/Superstructure/PDF.

[199] Oracle. Java SE 6 hotspot virtual machine garbage collection tuning. http://www.oracle.com/technetwork/java/javase/gc-tuning-6-140523.html, 2006.

[200] Oracle. Expression Language specification, version 3.0. http://java.net/projects/el-spec/, 2013.

[201] Oracle. The Java EE 7 Tutorial, September 2013. http://docs.oracle.com/javaee/7/tutorial/.

[202] Oracle. JavaBeans spec. http://www.oracle.com/technetwork/java/javase/documentation/spec-136004.html, October 30, 2013.

[203] OSGi website. http://www.osgi.org, 2014.

[204] Susan Owicki and David Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319–340, 1976.

[205] D. L. Parnas. On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12):1053–1059, December 1972.

[206] Terence Parr. The Definitive ANTLR Reference: Building Domain-Specific Languages. Pragmatic Bookshelf, 2007.

[207] Frank Penczek, Wei Cheng, Clemens Grelck, Raimund Kirner, Bernd Scheuermann, and Alex Shafarenko. A data-flow based coordination approach to concurrent software engineering. In Data-Flow Execution Models for Extreme Scale Computing, DFM 2012, pages 36–43, September 2012.

[208] Alan J. Perlis. Epigrams on programming. ACM SIGPLAN Notices, 12:7–13, September 1982.

[209] Benjamin C. Pierce. Types and Programming Languages. MIT Press, Cambridge, MA, 2002.

[210] Ed Post. Real programmers don’t use Pascal. Datamation, 29(7), 1983.

[211] Trygve Reenskaug, Per Wold, and Odd Arild Lehne. Working with Objects: the OORAM Software Engineering Method. Manning Publications, 1995.

[212] John H. Reppy. Concurrent Programming in ML. Cambridge University Press, 1999.

[213] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 02, 2002.

[214] Dan Rubel, Jaime Wren, and Eric Clayberg. The Eclipse Graphical Editing Framework (GEF). Addison-Wesley, 2012.

[215] S3C. Document object model. http://www.w3.org/DOM/, 2009.

[216] Stephen R. Schach. Object-Oriented and Classical Software Engineering. McGrawHill, 8th edition, 2010.

[217] Norbert Schirmer. Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universität München, Munich, Germany, 2005.

[218] Douglas Schmidt, Michael Stal, Hans Rohnert, and Frank Buschmann. Pattern-oriented Software Architecture: Patterns for Concurrent and Networked Objects. Wiley & Sons, 2000.

[219] Klaus Schneider. Verification of Reactive Systems: Formal Methods and Algorithms. Springer, 2004.

[220] Arne Schramm, André Preußner, Matthias Heinrich, and Lars Vogel. Rapid UI development for enterprise applications: Combining manual and model-driven techniques. In Proceedings of the 13th International Conference on Model Driven Engineering Languages and Systems (MODELS’10). Springer, 2010.

[221] Ken Schwaber and Jeff Sutherland. The Scrum guide: The definitive guide to Scrum: The rules of the game. http://www.scrumguides.org/, July 2013.

[222] Chris Sells and Ian Griffiths. Programming WPF. O’Reilly, 2007.

[223] Coupling and cohesion. http://c2.com/cgi/wiki?CouplingAndCohesion, 2014.

[224] Law of Demeter revisited. http://c2.com/cgi/wiki?LawOfDemeterRevisited, 2014.

[225] Shield pattern. http://c2.com/cgi/wiki?ShieldPattern, 2014.

[226] Singletons are evil. http://c2.com/cgi/wiki?SingletonsAreEvil, 2014.

[227] Stamp coupling. http://c2.com/cgi/wiki?StampCoupling, 2014.

[228] You aren’t gonna need it. http://c2.com/cgi/wiki?YouArentGonnaNeedIt, 2014.

[229] Ben Shneiderman and Catherine Plaisant. Designing the User Interface: Strategies for Effective Human–Computer Interaction. Addison-Wesley, 2009.

[230] Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In Proceedings of the 23rd European Conference on ECOOP 2009: Object-Oriented Programming, Genoa, pages 148–172. Springer, 2009.

[231] Jim Smith and Ravi Nair. Virtual Machines: Versatile Platforms for Systems and Processes. Morgan Kaufmann, San Francisco, CA, 2005.

[232] Alan Snyder. Encapsulation and inheritance in object-oriented programming languages. In OOPLSA ‘86 Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications, pages 38–45, New York, NY, 1986. ACM.

[233] Ian Sommerville. Software Engineering. Addison-Wesley, 2010.

[234] Simon St. Laurent, Edd Dumbill, and Eric J Gruber. Learning Rails 3. O’Reilly, 2012.

[235] Dave Steinberg. EMF: Eclipse Modeling Framework. Addison-Wesley, 2nd edition, 2008.

[236] W. P. Stevens, G. J. Myers, and L. L. Constantine. Structured design. IBM Systems Journal, 13(2), 1974.

[237] W. Richard Stevens. UNIX Network Programming. Prentice Hall, 1990.

[238] W. Richard Stevens. Advanced Programming in the UNIX Environment. Addison-Wesley, 1992.

[239] Bjarne Stroustrup. The C++ Programming Language. Addison-Wesley, 3rd edition, 1997.

[240] Bjarne Stroustrup. Exception safety: Concepts and techniques. In Alexander B. Romanovsky, Christophe Dony, Jørgen Lindskov Knudsen, and Anand Tripathi, editors, Advances in Exception Handling Techniques, volume 2022 of Lecture Notes in Computer Science, pages 60–76. Springer, 2000.

[241] Sun. Java code conventions. http://www.oracle.com/technetwork/java/codeconventions-150003.pdf, April 1999.

[242] Richard E. Sweet. The Mesa programming environment. In Proceedings of the ACM SIGPLAN 85 Symposium on Language Issues in Programming Environments, SLIPE ‘85, pages 216–229, New York, NY, 1985. ACM.

[243] Clemens Szypersky, Dominik Gruntz, and Stephan Murer. Component Software. Addison-Wesley/ACM Press, 2nd edition, 2002.

[244] Taligent. Building object-oriented frameworks. http://lhcb-comp.web.cern.ch/lhcb-comp/Components/postscript/buildingoo.pdf, 1997.

[245] Simon Thompson. Haskell: The Craft of Functional Programming. Addison-Wesley, 2nd edition, 1999.

[246] Harvey Tuch, Gerwin Klein, and Michael Norrish. Types, bytes, and separation logic. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ‘07, 2007.

[247] Thomas Tuerk. A formalisation of Smallfoot in HOL. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference (TPHOLs), volume 5674 of Lecture Notes in Computer Science. Springer, 2009.

[248] Tycho: Building Eclipse plug-ins with Maven. http://www.eclipse.org/tycho/, 2014.

[249] Arie van Deursen, Paul Klint, and Joost Visser. Domain-specific languages: An annotated bibliography. SIGPLAN Notices, 35(6):26–36, June 2000.

[250] Hibernate ORM. http://hibernate.org/.

[251] Jsr-000299 web beans. https://jcp.org/aboutJava/communityprocess/final/jsr299/index.html, December 2009.

[252] The spring framework. http://spring.io/, 2014.

[253] David von Oheimb. Hoare logic for mutual recursion and local variables. In C. Pandu Rangan, V. Raman, and R. Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1738 of Lecture Notes in Computer Science, pages 168–180. Springer, 1999.

[254] David von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience, 13(13):1173–1214, 2001.

[255] W3C. XSL Transformations (XSLT) version 2.0. http://www.w3.org/TR/xslt20/.

[256] W3C. Document object model events. http://www.w3.org/TR/DOM-Level-2-Events/events.html, 2000.

[257] Tim A. Wagner and Susan L. Graham. Incremental analysis of real programming languages. In Proceedings of the ACM SIGPLAN 1997 Conference on Programming Language Design and Implementation, PLDI ‘97, pages 31–43, New York, NY, 1997. ACM.

[258] Gerald M. Weinberg. The Psychology of Computer Programming. Van Nostrand Reinhold Company, New York, NY, 1971.

[259] Frank White. The Overview Effect: Space Exploration and Human Evolution. American Institute of Aeronautics and Astronautics, Reston, VA, 2nd edition, 1998.

[260] Mats Wirén. Interactive incremental chart parsing. In Proceedings of the Fourth Conference on European Chapter of the Association for Computational Linguistics, pages 241–248, Manchester, UK, 1989.

[261] Rebecca Wirfs-Brock. Characterizing classes. IEEE Software, 23(2):9–11, 2006.

[262] Rebecca Wirfs-Brock. A tour of responsibility-driven design. Tutorial at International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006, Portland, OR, 2006.

[263] Rebecca Wirfs-Brock and Alan McKean. Object Design: Roles, Responsibilities, Collaborations. Addison-Wesley, 2003.

[264] Rebecca Wirfs-Brock and Brian Wilkerson. Object-oriented design: A responsibility-driven approach. In OOPSLA ‘89 Conference Proceedings, pages 71–75, 1989.

[265] Xerox. AspectJ: Crosscutting objects for better modularity. http://www.eclipse.org/aspectj, 2013.

[266] Fan Yang, Nitin Gupta, Chavdar Botev, Elizabeth F. Churchill, George Levchenko, and Jayavel Shanmugasundaram. WYSIWYG development of data driven web applications. Proceedings of the 34th International Conference on Very Large Data Bases (VLDB), 1(1), 2008.

[267] Zend_Db_Select from the Zend framework. http://framework.zend.com/manual/1.12/en/zend.db.select.html, 2014.

[268] The Zend framwork. http://framework.zend.com/, 2014.

[269] ZEST. Zest: The Eclipse visualization toolkit. http://www.eclipse.org/gef/zest/, 2013.