立即尝试C ++ 20 Contract编程


在C ++ 20中,契约编程已经出现。 迄今为止,还没有编译器实现对此功能的支持。


但是,正如标准中所描述的那样,现在有一种方法可以尝试使用C ++ 20中的协定。


TL; DR


有一个支持合同的叉子c。 在他的示例中,我告诉您如何使用合约,以便一旦某个功能出现在您喜欢的编译器中,您就可以立即开始使用它。


关于合同程序设计的文章已经很多,但简而言之,我将告诉您它的用途以及用途。


灰白的逻辑


合同范式基于Hoar逻辑( 1,2 )。


灰白逻辑是形式上证明算法正确性的一种方式。
它以前置条件,后置条件和不变性等概念运行。
从实际的角度来看,使用Hoar的逻辑首先是一种在错误可能导致灾难或生命损失的情况下正式证明程序正确性的方法。 其次,一种增加程序可靠性的方法,以及静态分析和测试。


合同编制


1,2


合同的主要思想是,类似于业务合同,为每种功能或方法描述协议。 呼叫者和呼叫者都必须遵守这些安排。
合同不可分割的一部分是至少两种组装模式-调试和杂货。 合同的行为应取决于构建模式。 最常见的做法是在调试程序集中检查合同,而在杂​​货店中忽略它们。


有时,合同也会在产品组装中进行检查,例如,合同的未履行可能导致异常的产生。


与“经典”方法使用合同之间的主要区别在于,呼叫者必须遵守合同中描述的被呼叫者的前提条件,而呼叫者必须遵守其后置条件和不变式。
因此,被叫方不需要验证其参数的正确性。 该义务由合同分配给调用方。


应在测试阶段检测是否违反合同,并补充所有类型的测试:模块化集成等。


乍一看,合同的使用使开发更加困难,并降低了代码的可读性。 实际上,恰恰相反。 静态类型的坚持者会发现最容易评估合同的好处,因为他们最简单的选择是在方法和函数的签名中描述类型。


那么,合同的好处是什么:


  • 通过显式文档提高代码的可读性。
  • 通过补充测试来提高代码的可靠性。
  • 允许编译器使用低级优化并根据合同合规性生成更快的代码。 在后一种情况下,不遵守释放组件中的合同可能会导致UB。

C ++中的合同编程


合同编程以多种语言实现。 最引人注目的示例是Eiffel ,该范式最早在该范式中实现; D合同中的D是语言的一部分。


在C ++中,在C ++ 20标准之前,合同可用作单独的库。


这种方法有几个缺点:


  • 使用宏的语法非常笨拙。
  • 缺乏单一风格。
  • 编译器无法使用合同来优化代码。

库的实现通常基于对旧的assert和预处理器指令的使用,这些指令检查编译标志。


以这种形式使用合同确实会使代码难看且难以阅读。 这是为什么很少实践在C ++中使用合同的原因之一。


展望未来,我将展示合同使用在C ++ 20中的外观。
然后,我们将更详细地分析所有这些内容:


int f(int x, int y) [[ expects: x > 0 ]] // precondition [[ expects: y > 0 ]] // precondition [[ ensures r: r < x + y ]] // postcondition { int z = (x - x%y) / y; [[ assert: z >= 0 ]]; // assertion return z + y; } 

试一下


不幸的是,目前,尚未被广泛使用的编译器尚未实现合同支持。
但是有一个出路。


马德里卡洛斯三世大学的 ARCOS研究小组对c ++ ++分支中的合同实施了实验性支持。


为了不“在纸上写代码”,而是为了能够立即尝试新的业务机会,我们可以收集此fork并将其用于下面的示例。


汇编说明在github存储库的自述文件中进行了描述
https://github.com/arcosuc3m/clang-contracts


 git clone https://github.com/arcosuc3m/clang-contracts/ mkdir -p clang-contracts/build/ && cd clang-contracts/build/ cmake -G "Unix Makefiles" -DLLVM_USE_LINKER=gold -DBUILD_SHARED_LIBS=ON -DLLVM_USE_SPLIT_DWARF=ON -DLLVM_OPTIMIZED_TABLEGEN=ON ../ make -j8 

