摘要
类型限定词可以精化标准类型,提高类型系统的表达能力。流不敏感的类型限定词推断已被用于CQual架构,以提高C程序的质量。然而,类型转化会影响类型限定词推断的有效性。首先,展示了一种允许类型转化的程序语言和流不敏感的限定词推断系统;其次,提出了变量参与的限定词推断系统,引入了联合类型并给出约束求解算法;最后,证明了推断的正确性并展示了一些实例运行结果。
Type qualifiers can refine the standard types and improve the expressivity of type systems. Flow insensitive type qualifier inference has been used in the CQual framework to improve the quality of C programs. Type casts, however, will affect the effectiveness of type qualifier inference. First a language allowing type casts and its flow-insensitive qualifier inference system were presented. Then this paper proposed a variable-involved inference system, introduced union types and given constraints solving algorithm. Finally, the soundness was proved and some case studies were pre-sented.
出处
《计算机科学》
CSCD
北大核心
2014年第9期178-184,共7页
Computer Science
基金
国家科技重大专项(2012ZX01039-004)资助
