断言 (程式)

本页使用了标题或全文手工转换
维基百科，自由的百科全书

在程式设计中，断言（assertion）是一种放在程式中的一阶逻辑（如一个结果为真或是假的逻辑判断式），目的是为了标示与验证程式开发者预期的结果－当程式执行到断言的位置时，对应的断言应该为真。若断言不为真时，程式会中止执行，并给出错误讯息。

例如，以下的程式包括二个断言： 

x := 5;
{x > 0}
x := x + 1
{x > 1}

x > 0及x > 1，当程式执行到二个断言对应的位置时，断言的内容均为真。

程式设计者可以用断言来标示程式，提供程式正确性的相关资讯。例如在一段程式前加入断言（先验条件），说明这段程式执行前预期的状态。或在一段程式后加入断言（后验条件（英语：postcondition）），说明这段程式执行后预期的结果。

以下的范例使用东尼·霍尔在1969年论文中提出的断言标示方式[1]。 

x = 5;
x = x + 1;
// {x > 1}

以上注解中的大括号表示为断言，不是一般的注解。现有的主流程式语言不支援上述的标示方式，不过程式设计者仍可以用注解的方式标示断言，标示此时应该成立的条件，只是此断言没有检查机能，不成立时程式不会中止执行。

许多现代的程式语言已支援有检查机能的断言，可能是执行期或其他时间检查的陈述。若在执行期中有断言不成立，会出现断言失败，一般会停止程式的执行。程式设计者可以专注在断言失败，逻辑不一致的部份，并设法修正。

断言的使用有助于程式设计者设计、开发及理解程式。

用途[编辑]

在开发Eiffel语言的程式时，断言是设计过程中的一部份。像C语言或Java等程式语言，主要在执行期检查断言是否正确，也可以用静态断言的方式，在编译期检查断言。不论是哪一种情形，都可以检查断言的有效性，也可以关闭断言检查的机能。

契约式设计中的断言[编辑]

断言可以当做是一种软体的文档：断言可以描述程式执行前预期的情形（先验条件）以及执行后的预期的结果（后验条件（英语：postcondition））。断言也可以描述类别中的不变量。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 (程式标准版本)（英语：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，程式会立刻中止执行。

比较理想的错误处理方式是配置到记忆体时另外由程式处理。例如伺服器可能有数个客户端，可能有一些资源保留，尚未释放，也可能有一些修改尚未写入资料库。此时较好的处理方法只让单一的交易失败，出现错误讯息，而不是直接中止程式的执行。

相关条目[编辑]

参考资料[编辑]

  1. ^ C.A.R. Hoare, An axiomatic basis for computer programming （页面存档备份，存于互联网档案馆）, Communications of the ACM, 1969.
  2. ^ Jon Jagger, Compile Time Assertions in C （页面存档备份，存于互联网档案馆）, 1999.
  3. ^ GNU, "GCC 4.3 Release Series — Changes, New Features, and Fixes （页面存档备份，存于互联网档案馆）"

外部链接[编辑]

取自“https://zh.wikipedia.org/w/index.php?title=斷言_(程式)&oldid=75128403”