Abstract
Advances in programming often revolve around key design patterns, which programming languages embody as new control features. These control features, such as higher-order functions, advice, and context dependence, use indirection to decrease coupling and enhance modularity. However, this indirection makes them difficult to verify, because it hides actions (and their effects) behind an abstraction barrier. Such abstraction barriers can be overcome in a modular way using greybox specification techniques, provided the programming language supports interfaces as a place to record specifications. These techniques have previously allowed specification and modular verification of higher-order functional and object-oriented programs, as well as aspect-oriented and context-oriented programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This copying can be used repeatedly if the model program contains recursive calls. In general the substitution of actuals for formals may need to rename locals to avoid capture.
- 2.
Which handlers are invoked is implicit in implicit invocation languages, but where they are invoked from is evident in the source code. See Sanchez and Leavens’s paper [31] for a general discussion of the reasoning tradeoffs involved.
- 3.
See http://web.cs.iastate.edu/~ptolemy/ for details about PtolemyJ.
References
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)
Aotani, T., Leavens, G.T.: Towards modular reasoning for context-oriented programs. In: Formal Techniques for Java-like Programs, July 2016 (to appear)
Appel, A.W.: Program Logics - for Certified Compilers. Cambridge University Press, Cambridge (2014)
Appeltauer, M., Hirschfeld, R., Linckeb, J.: Declarative layer composition with the JCop programming language. J. Object Technol. 12(2), 4:1–4:37 (2013)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, New York (1998)
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)
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)
Bagherzadeh, M., Rajan, H., Darvish, A.: On exceptions, events and observer chains. In: 12th International Conference on Aspect-Oriented Software Development (2013)
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)
Barnett, M., Schulte, W.: Runtime verification of.NET contracts. J. Syst. Softw. 65(3), 199–208 (2003)
Büchi, M., Weck, W.: The greybox approach: when blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science (1999)
Damm, W., Josko, B.: A sound and relatively complete Hoare-logic for a language with higher type procedures. Acta Informatica 20(1), 59–101 (1983)
Ernst, G.W., Navlakha, J.K., Ogden, W.F.: Verification of programs with procedure-type parameters. Acta Informatica 18(2), 149–169 (1982)
Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: ACM International Conference on Functional Programming (2002)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)
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–78. Springer, Heidelberg (1991). doi:10.1007/BFb0019995
Hirschfeld, R., Costanza, P., Nierstrasz, O.: Context-oriented programming. J. Object Technol. 7(3), 125–151 (2008)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall, Englewood Cliffs (1986)
Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Akşit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997). doi:10.1007/BFb0053381
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–354. Springer, Heidelberg (2001). doi:10.1007/3-540-45337-7_18
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)
Meyer, B.: Applying ‘design by contract’. Computer 25(10), 40–51 (1992)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Upper Saddle River (1997)
Morgan, C.: Procedures, parameters, abstraction: separate concerns. Sci. Comput. Program. 11(1), 17–27 (1988)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Hertfordshire (1994)
Naumann, D.A.: Predicate transformers and higher order programs. Theor. Comput. Sci. 150, 111–159 (1995)
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
Rajan, H., Leavens, G.T.: Ptolemy: a language with quantified, typed events. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 155–179. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70592-5_8
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–347. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00590-9_24
Sánchez, J., Leavens, G.T.: Reasoning tradeoffs in languages with enhanced modularity features. In: 15th International Conference on Modularity (2016)
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)
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)
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–333. Springer, Heidelberg (2004). doi:10.1007/978-3-540-39993-3_15
Wing, J.M.: Writing Larch interface language specifications. ACM Trans. Prog. Lang. Syst. 9(1), 1–24 (1987)
Acknowledgments
Thanks to Luke Meyers and Klaus Havelund for comments on an earlier draft. Special thanks to Steve Shaner, who co-developed the theory behind this paper with Leavens and Naumann [33]. Thanks to Mehdi Bagherzadeh and Jose Sanchez, who helped us apply greybox specification techniques to Ptolemy and AspectJ. The work of Leavens was supported in part by US NSF grants CNS1228695 and CCF1518897. The work of Naumann was supported in part by NSF CNS 1228930. The work of Rajan was supported in part by NSF grants CCF-15-18897, CNS-15-13263, CCF-14-23370, CCF-11-17937, and CCF-08-46059. The work of Aotani was supported by the Core Research for Evolutional Science and Technology (CREST) Program, “Software development for post petascale supercomputing — Modularity for supercomputing” by the Japan Science and Technology Agency.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Leavens, G.T., Naumann, D., Rajan, H., Aotani, T. (2016). Specifying and Verifying Advanced Control Features. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. ISoLA 2016. Lecture Notes in Computer Science(), vol 9953. Springer, Cham. https://doi.org/10.1007/978-3-319-47169-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-47169-3_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47168-6
Online ISBN: 978-3-319-47169-3
eBook Packages: Computer ScienceComputer Science (R0)