我在组装过程中没有任何问题,但是编译源代码需要很长时间。


要编译示例,您将需要显式指定clang ++二进制文件的路径。
例如,对我来说看起来像这样


 /home/valmat/work/git/clang-contracts/build/bin/clang++ -std=c++2a -build-level=audit -g test.cpp -o test.bin 

我准备了一些示例,以使您可以方便地使用实际代码示例检查合同。 我建议您在开始阅读下一部分之前,先克隆并编译示例。


 git clone https://github.com/valmat/cpp20-contracts-examples/ cd cpp20-contracts-examples make CPP=/path/to/clang++ 

/path/to/clang++实验性编译器程序集的clang++二进制文件/path/to/clang++路径。


除了编译器本身之外,ARCOS研究小组还为其分支准备了他们的Compiler Explorer版本。


C ++ 20中的合同编程


现在,没有什么可以阻止我们开始研究合同编程提供的可能性,并立即在实践中尝试这些机会。


如上所述,合同是根据前提条件,后置条件和不变式(陈述)构建的。


在C ++ 20中,为此使用具有以下语法的属性


 [[contract-attribute modifier identifier: conditional-expression]] 

contract-attribute可以采用以下值之一:
期望确保主张


expects用于前置条件, ensures用于后置条件,并用于声明。


conditional-expression是在合同谓词中经过验证的布尔表达式。
modifieridentifier可以省略。


为什么我需要一个modifier我会写得更低一些。


identifier仅与ensures使用,并用于表示返回值。


前提条件可以访问参数。


后置条件可以访问该函数返回的值。 语法用于此目的。


 [[ensures return_variable: expr(return_variable)]] 

其中return_variable该变量的任何有效表达式。


换句话说,先决条件旨在声明对函数接受的参数施加的限制,而后条件旨在声明对函数返回的值施加的限制。


相信前提条件后置条件是功能接口的一部分,而语句是其实现的一部分。


前提条件谓词总是在执行函数之前立即进行评估。 在控制功能传递到调用代码后,立即满足后置条件。


如果在函数中引发异常,则将不检查后置条件。
仅在功能正常完成时才检查后置条件。


如果在检查合同中的表达式时发生异常,则将调用std::terminate()


前提条件和后置条件总是在函数体之外描述,并且无法访问局部变量。


如果前提条件和后置条件描述了公共类方法的合同,则它们不能访问私有和受保护的类字段。 如果类方法受保护,则可以访问该类的受保护的公共数据,但不能访问私有数据。
最后一个限制是完全合乎逻辑的,因为合同是方法接口的一部分。


语句(不变量)始终在函数或方法的主体中进行描述。 通过设计,它们是实现的一部分。 因此,他们可以访问所有可用数据。 包括局部函数变量以及私有和受保护的类字段。


例子1


我们定义了两个前提条件,一个后置条件和一个不变式:


 int foo(int x, int y) [[ expects: x > y ]] // precondition #1 [[ expects: y > 0 ]] // precondition #2 [[ ensures r: r < x ]] // postcondition #3 { int z = (x - x%y) / y; [[ assert: z >= 0 ]]; // assertion return z; } int main() { std::cout << foo(117, 20) << std::endl; std::cout << foo(10, 20) << std::endl; // <-- contract violation #1 std::cout << foo(100, -5) << std::endl; // <-- contract violation #2 return 0; } 

例子2


