zbMATH — the first resource for mathematics

Tunable static inference for generic universe types. (English) Zbl 1435.68061
Mezini, Mira (ed.), ECOOP 2011 – object-oriented programming. 25th European conference, Lancaster, UK, July 25–29, 2011. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 6813, 333-357 (2011).
Summary: Object ownership is useful for many applications, including program verification, thread synchronization, and memory management. However, the annotation overhead of ownership type systems hampers their widespread application. This paper addresses this issue by presenting a tunable static type inference for Generic Universe Types. In contrast to classical type systems, ownership types have no single most general typing. Our inference chooses among the legal typings via heuristics. Our inference is tunable: users can indicate a preference for certain typings by adjusting the heuristics or by supplying partial annotations for the program. We present how the constraints of Generic Universe Types can be encoded as a Boolean satisfiability (SAT) problem and how a weighted Max-SAT solver finds a correct Universe typing that optimizes the weights. We implemented the static inference tool, applied our inference tool to four real-world applications, and inferred interesting ownership structures.
For the entire collection see [Zbl 1220.68017].

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68R07 Computational aspects of satisfiability
Full Text: DOI