Sciweavers

ESOP
2006
Springer

Inference of User-Defined Type Qualifiers and Qualifier Rules

13 years 6 months ago
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...
Brian Chin, Shane Markstrum, Todd D. Millstein, Je
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where ESOP
Authors Brian Chin, Shane Markstrum, Todd D. Millstein, Jens Palsberg
Comments (0)