Title :
OwnKit: Inferring Modularly Checkable Ownership Annotations for Java
Author :
Dymnikov, Constantine ; Pearce, David J. ; Potanin, Alex
Author_Institution :
Sch. of Eng. & Comput. Sci., Victoria Univ. of Wellington, Wellington, New Zealand
Abstract :
Ownership and related systems impose restrictions on the object graph that can help improve program structure, exploit concurrency and verify software. Such systems rely on the presence of appropriate ownership annotations in the source code. Unfortunately, manually adding ownership annotations to legacy systems is a tedious process. Previous attempts at automatically inferring such ownership systems do not produce modularly checkable annotations (i.e. which allow classes to be checked in isolation) making them difficult to incorporate into day-to-day development. In this paper, we present Own Kit - a system for automatically inferring ownership annotations which are modularly checkable. We describe and evaluate our approach on a number of real-world benchmarks and compare against an existing system.
Keywords :
Java; formal verification; graph theory; inference mechanisms; multiprocessing programs; source coding; Java; OwnKit; concurrency; modularly checkable ownership annotations; object graph; program structure; software verification; source code; Aging; Complexity theory; Educational institutions; Electronic mail; Java; Software; Java; ownership; type inference;
Conference_Titel :
Software Engineering Conference (ASWEC), 2013 22nd Australian
Conference_Location :
Melbourne, VIC
DOI :
10.1109/ASWEC.2013.30