zbMATH — the first resource for mathematics

A proof system for adaptable class hierarchies. (English) Zbl 1304.68031
Summary: The code base of a software system undergoes changes during its life time. For object-oriented languages, classes are adapted, e.g., to meet new requirements, customize the software to specific user functionalities, or refactor the code to reduce its complexity. However, the adaptation of class hierarchies makes reasoning about program behavior challenging; even classes in the middle of a class hierarchy can be modified. This paper develops a proof system for analyzing the effect of operations to adapt classes, in the context of method overriding and late bound method calls. The proof system is incremental in the sense that reverification is avoided for methods that are not explicitly changed by adaptations. Furthermore, the possible adaptations are not unduly restricted; i.e., flexibility is retained without compromising on reasoning control. To achieve this balance, we extend the mechanism of lazy behavioral subtyping, originally proposed for reasoning about inheritance when subclasses are added to a class hierarchy, to deal with the more general situation of adaptable class hierarchies and changing specifications. The reasoning system distinguishes guaranteed method behavior from requirements toward methods, and achieves incremental reasoning by tracking guarantees and requirements in adaptable class hierarchies. We show soundness of the proposed proof system.
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
Full Text: DOI
[1] Clarke, D.; Diakov, N.; Hähnle, R.; Johnsen, E. B.; Schaefer, I.; Schäfer, J.; Schlatte, R.; Wong, P. Y.H., Modeling spatial and temporal variability with the HATS abstract behavioral modeling language, (Bernardo, M.; Issarny, V., Proceedings of the 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM 2011), Lect. Notes Comput. Sci., vol. 6659, (2011), Springer-Verlag), 417-457
[2] Mens, T.; Tourwé, T., A survey of software refactoring, IEEE Trans. Softw. Eng., 30, 2, 126-139, (2004)
[3] Fowler, M., Refactoring: improving the design of existing code, (1999), Addison-Wesley · Zbl 1020.68632
[4] Liskov, B. H.; Wing, J. M., A behavioral notion of subtyping, ACM Trans. Program. Lang. Syst., 16, 6, 1811-1841, (1994)
[5] Soundarajan, N.; Fridella, S., Inheritance: from code reuse to reasoning reuse, (Devanbu, P.; Poulin, J., Proceedings of the Fifth International Conference on Software Reuse (ICSR5), (1998), IEEE Computer Society Press), 206-215
[6] Dovland, J.; Johnsen, E. B.; Owe, O.; Steffen, M., Lazy behavioral subtyping, J. Log. Algebr. Program., 79, 7, 578-607, (2010) · Zbl 1204.68072
[7] Dovland, J.; Johnsen, E. B.; Owe, O.; Steffen, M., Incremental reasoning with lazy behavioral subtyping for multiple inheritance, Sci. Comput. Program., 76, 10, 915-941, (2011) · Zbl 1221.68058
[8] Damiani, F.; Dovland, J.; Johnsen, E. B.; Schaefer, I., Verifying traits: an incremental proof system for fine-grained reuse, Form. Asp. Comput., 26, 4, 761-793, (2014) · Zbl 1342.68059
[9] Igarashi, A.; Pierce, B. C.; Wadler, P., Featherweight Java: a minimal core calculus for Java and GJ, ACM Trans. Program. Lang. Syst., 23, 3, 396-450, (2001)
[10] Gamma, E.; Helm, R.; Johnson, R.; Vlissides, J., Design patterns: elements of reusable object-oriented software, (1995), Addison-Wesley Reading, MA
[11] Johnsen, E. B.; Kyas, M.; Yu, I. C., Dynamic classes: modular asynchronous evolution of distributed concurrent objects, (Cavalcanti, A.; Dams, D., Proc. 16th International Symposium on Formal Methods (FM’09), Lect. Notes Comput. Sci., vol. 5850, (2009), Springer-Verlag), 596-611
[12] Johnsen, E. B.; Owe, O., An asynchronous communication model for distributed concurrent objects, Softw. Syst. Model., 6, 1, 35-58, (2007)
[13] Schaefer, I.; Bettini, L.; Bono, V.; Damiani, F.; Tanzarella, N., Delta-oriented programming of software product lines, (Proceedings of the 14th International Conference on Software Product Lines (SPLC 2010), Lect. Notes Comput. Sci., vol. 6287, (2010), Springer-Verlag), 77-91
[14] Johnsen, E. B.; Owe, O.; Yu, I. C., Creol: a type-safe object-oriented model for distributed concurrent systems, Theor. Comput. Sci., 365, 1-2, 23-66, (2006) · Zbl 1118.68031
[15] Apt, K. R., Ten years of Hoare’s logic: a survey — part I, ACM Trans. Program. Lang. Syst., 3, 4, 431-483, (1981) · Zbl 0471.68006
[16] Apt, K. R.; de Boer, F. S.; Olderog, E.-R., Verification of sequential and concurrent systems, Texts Monogr. Comput. Sci., (2009), Springer-Verlag · Zbl 1183.68361
[17] de Boer, F. S., A WP-calculus for OO, (Thomas, W., Proceedings of Foundations of Software Science and Computation Structure (FOSSACS’99), Lect. Notes Comput. Sci., vol. 1578, (1999), Springer-Verlag), 135-149
[18] Hoare, C. A.R., An axiomatic basis of computer programming, Commun. ACM, 12, 576-580, (1969) · Zbl 0179.23105
[19] Owicki, S.; Gries, D., An axiomatic proof technique for parallel programs I, Acta Inform., 6, 4, 319-340, (1976) · Zbl 0312.68011
[20] Dahl, O.-J.; Owe, O., Formal development with ABEL, (Prehn, S.; Toetenel, H., Proc. Formal Software Development Methods (VDM’91), Lect. Notes Comput. Sci., vol. 552, (1991), Springer-Verlag), 320-362
[21] Dovland, J.; Johnsen, E. B.; Owe, O., Verification of concurrent objects with asynchronous method calls, (Proceedings of the IEEE International Conference on Software - Science, Technology & Engineering (SwSTE’05), (2005), IEEE Computer Society Press), 141-150
[22] Din, C. C.; Dovland, J.; Johnsen, E. B.; Owe, O., Observable behavior of distributed systems: component reasoning for concurrent objects, J. Log. Algebr. Program., 81, 3, 227-256, (2012) · Zbl 1247.68184
[23] Dhara, K. K.; Leavens, G. T., Forcing behavioural subtyping through specification inheritance, (Proceedings of the 18th International Conference on Software Engineering, (1996), IEEE Computer Society Press), 258-267, also as Iowa State University Tech. Rep. TR-95-20c
[24] Dovland, J.; Johnsen, E. B.; Yu, I. C., Tracking behavioral constraints during object-oriented software evolution, (Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’12), Part I, Lect. Notes Comput. Sci., vol. 7609, (2012), Springer-Verlag), 253-268
[25] Pohl, K.; Böckle, G.; Van Der Linden, F., Software product line engineering: foundations, principles, and techniques, (2005), Springer-Verlag · Zbl 1075.68575
[26] Schaefer, I.; Hähnle, R., Formal methods in software product line engineering, Computer, 44, 2, 82-85, (2011)
[27] Thüm, T.; Schaefer, I.; Kuhlemann, M.; Apel, S., Proof composition for deductive verification of software product lines, (Proceedings of the International Workshop Variability-intensive Systems Testing, Validation and Verification (VAST), (2011), IEEE Computer Society Press), 270-277
[28] Bruns, D.; Klebanov, V.; Schaefer, I., Verification of software product lines with delta-oriented slicing, (Proceedings of the International Conference on Formel Verification of Object-Oriented Software (FoVeOOS 2010), Lect. Notes Comput. Sci., vol. 6528, (2011)), 61-75 · Zbl 1308.68038
[29] Hähnle, R.; Schaefer, I., A liskov principle for delta-oriented programming, (Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), Part I, Lect. Notes Comput. Sci., vol. 7609, (2012), Springer-Verlag), 32-46
[30] Damiani, F.; Dovland, J.; Johnsen, E. B.; Owe, O.; Schaefer, I.; Yu, I. C., A transformational proof system for delta-oriented programming, (de Almeida, E. S.; Schwanninger, C.; Benavides, D., Proceedings of the 16th International Software Product Line Conference (SPLC), vol. 2, (2012), ACM), 53-60, Proceedings of the 3rd International Workshop on Formal Methods for Software Product Lines (FMSPLE’12)
[31] Van Der Straeten, R.; Jonckers, V.; Mens, T., A formal approach to model refactoring and model refinement, Softw. Syst. Model., 6, 139-162, (2007)
[32] Massoni, T.; Gheyi, R.; Borba, P., Synchronizing model and program refactoring, (Davies, J.; Silva, L.; Simao, A., Formal Methods: Foundations and Applications, Lect. Notes Comput. Sci., vol. 6527, (2011), Springer-Verlag), 96-111 · Zbl 1325.68067
[33] Marković, S.; Baar, T., Refactoring OCL annotated UML class diagrams, Softw. Syst. Model., 7, 25-47, (2008)
[34] Yin, X.; Knight, J. C.; Weimer, W., Exploiting refactoring in formal verification, (Proceedings Dependable Systems and Networks (DSN’09), (2009), IEEE Computer Society Press), 53-62
[35] Ubayashi, N.; Piao, J.; Shinotsuka, S.; Tamai, T., Contract-based verification for aspect-oriented refactoring, (Proceedings of the International Conference on Software Testing, Verification, and Validation, (2008), IEEE Computer Society Press), 180-189
[36] Wehrheim, H., Slicing techniques for verification re-use, Theor. Comput. Sci., 343, 3, 509-528, (2005) · Zbl 1079.68061
[37] (Beckert, B.; Hähnle, R.; Schmitt, P. H., Verification of Object-Oriented Software. The KeY Approach, Lect. Notes Artif. Intell., vol. 4334, (2007), Springer-Verlag)
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.