K框架中规约的自动推断
编程语言
2015-12-23 v1 计算机科学中的逻辑
摘要
尽管形式化规约具有许多毋庸置疑的好处，但它们并未在工业软件开发中被广泛采用。为了减少编写形式化规约所需的时间和精力，本文提出一种从真实代码中自动发现规约的技术。所提出的方法依赖于 K 框架最近提供的符号执行能力，我们利用该能力从用 C 语言的一个非平凡片段（称为 KernelC）编写的程序中自动推断形式化规约。粗略地说，我们对 KernelC 程序的符号分析通过使用程序中的其他（观察器）例程来解释（修改器）函数的执行。我们在自动化工具 Kindspec 2.0 中实现了该技术，其生成公理来描述处理基于指针的结构（即结果值和状态改变）的 C 例程的精确输入/输出行为。我们描述了系统的实现，并讨论了与我们之前从 C 代码推断规约工作的差异。
引用
@article{arxiv.1512.06941,
title = {Automatic Inference of Specifications in the K Framework},
author = {María Alpuente and Daniel Pardo and Alicia Villanueva},
journal= {arXiv preprint arXiv:1512.06941},
year = {2015}
}
备注
In Proceedings PROLE 2015, arXiv:1512.06178