A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors . In this paper, we consider theproblem of enforcing guidelines for Featherweight Java (FJ) We formalize guidelines as sets of finite or infinite execution traces and develop aregion-based type and effect system for FJ that can enforce such guidelines . We use ideas of Hofmann and Chen to extend it to capture also infinite traces produced by non-terminating programs . Our type inference algorithm is realized by working with the finitary abstraction of the system based on B\”uchi automata. Our type system can express properties ofboth finite and infinite traces and can compute information about the possibleinfinite traces of FJ programs. Specifically, the set of infinite traces of amethod is constructed as the greatest fixed point of the operator whichculates

Author(s) : Serdar Erbatur, Ulrich Schöpp, Chuangjie Xu

Links : PDF - Abstract

Code :

Keywords : traces - infinite - guidelines - type - fj -

Leave a Reply

Your email address will not be published. Required fields are marked *