CAJ | 학술논문

提出了一种链表抽象表示方法.该方法隐式存储链表结点之间的边信息,并采用了一种紧致的链表状态表示,存储开销较低,且维护了链表长度信息,精确度较高.具体而言,根据变量对链表结点的可达性质定义了变量可达向量,采用带计数的变量可达向量集描述链表的形态及数量性质,并定义了基本链表操作的抽象语义.通过简单扩展,该方法可以建模包括环形链表在内的所有单向链表.最后,为了验证该链表抽象方法的正确性,在符号执行框架中进行实验,并对常见链表操作程序的运行时错误、长度相关性质等关键性质进行了分析与验证.
제출료일충련표추상표시방법.해방법은식존저련표결점지간적변신식,병채용료일충긴치적련표상태표시,존저개소교저,차유호료련표장도신식,정학도교고.구체이언,근거변량대련표결점적가체성질정의료변량가체향량,채용대계수적변량가체향량집묘술련표적형태급수량성질,병정의료기본련표조작적추상어의.통과간단확전,해방법가이건모포괄배형련표재내적소유단향련표.최후,위료험증해련표추상방법적정학성,재부호집행광가중진행실험,병대상견련표조작정서적운행시착오、장도상관성질등관건성질진행료분석여험증.