Resource control of object-oriented programs

TL;DR

This paper extends the concept of sup-interpretations from first-order functional programs to a fragment of object-oriented programs, providing a criterion to ensure polynomial size bounds on computed objects.

Contribution

It introduces the brotherly criterion for object-oriented programs, enabling size bounds analysis within this programming paradigm.

Findings

The brotherly criterion guarantees polynomial size bounds for certain object-oriented programs.

Sup-interpretations can be adapted to object-oriented languages with loops, methods, and side effects.

The framework helps analyze complexity and resource control in object-oriented programming.

Abstract

A sup-interpretation is a tool which provides an upper bound on the size of a value computed by some symbol of a program. Sup-interpretations have shown their interest to deal with the complexity of first order functional programs. For instance, they allow to characterize all the functions bitwise computable in Alogtime. This paper is an attempt to adapt the framework of sup-interpretations to a fragment of oriented-object programs, including distinct encodings of numbers through the use of constructor symbols, loop and while constructs and non recursive methods with side effects. We give a criterion, called brotherly criterion, which ensures that each brotherly program computes objects whose size is polynomially bounded by the inputs sizes.