类型状态检查和正则图约束
Typestate Checking and Regular Graph Constraints
摘要：
我们引入了正则图约束，并探讨其可判定性。规则图约束的动机是1）在存在链接的数据结构的情况下改变对象类型的类型检查，2）形状分析技术，以及3）在树和网格上的类似约束的泛化。我们定义了一个称为堆的图子类，作为程序在执行过程中构造的数据结构的抽象。证明了堆类上正则图约束蕴涵的有效性是不可判定的。我们表现出不可判定性表现出一定的“对应图”的存在和不存在的同态有限数量的固定图的特征。正则图约束蕴涵的不可判定性意味着，当这些属性用任何规约语言表达时，都没有算法来验证过程前提条件是否满足，或者不变量是否保持不变，至少与正则图约束一样具有表达性。
英文摘要：
We introduce regular graph constraints and explore their decidability properties. The motivation for regular graph constraints is 1) type checking of changing types of objects in the presence of linked data structures, 2) shape analysis techniques, and 3) generalization of similar constraints over trees and grids. We define a subclass of graphs called heaps as an abstraction of the data structures that a program constructs during its execution. We prove that determining the validity of implication for regular graph constraints over the class of heaps is undecidable. We show undecidability by exhibiting a characterization of certain "corresponder graphs" in terms of presence and absence of homomorphisms to a finite number of fixed graphs. The undecidability of implication of regular graph constraints implies that there is no algorithm that will verify that procedure preconditions are met or that the invariants are maintained when these properties are expressed in any specification language at least as expressive as regular graph constraints.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
