{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T03:45:13Z","timestamp":1743133513030,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471686"},{"type":"electronic","value":"9783319471693"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_7","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T17:56:23Z","timestamp":1475603783000},"page":"80-96","source":"Crossref","is-referenced-by-count":3,"title":["Specifying and Verifying Advanced Control Features"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Naumann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hridesh","family":"Rajan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomoyuki","family":"Aotani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Ambler, A.L., Good, D.I., Browne, J.C., Burger, W.F., Choen, R.M., Hoch, C.G., Wells, R.E.: Gypsy: a language for specification and implementation of verifiable programs. In: Proceedings of the ACM Conference on Language Design for Reliable Software (1977)","DOI":"10.1145\/800022.808306"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Aotani, T., Leavens, G.T.: Towards modular reasoning for context-oriented programs. In: Formal Techniques for Java-like Programs, July 2016 (to appear)","DOI":"10.1145\/2955811.2955819"},{"key":"7_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics - for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W.: Program Logics - for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"issue":"2","key":"7_CR4","doi-asserted-by":"crossref","first-page":"4:1","DOI":"10.5381\/jot.2013.12.2.a4","volume":"12","author":"M Appeltauer","year":"2013","unstructured":"Appeltauer, M., Hirschfeld, R., Linckeb, J.: Declarative layer composition with the JCop programming language. J. Object Technol. 12(2), 4:1\u20134:37 (2013)","journal-title":"J. Object Technol."},{"key":"7_CR5","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R-J Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, New York (1998)"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Bagherzadeh, M., Leavens, G.T., Dyer, R.: Applying translucid contracts for modular reasoning about aspect andobject oriented events. In: 10th International Workshop on Foundations of Aspect-Oriented Languages (2011a)","DOI":"10.1145\/1960510.1960517"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Bagherzadeh, M., Rajan, H., Leavens, G.T., Mooney, S.: Translucid contracts: expressive specification and modularverification for aspect-oriented interfaces. In: 10th International Conference on Aspect-Oriented Software Development (2011b)","DOI":"10.1145\/1960275.1960293"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Bagherzadeh, M., Rajan, H., Darvish, A.: On exceptions, events and observer chains. In: 12th International Conference on Aspect-Oriented Software Development (2013)","DOI":"10.1145\/2451436.2451458"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Bagherzadeh, M., Dyer, R., Fernando, R.D., Sanchez, J., Rajan, H.: Modular reasoning in the presence of event subtyping. In: 14th International Conference on Modularity (2015)","DOI":"10.1145\/2724525.2724569"},{"issue":"3","key":"7_CR10","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/S0164-1212(02)00041-9","volume":"65","author":"M Barnett","year":"2003","unstructured":"Barnett, M., Schulte, W.: Runtime verification of.NET contracts. J. Syst. Softw. 65(3), 199\u2013208 (2003)","journal-title":"J. Syst. Softw."},{"key":"7_CR11","unstructured":"B\u00fcchi, M., Weck, W.: The greybox approach: when blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science (1999)"},{"issue":"1","key":"7_CR12","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF00264295","volume":"20","author":"W Damm","year":"1983","unstructured":"Damm, W., Josko, B.: A sound and relatively complete Hoare-logic for a language with higher type procedures. Acta Informatica 20(1), 59\u2013101 (1983)","journal-title":"Acta Informatica"},{"issue":"2","key":"7_CR13","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF00264436","volume":"18","author":"GW Ernst","year":"1982","unstructured":"Ernst, G.W., Navlakha, J.K., Ogden, W.F.: Verification of programs with procedure-type parameters. Acta Informatica 18(2), 149\u2013169 (1982)","journal-title":"Acta Informatica"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: ACM International Conference on Functional Programming (2002)","DOI":"10.1145\/581478.581484"},{"key":"7_CR15","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0019995","volume-title":"VDM \u201991 Formal Software Development Methods","author":"JV Guttag","year":"1991","unstructured":"Guttag, J.V., Horning, J.J.: A tutorial on Larch and LCL, a Larch\/C interface language. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 1\u201378. Springer, Heidelberg (1991). doi: 10.1007\/BFb0019995"},{"issue":"3","key":"7_CR17","doi-asserted-by":"crossref","first-page":"125","DOI":"10.5381\/jot.2008.7.3.a4","volume":"7","author":"R Hirschfeld","year":"2008","unstructured":"Hirschfeld, R., Costanza, P., Nierstrasz, O.: Context-oriented programming. J. Object Technol. 7(3), 125\u2013151 (2008)","journal-title":"J. Object Technol."},{"issue":"10","key":"7_CR18","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"7_CR19","volume-title":"Systematic Software Development Using VDM","author":"CB Jones","year":"1986","unstructured":"Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0053381","volume-title":"ECOOP\u201997 \u2014 Object-Oriented Programming","author":"G Kiczales","year":"1997","unstructured":"Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Ak\u015fit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220\u2013242. Springer, Heidelberg (1997). doi: 10.1007\/BFb0053381"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"ECOOP 2001 \u2014 Object-Oriented Programming","author":"G Kiczales","year":"2001","unstructured":"Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327\u2013354. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45337-7_18"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Aldrich, J., Birkedal, L., Svendsen, K., Buisse, A.: Design patterns in separation logic. In: International Workshop on Types in Languages Design and Implementation (2009)","DOI":"10.1145\/1481861.1481874"},{"issue":"10","key":"7_CR23","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u2018design by contract\u2019. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"7_CR24","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Upper Saddle River (1997)","edition":"2"},{"issue":"1","key":"7_CR25","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0167-6423(88)90062-7","volume":"11","author":"C Morgan","year":"1988","unstructured":"Morgan, C.: Procedures, parameters, abstraction: separate concerns. Sci. Comput. Program. 11(1), 17\u201327 (1988)","journal-title":"Sci. Comput. Program."},{"key":"7_CR26","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Hertfordshire (1994)","edition":"2"},{"key":"7_CR27","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0304-3975(94)00247-G","volume":"150","author":"DA Naumann","year":"1995","unstructured":"Naumann, D.A.: Predicate transformers and higher order programs. Theor. Comput. Sci. 150, 111\u2013159 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR28","unstructured":"Rajan, H., Leavens, G.T.: Quantified, typed events for improved separation of concerns. Technical Report 07-14c, Iowa State University, Department of Computer Science, October 2007. ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR07-14\/TR.pdf"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-540-70592-5_8","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"H Rajan","year":"2008","unstructured":"Rajan, H., Leavens, G.T.: Ptolemy: a language with quantified, typed events. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 155\u2013179. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-70592-5_8"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-00590-9_24","volume-title":"Programming Languages and Systems","author":"H Rajan","year":"2009","unstructured":"Rajan, H., Tao, J., Shaner, S., Leavens, G.T.: Tisa: a language design and modular verification technique for temporal policies in web services. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 333\u2013347. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00590-9_24"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, J., Leavens, G.T.: Reasoning tradeoffs in languages with enhanced modularity features. In: 15th International Conference on Modularity (2016)","DOI":"10.1145\/2889443.2889447"},{"key":"7_CR32","unstructured":"Shaner, S., Rajan, H., Leavens, G.T.: Model programs for preserving composite invariants. In: 7th International Workshop on Specification and Verification of Component-Based Systems, Technical report CS-TR-08-07, University of Central Florida (2008)"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Shaner, S.M., Leavens, G.T., Naumann, D.A.: Modular verification of higher-order methods with mandatory calls specified by model programs. In: International Conference on Object-Oriented Programming, Systems, Languages and Applications (2007)","DOI":"10.1145\/1297027.1297053"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-540-39993-3_15","volume-title":"From Object-Orientation to Formal Methods","author":"N Soundarajan","year":"2004","unstructured":"Soundarajan, N., Fridella, S.: Incremental reasoning for object oriented systems. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 302\u2013333. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-39993-3_15"},{"issue":"1","key":"7_CR35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/9758.10500","volume":"9","author":"JM Wing","year":"1987","unstructured":"Wing, J.M.: Writing Larch interface language specifications. ACM Trans. Prog. Lang. Syst. 9(1), 1\u201324 (1987)","journal-title":"ACM Trans. Prog. Lang. Syst."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T04:07:51Z","timestamp":1568434071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}