题目：Scope Logic及其设计动机

报告人：赵建华（南京大学计算机系）

时间：2010年3月8日（星期一）上午9:00

地点：中科院软件所5号楼三层报告厅

摘要：

这个报告首先通过一个小程序的正确性论证过程说明指针程序的形式化验证需要把以下知识形式化地表述出来：

1. 程序中复合类型的内存布局方式

2. 递归定义的函数对内存的存取范围

3. 各类语句的操作效果

我们还演示如何有效地使用这些知识和一些技巧来证明指针程序的正确性。

随后，这个报告给出相应的证明规则来形式化地表述上面的知识。这些规则包括：刻画内存存取过程的规则、复合类型内存布局的规则、递归函数对内存访问范围的证明规则、赋值语句/内存分配语句的规则、控制流语句的证明规则。还通过一个程序粗略地演示如何在较高的抽象层次上证明一段代码。