Abstract
In previous work, we described a new approach to supporting user-defined 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 user-defined 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 the burden of manually producing such rules. We have formalized both qualifier and rule inference and proven their correctness. We have also extended Clarity to support qualifier and rule inference, and we illustrate their utility in practice through experiments with several type qualifiers and open-source C programs.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of the ACMSIGPLAN 2001 conference on Programming language design and implementation, pp. 203–213. ACM Press, New York (2001)
Chin, B., Markstrum, S., Millstein, T.: Semantic type qualifiers. In: PLDI 2005: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 85–95. ACM Press, New York (2005)
Chin, B., Markstrum, S., Millstein, T., Palsberg, J.: Inference of user-defined type qualifiers and qualifier rules. Technical Report CSD-TR-050041, UCLA Computer Science Department (October 2005)
Davies, R., Pfenning, F.: Intersection types and computational effects. In: ICFP 2000: Proceedings of the ACM SIGPLAN International Conference on Functional Programming, pp. 198–208. ACM Press, New York (2000)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)
Foster, J.S., Fähndrich, M., Aiken, A.: A Theory of Type Qualifiers. In: Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation, Atlanta, Georgia, pp. 192–203 (May 1999)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 1–12. ACM Press, New York (2002)
Freeman, T., Pfenning, F.: Refinement types for ML. In: PLDI 1991: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, pp. 268–277. ACM Press, New York (1991)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proceedings of the eighth ACMSIGPLAN international conference on Functional programming, pp. 213–225. ACM Press, New York (2003)
Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theor. Pract. Object Syst. 5(1), 35–55 (1999)
Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic implementation of the best transformer. In: 5th International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 252–266 (2004)
Yorsh, G., Reps, T.W., Sagiv, S.: Symbolically computing most-precise abstract operations for shape analysis. In: 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 530–545 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chin, B., Markstrum, S., Millstein, T., Palsberg, J. (2006). Inference of User-Defined Type Qualifiers and Qualifier Rules. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_18
Download citation
DOI: https://doi.org/10.1007/11693024_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33095-0
Online ISBN: 978-3-540-33096-7
eBook Packages: Computer ScienceComputer Science (R0)