×

A type-based complexity analysis of object oriented programs. (English) Zbl 1395.68087

Summary: A type system is introduced for a generic Object Oriented programming language in order to infer resource upper bounds. A sound and complete characterization of the set of polynomial time computable functions is obtained. As a consequence, the heap-space and the stack-space requirements of typed programs are also bounded polynomially. This type system is inspired by previous works on Implicit Computational Complexity, using tiering and non-interference techniques. The presented methodology has several advantages. First, it provides explicit big \(O\) polynomial upper bounds to the programmer, hence its use could allow the programmer to avoid memory errors. Second, type checking is decidable in polynomial time. Last, it has a good expressivity since it analyzes most object oriented features like inheritance, overload, override and recursion. Moreover it can deal with loops guarded by objects and can also be extended to statements that alter the control flow like break or return.

MSC:

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q25 Analysis of algorithms and problem complexity

References:

[1] Bellantoni, S.; Cook, S., A new recursion-theoretic characterization of the poly-time functions, Comput. Complex., 2, 97-110, (1992) · Zbl 0766.68037
[2] Leivant, D.; Marion, J.-Y., Lambda calculus characterizations of poly-time, Fundam. Inform., 19, 1/2, 167-184, (1993) · Zbl 0781.68059
[3] Volpano, D.; Irvine, C.; Smith, G., A sound type system for secure flow analysis, J. Comput. Secur., 4, 2/3, 167-188, (1996)
[4] Hainry, E.; Péchoux, R., Objects in polynomial time, (Programming Languages and Systems, 13th Asian Symposium, APLAS 2015, Lecture Notes in Computer Science, vol. 9458, (2015)), 387-404 · Zbl 1329.68069
[5] Marion, J.-Y., A type system for complexity flow analysis, (26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, (2011)), 123-132
[6] 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)
[7] Girard, J.-Y., Light linear logic, Inf. Comput., 143, 2, 175-204, (1998) · Zbl 0912.03025
[8] Cook, S. A.; Rackoff, C., Space lower bounds for maze threadability on restricted machines, SIAM J. Comput., 9, 3, 636-652, (1980) · Zbl 0445.68038
[9] Danner, N.; Royer, J. S., Ramified structural recursion and corecursion, CoRR
[10] Hainry, E.; Marion, J.-Y.; Péchoux, R., Type-based complexity analysis for fork processes, (FOSSACS, Lecture Notes in Computer Science, vol. 7794, (2013)), 305-320 · Zbl 1260.68097
[11] Leivant, D.; Marion, J.-Y., Evolving graph-structures and their implicit computational complexity, (Automata, Languages, and Programming, ICALP 2013, Lecture Notes in Computer Science, vol. 7966, (2013)), 349-360 · Zbl 1334.68048
[12] Niggl, K.-H.; Wunderlich, H., Certifying polynomial time and linear/polynomial space for imperative programs, SIAM J. Comput., 35, 5, 1122-1147, (2006) · Zbl 1100.68035
[13] Moyen, J.-Y., Resource control graphs, ACM Trans. Comput. Log., 10, 4, 29:1-29:44, (2009) · Zbl 1351.68077
[14] Jones, N. D.; Kristiansen, L., A flow calculus of wp-bounds for complexity analysis, ACM Trans. Comput. Log., 10, 4, (2009)
[15] Hofmann, M.; Jost, S., Type-based amortised heap-space analysis, (ESOP, Lecture Notes in Computer Science, vol. 3924, (2006)), 22-37 · Zbl 1178.68143
[16] Hofmann, M.; Rodriguez, D., Efficient type-checking for amortised heap-space analysis, (CSL, Lecture Notes in Computer Science, vol. 5771, (2009)), 317-331 · Zbl 1257.68051
[17] Hofmann, M.; Jost, S., Static prediction of heap space usage for first-order functional programs, (Symposium on Principles of Programming Languages, POPL 2003, (2003), ACM), 185-197 · Zbl 1321.68180
[18] Jost, S.; Hammond, K.; Loidl, H.-W.; Hofmann, M., Static determination of quantitative resource usage for higher-order programs, (Symposium on Principles of Programming Languages, POPL 2010, (2010)), 223-236 · Zbl 1312.68039
[19] Beringer, L.; Hofmann, M.; Momigliano, A.; Shkaravska, O., Automatic certification of heap consumption, (LPAR, Lecture Notes in Computer Science, vol. 3452, (2004)), 347-362 · Zbl 1108.68374
[20] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Zanardini, D., Costa: design and implementation of a cost and termination analyzer for Java bytecode, (FMCO, Lecture Notes in Computer Science, vol. 5382, (2008)), 113-132
[21] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Zanardini, D., Cost analysis of object-oriented bytecode programs, Theor. Comput. Sci., 413, 1, 142-159, (2012) · Zbl 1236.68042
[22] Kersten, R.; Shkaravska, O.; van Gastel, B.; Montenegro, M.; van Eekelen, M. C.J. D., Making resource analysis practical for real-time Java, (Java Technologies for Real-Time and Embedded Systems, JTRES’12, (2012)), 135-144
[23] Cachera, D.; Jensen, T.; Pichardie, D.; Schneider, G., Certified memory usage analysis, (FM 2005: Formal Methods, Lecture Notes in Computer Science, vol. 3582, (2005)), 91-106 · Zbl 1120.68385
[24] Albert, E.; Genaim, S.; Gómez-Zamalloa Gil, M., Live heap space analysis for languages with garbage collection, (Proceedings of the 2009 International Symposium on Memory Management, (2009), ACM), 129-138
[25] Albert, E.; Genaim, S.; Gómez-Zamalloa, M., Parametric inference of memory requirements for garbage collected languages, ACM Sigplan Notices, vol. 45, 121-130, (2010), ACM
[26] Chin, W.; Nguyen, H.; Qin, S.; Rinard, M., Memory usage verification for OO programs, (Static Analysis, SAS 2005, (2005)), 70-86 · Zbl 1141.68364
[27] Hofmann, M.; Schöpp, U., Pointer programs and undirected reachability, (24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, (2009), IEEE Computer Society), 133-142
[28] Hofmann, M.; Schöpp, U., Pure pointer programs with iteration, ACM Trans. Comput. Log., 11, 4, (2010) · Zbl 1351.68101
[29] Ben-Amram, A. M., Size-change termination, monotonicity constraints and ranking functions, Log. Methods Comput. Sci., 6, 3, (2010) · Zbl 1191.68179
[30] Ben-Amram, A. M.; Genaim, S.; Masud, A. N., On the termination of integer loops, (Verification, Model Checking, and Abstract Interpretation, VMCAI 2012, Lecture Notes in Computer Science, vol. 7148, (2012)), 72-87 · Zbl 1325.68056
[31] Cook, B.; Podelski, A.; Rybalchenko, A., Terminator: beyond safety, (Computer Aided Verification, CAV 2006, Lecture Notes in Computer Science, vol. 4144, (2006)), 415-426
[32] Podelski, A.; Rybalchenko, A., Transition predicate abstraction and fair termination, (Symposium on Principles of Programming Languages, POPL 2005, (2005), ACM), 132-144 · Zbl 1369.68152
[33] Gulwani, S., Speed: symbolic complexity bound analysis, (Computer Aided Verification, CAV 2009, Lecture Notes in Computer Science, vol. 5643, (2009)), 51-62 · Zbl 1242.68121
[34] Gulwani, S.; Mehra, K. K.; Chilimbi, T. M., Speed: precise and efficient static estimation of program computational complexity, (Symposium on Principles of Programming Languages, POPL 2009, (2009), ACM), 127-139 · Zbl 1315.68095
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.