公共方法的先决条件不能引用受保护或私有字段:


 struct X { //protected: int m = 5; public: int foo(int n) [[expects: n < m]] { return n*n; } }; 

不允许在合同属性所描述的表达式中修改变量。 如果损坏,将有UB。


合同中描述的表达不应有副作用。 尽管编译器可以验证这一点,但他们并不需要这样做。 违反此要求被视为未定义行为。


 struct X { int m = 5; int foo(int n) [[ expects: n < m++ ]] // UB: Modifies variable m { int k = n*n; [[ assert: ++k < 100 ]] // UB: Modifies variable k return n*n; } }; 

当我谈论合同修饰符和构建模式的级别时,不更改合同表达式中程序状态的要求将变得明显降低。


现在我只注意到正确的程序应该就像没有任何合同一样工作。


如上所述,在合同中,您可以指定任意多个前提条件和后置条件。
所有这些都将按顺序检查。 但是始终在执行函数之前检查先决条件,并在退出函数后立即检查后置条件。


这意味着始终先检查前提条件,如以下示例所示:


 int foo(int n) [[ expects: expr(n) ]] // # 1 [[ ensures r: expr(r) ]] // # 4 [[ expects: expr(n) ]] // # 2 [[ expects: expr(n) ]] // # 3 [[ ensures r: expr(r) ]] // # 5 {...} 

后置条件中的表达式不仅可以引用函数返回的值,还可以引用函数的参数。


 int foo(int &n) [[ ensures: expr(n) ]]; 

在这种情况下,您可以省略返回值标识符。


如果后置条件引用了函数的自变量,则与先决条件一样,该自变量在函数的退出点而不是入口点被考虑。


在后置条件中无法引用原始(在函数入口点)值。


例如


 void incr(int &n) [[ expects: 3 == n ]] [[ ensures: 4 == n ]] {++n;} 

合同中的谓词只能在局部变量的生存期与谓词计算时间相对应的情况下引用局部变量。


例如,对于constexpr函数,除非在编译时已知局部变量,否则无法引用它们。


例如


 int a = 1; constexpr int b = 100; constexpr int foo(int n) [[ expects: a <= n ]] // error: `a` is not constexpr [[ expects: n < b ]] // OK { [[assert: n > 2*a]]; // error: `a` is not constexpr [[assert: n < 2*b]]; // OK return 2*n; } 

函数指针的合同


您不能为函数指针定义协定,但是可以将为其定义协定的函数的地址分配给函数指针。


例如


 int foo(int n) [[expects: n < 10]] { return n*n; } int (*pfoo)(int n) = &foo; 

调用pfoo(100)将违反合同。


继承合同


合同概念的经典实现表明,子类中的先决条件可以弱化,子类中的后置条件和不变性可以增强。


在C ++ 20实现中,情况并非如此。


首先,C ++ 20中的不变量是实现的一部分,而不是接口。 因此,它们既可以增强也可以减弱。 如果虚拟函数实现中没有assert ,那么它将不会被继承。


其次,要求在继承功能时, ODR必须相同。
并且,由于前置条件和后置条件是接口的一部分,因此在继承人中它们必须完全匹配。


此外,可以省略继承过程中对先决条件和后置条件的描述。 但是,如果声明了它们,则它们必须与基类中的定义完全匹配。


例如


 struct Base { virtual int foo(int n) [[ expects: n < 10 ]] [[ ensures r: r > 100 ]] { return n*n; } }; struct Derived1 : Base { virtual int foo(int n) override [[ expects: n < 10 ]] [[ ensures r: r > 100 ]] { return n*n*2; } }; struct Derived2 : Base { // Inherits contracts from Base virtual int foo(int n) override { return n*3; } }; 

备注

不幸的是,上面的示例在实验性编译器中无法按预期工作。


如果来自Derived2 foo Derived2合同,那么它将不会从基类继承。 此外,编译器允许您为子类确定与基本合同不匹配的合同。


另一个实验性的编译器错误


该记录在语法上应该正确


 virtual int foo(int n) override [[expects: n < 10]] {...} 

但是,以这种形式,我收到了编译错误


 inheritance1.cpp:20:36: error: expected ';' at end of declaration list virtual int foo(int n) override ^ ; 

并且必须替换为


 virtual int foo(int n) [[expects: n < 10]] override {...} 

我认为这是由于实验性编译器的特殊性,语法正确的代码将在编译器的发行版中运行。


合约修正


合同谓词检查可能会产生额外的处理成本。
因此,通常的做法是在开发和测试版本中检查合同,而在发布版本中忽略它们。


为此,该标准提供了三个级别的合同修改器。 使用修饰符和编译器键,程序员可以控制在装配体中检查哪些触点以及忽略哪些触点。


  • default -默认情况下使用此修饰符。 假定与使用函数本身的计算成本相比,使用此修饰符验证表达式执行的计算成本较小
  • audit -此修饰符假定验证表达式执行的计算量与计算函数本身的量相比是可观的
  • axiom -如果表达式是声明性的,则使用此修饰符。 在运行时未检查。 用于记录函数接口,供静态分析器和编译器优化器使用。 带有axiom修饰符的表达式永远不会在运行时求值。

例子


 [[expects: expr]] //  default [[expects default: expr]] //  default [[expects axiom : expr]] // Run-time    [[expects audit : expr]] //    

使用修饰符,可以确定哪些检查将使用哪些程序集版本以及哪些检查将被禁用。


值得注意的是,即使不执行检查,编译器也有权使用合同进行低级优化。 尽管可以通过编译标志禁用合同验证,但是违反合同会导致未定义的程序行为。


由编译器决定,可以提供一些工具来axiom标记为axiom表达式。


在我们的例子中,这是一个编译器选项


 -axiom-mode=<mode> 

-axiom-mode=on 打开公理模式,并因此关闭对具有标识符axiom的声明的验证,


-axiom-mode=off 关闭公理模式并因此启用验证标识符为axiom的语句。


例如


 int foo(int n) [[expects axiom: n < 10]] { return n*n; } 

可以使用三种不同的验证级别来编译程序:


  • off关闭合同中的所有表达式检查
  • 仅检查具有default修饰符的default表达式
  • 使用defaultaudit修饰符执行所有检查时, audit高级模式

编译器开发人员可以自行决定如何准确实现验证级别的安装。


在我们的情况下,为此使用了编译器选项


 -build-level=<off|default|audit> 

默认值为-build-level=default


如前所述,编译器可以使用协定进行低级优化。 因此,尽管在执行时可能未计算合同中的某些谓词(取决于验证级别),但它们的不履行导致不确定的行为。


我将把装配级应用的示例推迟到下一部分,使它们可视化。


截取违约


根据程序要使用的选项,在违反合同的情况下,可能会有不同的行为方案。


默认情况下,违反合同会导致程序崩溃,调用std::terminate() 。 但是,程序员可以通过提供自己的处理程序并向编译器指示在违反合同后有必要继续执行程序来覆盖此行为。


在编译时,您可以安装违反处理程序 ,在违反合同时调用该处理程序


编译器的创建者可以自行决定实现处理程序安装的方式。


就我们而言


 -contract-violation-handler=<violation_handler> 

处理器签名应为


 void(const std::contract_violation& info) 


 void(const std::contract_violation& info) noexcept 

std::contract_violation等效于以下定义:


 struct contract_violation { uint_least32_t line_number() const noexcept; std::string_view file_name() const noexcept; std::string_view function_name() const noexcept; std::string_view comment() const noexcept; std::string_view assertion_level() const noexcept; }; 

因此,处理程序使您可以获得有关合同违约发生的确切时间和条件的全面信息。


如果指定了冲突处理程序处理程序 ,则在违反合同的情况下,默认情况下,默认情况下,执行后将立即调用std::abort() (不指定处理程序,将调用std::terminate() )。


该标准假定编译器提供了允许程序员在违反合同后继续执行程序的工具。


编译器开发人员可以自行决定实现这些工具的方式。
在我们的例子中,这是一个编译器选项


 -fcontinue-after-violation 

可以在相互独立的情况下设置-fcontinue-after-violation-fcontinue-after-violation -contract-violation-handler 。 例如,您可以设置-fcontinue-after-violation ,但不能设置-contract-violation-handler 。 在后一种情况下,违反合同后,该程序将继续运行。


标准规定了在违反合同后继续执行程序的能力,但是必须小心使用此功能。


从技术上讲,即使程序员明确指出程序应继续运行,也未定义程序在违反合同后的行为。


这是由于编译器能够基于合同执行来执行低级优化。


理想情况下,如果发生违反合同的情况,则需要尽快记录诊断信息并终止程序。 您需要通过让程序在违规后正常工作来确切地了解您在做什么。


定义您的处理程序并使用它来拦截违约行为


 void violation_handler(const std::contract_violation& info) { std::cerr << "line_number : " << info.line_number() << std::endl; std::cerr << "file_name : " << info.file_name() << std::endl; std::cerr << "function_name : " << info.function_name() << std::endl; std::cerr << "comment : " << info.comment() << std::endl; std::cerr << "assertion_level : " << info.assertion_level() << std::endl; } 

考虑一个违反合同的例子


 #include "violation_handler.h" int foo(int n) [[expects: n < 10]] { return n*n; } int main() { foo(100); // <-- contract violation return 0; } 

我们使用选项-contract-violation-handler=violation_handler -fcontinue-after-violation-fcontinue-after-violation编译程序并运行


 $ bin/example8-handling.bin line_number : 4 file_name : example8-handling.cpp function_name : foo comment : n < 10 assertion_level : default 

现在我们可以举一些例子说明在不同组装级别和合同模式下违反合同的情况下程序的行为。


考虑以下示例


 #include "violation_handler.h" int foo(int n) [[ expects axiom : n < 100 ]] [[ expects default : n < 200 ]] [[ expects audit : n < 300 ]] { return 2 * n; } int main() { foo(350); // audit foo(250); // default return 0; } 

如果使用-build-level=off选项进行构建, -build-level=off预期,将不检查合同。


收集default级别(使用选项-build-level=default ),我们得到以下输出:


 $ bin/example9-default.bin line_number : 5 file_name : example9.cpp function_name : foo comment : n < 200 assertion_level : default line_number : 5 file_name : example9.cpp function_name : foo comment : n < 200 assertion_level : default 

具有audit级别的程序集将给出:


  $ bin/example9-audit.bin line_number : 5 file_name : example9.cpp function_name : foo comment : n < 200 assertion_level : default line_number : 6 file_name : example9.cpp function_name : foo comment : n < 300 assertion_level : audit line_number : 5 file_name : example9.cpp function_name : foo comment : n < 200 assertion_level : default 

备注


violation_handler可能会引发异常。 在这种情况下,您可以配置程序,以便违反合同会导致引发异常。


如果描述了合同的函数标记为noexcept并且在检查合同时会抛出异常,则调用noexcept会引发异常。


例子


 void violation_handler(const std::contract_violation&) { throw std::exception(); } int foo(int n) noexcept [[ expects: n > 0 ]] { return n*n; } int main() { foo(0); // <-- std::terminate() when violation handler throws an exception return 0; } 

如果将标志传递给编译器:打破合同后不要继续执行程序( continuation mode=off ),但是违反处理程序将引发异常,则将强制执行std::terminate()


结论


合同与非侵入式运行时检查有关。 它们在确保发布的软件质量方面起着非常重要的作用。


C ++的使用非常广泛。 并且可以肯定的是,有足够数量的合同说明索赔。 从我的主观观点来看,该实现非常方便且直观。


C ++ 20合同将使我们的程序更加可靠,快速和易于理解。 我期待它们在编译器中的实现。




聚苯乙烯
在PM中,他们告诉我,在标准的最终版本中, expectsensures可能ensuresprepost代替。

Source: https://habr.com/ru/post/zh-CN443766/


All Articles