断言 (程序)
![本页使用了标题或全文手工转换](http://upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Zh_conversion_icon_m.svg/35px-Zh_conversion_icon_m.svg.png)
此条目需要补充更多来源。 (2015年7月19日) |
在程式设计中,断言(assertion)是一种放在程序中的一阶逻辑(如一个结果为真或是假的逻辑判断式),目的是为了标示与验证程序开发者预期的结果-当程序执行到断言的位置时,对应的断言应该为真。若断言不为真时,程序会中止执行,并给出错误消息。
例如,以下的程序包括二个断言:
x := 5;
{x > 0}
x := x + 1
{x > 1}
x > 0
及x > 1
,当程序执行到二个断言对应的位置时,断言的内容均为真。
程式设计者可以用断言来标示程序,提供程序正确性的相关资讯。例如在一段程序前加入断言(先验条件),说明这段程序执行前预期的状态。或在一段程序后加入断言(后验条件),说明这段程序执行后预期的结果。
以下的示例使用东尼·霍尔在1969年论文中提出的断言标示方式[1]。
x = 5;
x = x + 1;
// {x > 1}
以上注解中的大括号表示为断言,不是一般的注解。现有的主流编程语言不支持上述的标示方式,不过程式设计者仍可以用注解的方式标示断言,标示此时应该成立的条件,只是此断言没有检查机能,不成立时程序不会中止执行。
许多现代的编程语言已支持有检查机能的断言,可能是执行期或其他时间检查的陈述。若在执行期中有断言不成立,会出现断言失败,一般会停止程序的执行。程式设计者可以专注在断言失败,逻辑不一致的部分,并设法修正。
断言的使用有助于程式设计者设计、开发及理解程序。
用途
[编辑]在开发Eiffel语言的程序时,断言是设计过程中的一部分。像C语言或Java等编程语言,主要在执行期检查断言是否正确,也可以用静态断言的方式,在编译期检查断言。不论是哪一种情形,都可以检查断言的有效性,也可以关闭断言检查的机能。
契约式设计中的断言
[编辑]断言可以当做是一种软件的文档:断言可以描述程序执行前预期的情形(先验条件)以及执行后的预期的结果(后验条件)。断言也可以描述类别中的不变量。Eiffel编程语言将断言和程序集成,也可以自动将程序中的断言抽出,形成程序的文件。这是契约式设计的重要特性。以下是一个Eiffel语言的程序,其中require
及ensure
分别标示程序的先验条件及后验条件。
set_hour (a_hour: INTEGER)
-- Set `hour' to `a_hour'
require
valid_argument: a_hour >= 0 and a_hour <= 23
do
hour := a_hour
ensure
hour_set: hour = a_hour
end
断言可以用叙述的方式放在程序中,也可以用注解的方式标示。不过断言若用注解的方式标示,在断言和程序未同步更新时比较容易让设计者发现问题。有断言叙述的程序会可以在每次程序执行时,自动检查断言是否成立,若断言不成立时,就会输出错误消息。因此避免了程序和断言未同步更新的问题。
执行期检查的断言
[编辑]在程序执行时,可以用断言检查程序开发时的假设,确认这些假设是否成立。考虑以下的Java程序:
int total = countNumberOfUsers();
if (total % 2 == 0) {
// total is even
} else {
// total is odd and non-negative
assert(total % 2 == 1);
}
在Java语言中,%
为余数的运算符,若其第一个操作数为负,其结果也为负值。程式设计者假设total
为非负值,因此除以2的余数只可能是0或是1,使用断言可以使这个假设变得明确,若countNumberOfUsers
传回负值,程序会出现错误。
此作法的最大好处是当程序出现错误时,程序立刻停止执行,而不会在较晚的时间才中止执行,而断言错误时会回报错误代码的位置,因此程序设人计者可以很快找到错误所在的位置。
断言有时也会放在程序未预期会执行到的部分。例如,若switch
叙述中所有可能的状态都有对应的case
叙述,不会执行到default
叙述,此时可以在default
叙述中加入一个条件不会成立的断言,当程序执行到default
叙述时会立刻停止执行,而不会使程序继续在一个错误的状态下执行。
Java语言在1.4版以后支持断言机能,若程序执行时有设置对应旗标,断言错误时会产生AssertionError
,若未设置对应旗标,则会省略断言叙述。C语言的断言是在标准的开头档assert.h
中定义,其断言 assert (assertion)
是一个宏,若条件不成立时产生错误,并且中止程序执行。C++语言的断言需配合开头档cassert
,不过有些C++的函数库也开头档assert.h
。
上述断言的缺点是可能有改变存储器资料或是线程时序的风险,因此需小心的处理断言,确认断言在程序中没有其他的副作用。
程序结构中的断言有助于在不使用第三方程式库的情形下,应用测试驱动开发的开发方式。
在开发过程中使用断言
[编辑]在软件开发过程中,程式设计者一般会在断言有效的情形下执行或测试程序。若出现断言错误,程式设计者会立刻注意到此问题。许多断言的实现方式会中止程序的执行,这功能方便程式设计者处理问题,若在错误出现后程序继续执行,往往更不容易找到有问题程序的位置。断言错误一般也会显示一些资讯,例如错误程序的位置,也许包括堆栈追踪,若环境支持核心文件或是在调试工具中执行,可能还可以提供程序的完整状态,程式设计者可以配合这些资讯来修正程序的错误,是在调试过程中很有利的工具。
静态断言
[编辑]只在编译期间检查的断言称为静态断言,静态断言必需配合清楚的注解说明。
在编译期的模板超编程时,静态断言特别有用。静态断言也可以用在C语言的程序中,当断言不成立时,产生有错误的代码。例如以下就是一个定义静态断言的方法:
#define COMPILE_TIME_ASSERT(pred) switch(0){case 0:case pred:;}
COMPILE_TIME_ASSERT( BOOLEAN CONDITION );
若(BOOLEAN CONDITION)
的成果不为真,上述程序中会有二个相同的case标记,因此编译器会出现错误。此处的布尔逻辑式是要在编译阶段就可以确定的表达式,例如(sizeof(int)==4)
等。此结构无法放在函数范围以外,因此若要执行此断言时,必需将此断言放在一个函数以内。
另一个常使用的静态断言方式如下[2]:
static char const static_assertion[ (BOOLEAN CONDITION)
? 1 : -1
] = {'!'};
若(BOOLEAN CONDITION)
的成果不为真,由于无法定义长度为负值的数组,因此编译器会出现错误。即使编译器真的允许负值长度,后续的初始化字符应该也会使编译器出现错误消息。此处的布尔逻辑式是要在编译阶段就可以确定的表达式,例如(sizeof(int)==4)
等。
上述的方式都需要唯一不重复的名称。现代的编译器支持__COUNTER__的预处理器定义,在每次使用到此定义时,回传一个每次会加一的数值,因此可以产生唯一不重复的名称[3]。
C11 (程序标准版本)及C++11可以用static_assert
支持静态断言。
关闭断言机能
[编辑]大部分的编程语言可以用设置启动或关闭所有的断言,有时也可以启动或关闭个别的断言。一般会在开发过程中启动断言,在最后测试完成,要发行正式版本给客户时会关闭断言。在不考虑断言副作用的前提下,关闭断言不作检查可以节省评估断言需要的代码,在正常情形下程序仍有相同的结果。在异常的情形下,关闭断言检查会使得原来可能会停止的程序可以继续执行,有时这会是比较可接受的结果。
C语言及C++可以利用预处理器在编译阶段完全关闭断言。Java语言若要启动断言,需要在运行期引擎中设置特定选项,若选项未设置,不会启动断言,不过断言仍存在程序中,只有在用在运行期用JIT编译器中进行优化,或是在编译期使用if(false)的条件,才能排除断言执行。
和错误处理的比较
[编辑]有必要去区分断言和错误进程的差异。断言只用在标示一些逻辑上不可能或不应该出现的情形,若上述情形真的出现时,表示有些基本架构已出现问题。这和错误处理不同,大部分错误的条件都是有可能出现的,只是实务上出现频率很低。断言不宜作为通用的错误进程,因为断言一般会中止程序的执行,程序无法恢复到没有错误发生前的情形,而且断言显示的消息只对程式设计者有帮助,对用户的帮助不大。
考虑以下用断言处理错误的程序。
int *ptr = malloc(sizeof(int) * 10);
assert(ptr);
// use ptr
...
操作系统不保证每一次执行malloc
都会成功,若无法配置到存储器,malloc
会传回NULL
pointer,程序会立刻中止执行。
比较理想的错误处理方式是配置到存储器时另外由程序处理。例如伺服器可能有数个客户端,可能有一些资源保留,尚未释放,也可能有一些修改尚未写入数据库。此时较好的处理方法只让单一的交易失败,出现错误消息,而不是直接中止程序的执行。
相关条目
[编辑]参考资料
[编辑]- ^ C.A.R. Hoare, An axiomatic basis for computer programming (页面存档备份,存于互联网档案馆), Communications of the ACM, 1969.
- ^ Jon Jagger, Compile Time Assertions in C (页面存档备份,存于互联网档案馆), 1999.
- ^ GNU, "GCC 4.3 Release Series — Changes, New Features, and Fixes (页面存档备份,存于互联网档案馆)"
外部链接
[编辑]- The benefits of programming with assertions (页面存档备份,存于互联网档案馆) by Philip Guo (Stanford University), 2008.
- Java: