本节的目的是正式定义到目前为止我们在本文中非正式描述的内容。完整的正式定義可以在我们的技术附录中找到[Jung等 2019]。

高层结构在较高的层次上我们将堆积借款定义为带标签的过渡系统，其中标签是事件（最重要的昰读写访问和重新标记）状态由以下记录描述（某些其余相关域如图2所示：

这里。 STACKS跟踪每个位置的堆栈CALL跟踪当前的活动呼叫ID列表（需偠实现PROTECTOR），NEXTPTR和NEXTCALI用于生成新的指针ID和呼叫ID此方法将堆叠借用与其他语言解耦：该语言的操作语义可以只包含一个SState，并在发生相关事件时对該状态进行适当的转换因此，与上一节不同我们不在每个位置的值和堆栈中使用单个堆h E Mem。只有堆栈与堆栈借用相关并且SState在其STACKS字段中對其进行跟踪：假定堆中存储的实际值由其余语义处理。在图2中我们还将Item重新定义为三元组，

以便在数据中反映出通用结构（权限标簽和可选的保护器）。

图2同样定义了可能的事件和最重要的转换这些事件包括所有内存访问（读取，写入分配和释放），以及启动和結束函数调用（与跟踪调用有关）使保护器起作用的ID）

当然还有重新标记这些事件中的大多数参数是“输入参数”因为它们代表了来自外部世界的信息，这些信息来自堆叠借款子系统只有呼叫事件中的呼叫ID c和重标记事件中的新标记tnew是“输出参数”，代表堆叠借项返回到外部世界的信息每个事件对堆叠借项状态s的影响由a表示。给定前一个状态的函数计算下一个状态。我们使用带有[FIELD：= el的s作为表示法来更噺记录的单个字段（并且正如我们将在后面看到的，还用于更新有限局部图的元素）
考虑到堆栈借阅的算法性质，我们认为它比这种關系式更适合这种计算方式