自然数阶乘算法程序正确性的形式化证明
摘 要：程序正确性与可信性是各类计算机系统中最重要的核心问题。在开展“C程序设计”课程双语教学、以及精品在线开放课程建设的实践中，培养计算思维的意识和能力是核心任务。本文选择体现计算思维本质特征的“自然数阶乘算法”这个典型程序为抓手，透过程序调试与测试的表象，直击程序正确性与可信性的核心，通过程序的完全正确性证明，为开展计算思维的形式化方法教育、培养视野及思维开阔的国际化人才，进行了有益的实践。
关键词：阶乘算法;程序正确性;形式化证明;计算思维;双语教学
1 引言
实施双语教学，是“互联网+”及智能时代培养国际化人才的重要举措。广州涉外学院发挥“涉外”特色优势，采用爱尔兰都柏林工业大学Paul Kelly编著的中国教育部双语教学示范教材[1]，在计算机应用及软件技术专业强化双语教学，取得显著成效[2]。在进一步开展“双语C程序设计”精品在线开放课程的建设实践中，更需要注重将“计算思维”的意识培养和方法应用贯穿人才培养和实践教学的全过程。
计算思维被认为是数学逻辑思维、物理实证思维后的第三种思维方式，由美国计算机科学家周以真教授首次提出[3]：计算思维是与形式化问题及其解决方法相关的思维过程，是运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等思维活动，根本特征是抽象和自动化。形式化方法用严格的符号系统和数学模型描述和验证一个目标软件系统的行为和特性[4]，使用严格精确的数学语言、无二义的语法语义，以及一组定義其语法语义的形式化规则，采用严谨的演绎推理法完成逻辑分析和证明。
程序设计课程是培养计算思维最有效的工具。中国九校(首批“985工程”建设高校)联盟在计算机基础教学发展战略联合声明中，把培养计算思维能力作为计算机基础教学的核心任务[5]。而自然数的阶乘算法，可用“循环结构”与“递归函数”两种程序实现，体现了计算思维中“自动化”的本质特征，成为培养计算思维能力的最好抓手。
2 程序正确性概述
程序的正确性是衡量一个程序正常工作的基本条件。然而，程序所描述的动态计算过程是无法直接用程序本身的静态结构进行正确性证明。因此，程序含有错误是难免的。为尽量减少错误[6]，首先应使用结构化程序设计方法，并在程序调试时采用软件测试的方法去跟踪程序的运行，从而发现与改正错误，但更重要的是采用程序正确性证明的理论进行证明。
然而，这些早期的奠基性工作仍有很多不足之处[4]，在应用中异常繁琐且较难掌握。但其中采用形式化方法构建正确及可信的程序，则有利于提高计算思维能力，便于从理论上指导设计出正确的程序。
程序规约是对程序所实现功能的精确描述，是程序正确性的判断依据，由程序的前置断言和后置断言两部分组成。前置断言是程序执行前的输入应满足的条件，用一阶逻辑公式Pre表示。后置断言是程序执行后的输出应满足的条件，用一阶逻辑公式Post表示。若用P表示问题求解的实现程序，则程序规约可用Floyd-Hoare逻辑公式表示为{Pre}P{Post}，根据此逻辑表达式的布尔值，对程序正确性做以下定义：
(1)部分正确：若对于每个使Pre(i)为真，且能使程序P计算终止的输入信息i，Post(i，P(i))都为真，则称程序P关于Pre和Post是部分正确的。
(2)程序终止：若对于每个使Pre(i)为真的输入i，程序P的计算都终止，则称程序P关于Pre是终止的。
(3)完全正确：若对于每个使Pre(i)为真的输入信息i，程序P的计算都将终止，并且Post(i，P(i))都为真，则称程序P关于Pre和Post是完全正确的。
一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。
3 自然数阶乘算法的递归实现及正确性证明
自然数阶乘的C语言递归程序P如下[1]：
int fact( int n )
{
int x = 1;
if ( n > 0 )
x = n * fact(n-1);
return x;
}
证：使用广义数学归纳法，容易证明程序正确，此处从略。
4 自然数阶乘算法的循环实现及正确性证明
自然数阶乘的C语言循环程序P如下[1]：
int fact( int y )
{
int x = 1;
while ( y > 0 )
x = y * x， y = y-1;
return x;
}
证：① 首先使用Hoare公理法证明程序部分正确性。
采用Hoare逻辑三元组描述程序为：
[ y ≥ 0 y = n ] F [x = n!] (4-1)
由此可见：P： y ≥ 0 y = n
Q： x = n!
首先， y > 0 x × y! = n! → y > 0 ( y × x ) × (y - 1)! = n! (4-2)
根据赋值公理，用 x 代替 y × x 可得到以下表达式：
[ y > 0 ( y × x ) × (y - 1)! = n! ] x = y * x [ y > 0 x × (y - 1)! = n! ] (4-3)
由式(4-2)和式(4-3)利用结论规则，可得
[ y > 0 x × y! = n! ] x = y * x [ y > 0 x × (y - 1)! = n! ] (4-4)
同理，由赋值公理可得
[ y > 0 x × (y - 1)! = n! ] y = y - 1 [ y ≥ 0 x × y! = n! ] (4-5)
由式(4-4)和式(4-5)利用順序规则，可得
[ y > 0 x × y! = n! ] x = y * x， y = y - 1 [ y ≥ 0 x × y! = n! ] (4-6)
根据式(4-6)，利用循环规则中 P = y > 0 x × y! = n!，R = y > 0，可得
[y ≥ 0 x × y! = n! ] while (y>0) x = y * x， y = y - 1 [ y≥0 x × y! = n! y≤0 ] (4-7)
因为 y = n x = 1 → x × y! = n! (4-8)
由式(4-7)和式(4-8)利用结论规则，可得
[ y ≥ 0 y = n x = 1] while (y > 0) x = y * x， y = y - 1 [ y≥0 x × y! = n! y≤0 ] (4-9)
又因为 0! = 1，所以
y ≥ 0 x × y! = n! y ≤ 0 → y=0 x × y! = n! → x = n! (4-10)
由式(4-9)和式(4-10)利用结论规则，可得
[ y ≥ 0 y = n x = 1 ] while ( y > 0 ) x = y * x， y = y - 1 [ x = n! ] (4-11)
根据赋值公理可得
[ y≥0 y = n] x = 1 [ y≥0 y = n x = 1 ] (4-12)
最后，由式(4-11)和式(4-12)利用顺序规则，可得
[ y ≥ 0 y = n ] x = 1; while ( y > 0 ) x = y * x， y = y - 1 [ x = n! ] (4-13)
可以看出，式(4-13)和式(4-1)相同且成立，程序的部分正确性得证。
② 再用 Kruth计数器方法证明程序终止性。
选取 N(y) = y
输入断言： I(y)： y > 0
当第一次进入循环时有 y > 0
根据程序算法容易看出：循环体内始终满足 y > 0，于是就有N(y) > 0;
而每执行一次循环，N(y)是递减的;
因而，循环只能执行有限次，必定终止，程序的终止性得证。
完全正确性：综合上述证明，程序是部分正确的且也是终止的，故程序是完全正确的。
5 结语
计算思维的形式化方法能够严格分析、处理、证明程序及其性质，对于确保程序正确性和提高可信性具有基础性的作用。当前，形式化方法教育已在欧美教育界进行了相关的实践，因此我国高校计算机教育强调计算思维的同时，更要注重其内涵形式化方法的教育作用。
参考文献：
[1] Paul Kelly等，双语版C程序设计[M]， 2017，电子工业出版社
[2]Jiangtao Geng etc. Research on Speeding up the Internationalization of Private High Vocational Education[J].International Journal of Technology Management 2017(4)：7-9
[3] Jeannette M. Wing. Computational Thinking[J]. Communication of the ACM. 2006， 49，(3)：33-35.
[4] 王戟等. 形式化方法概貌[J]. 软件学报， 2019， 30(01)：33-61.
[5] 何钦铭等.计算机基础教学的核心任务是计算思维能力的培养[J].中国大学教学，2010(9)： 5-9.
推荐阅读：如何投稿软件测试方面论文