Inference of User-Defined Type Qualifiers and Qualifier Rules

Abstract. In previous work, we described a new approach to supporting userdefined type qualifiers, which augment existing types to specify and check additional properties of interest. For each qualifier, users define a set of rules that are enforced during static typechecking of programs. Separately, these rules are automatically validated with respect to a user-defined predicate that formalizes the qualifier's intended run-time invariant. We instantiated this approach as a framework for user-defined type qualifiers in C programs, called CLARITY. In this paper, we extend our earlier approach by resolving two usability issues. First, we show how to perform qualifier inference in the presence of userdefined rules by generating and solving a system of conditional set constraints, thereby relieving users of the burden of explicitly annotating programs. Second, we show how to automatically infer rules that respect a given user-defined invariant, thereby relieving qualifier designers of...

• Type: Conference
• Year: 2006
• Where: ESOP
• Authors: Brian Chin, Shane Markstrum, Todd D. Millstein, Jens Palsberg
• Keywords: ESOP 2006, Programming Languages, Qualifier, Type Qualifiers, User-defined Type Qualifiers