类型状态检查与正则图约束

我们引入了正则图约束并探讨了其可判定性。正则图约束的动机是：1）在存在链式数据结构的情况下对对象变化类型进行类型检查；2）形状分析技术；3）对树和网格上类似约束的推广。我们将图的子类“堆”定义为对程序在执行期间所构造数据结构的抽象。我们证明了，确定堆类上正则图约束蕴含的有效性是不可判定的。我们通过以下方式证明不可判定性：利用同态到有限数量固定图的存在与不存在，对某些“对应图”进行刻画。正则图约束蕴含的不可判定性意味着，当这些属性在任何表达能力至少与正则图约束相当的规约语言中表达时，不存在能够验证过程前置条件是否满足或不变量是否得以维持的算法。