In C ++ 20 contract programming appeared. At the moment, no compiler has yet implemented support for this feature.
But there is a way to try to use contracts from C ++ 20 right now, as it is described in the standard.
There is fork clang supporting contracts. On his example, I tell you how to use contracts so that as soon as the feature appears in your favorite compiler, you can immediately start using it.
A lot has already been written about contract programming, but in a nutshell I’ll tell you what it is and why you need it.
The contract paradigm is based on the logic of Hoare ( 1 , 2 ).
Hoar's logic is a way to formally prove the correctness of an algorithm.
It operates with such concepts as precondition, postcondition and invariant.
From a practical point of view, the use of Hoar’s logic is, firstly, a way to formally prove the correctness of a program in cases where errors can lead to a catastrophe or death. Secondly, a way to increase the reliability of the program, along with static analysis and testing.
The basic idea of ​​contracts is that by analogy with contracts in business, agreements are described for each function or method. These arrangements must be respected by both the caller and the callee.
An integral part of the contract is at least two modes of assembly - debugging and grocery. Depending on the build mode, contracts must behave differently. The most common practice is to check contracts in the debug build and ignore them in the grocery.
Sometimes in a product assembly contracts are also checked and their non-fulfillment may, for example, lead to an exception being thrown.
The main difference between the use of contracts from the "classic" approach is that the caller must comply with the caller's preconditions, which are described in the contract, and the callee must abide by his post-conditions and invariants.
Accordingly, the called party is not obliged to check the correctness of its transmitted parameters. This obligation is imposed by the contract to the caller.
Noncompliance with contracts must be detected at the testing stage and complements all types of tests: modular integration, etc.
At first glance, the use of contracts leads to more complicated development and degrades the readability of the code. In fact, everything is just the opposite. Adherents of static typing will be the easiest to evaluate the benefits of contracts, because the simplest option is to describe types in the signature of methods and functions.
So, what benefits give contracts:
Contract programming is implemented in many languages. The most prominent examples are Eiffel , where the paradigm was first implemented, and D , in D, contracts are part of the language.
In C ++, up to the standard C ++ 20, contracts could be used as separate libraries.
This approach has several disadvantages:
Library implementations are usually based on the use of the good old assert and preprocessor directives that check for the presence of a compilation flag.
Using contracts in this form really makes the code ugly and unreadable. This is one of the reasons why contracting is little practiced in C ++.
Looking ahead, I'll show you how in C ++ 20 the use of contracts will look.
And then, let's look at all this in more detail:
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; }
Unfortunately, at the moment none of the widely used compilers have yet implemented contract support.
But there is a way out.
The ARCOS research group from the Universidad Carlos III de Madrid implemented experimental support for contracts in the fork of clang ++.
In order not to “write code on a piece of paper,” but to have the opportunity to immediately try new possibilities in business, we can assemble this fork and use it to try the examples given below.
Assembly instructions are described in the Github repository readme.
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
I did not have any problems with the build, but compiling the source takes a lot of time.
To compile the examples, you will need to explicitly specify the path to the clang ++ binary.
For example, I have it looks like this
/home/valmat/work/git/clang-contracts/build/bin/clang++ -std=c++2a -build-level=audit -g test.cpp -o test.bin
I prepared examples for you to conveniently explore contracts with real code examples. I suggest, before starting the next section, to clone and compile the examples.
git clone https://github.com/valmat/cpp20-contracts-examples/ cd cpp20-contracts-examples make CPP=/path/to/clang++
Here /path/to/clang++
path to the clang++
binary of your experimental compiler build.
In addition to the compiler itself, the ARCOS research group prepared their own version of the Compiler Explorer for their fork.
Now nothing prevents us from starting to explore the possibilities offered by contract programming, and immediately try these possibilities in action.
As mentioned above, contracts are built from preconditions, postconditions and invariants (statements).
In C ++ 20, attributes with the following syntax are used for this.
[[contract-attribute modifier identifier: conditional-expression]]
Where contract-attribute
can be one of the following values:
expects , ensures or assert .
expects
used for preconditions, ensures
for postconditions and assert
for statements.
conditional-expression
is a boolean expression that is checked in a predicate contract.modifier
and identifier
may be omitted.
Why do I need a modifier
I will write below.
identifier
used only with ensures
and serves to represent the return value.
Preconditions have access to arguments.
Postconditions have access to the value returned by the function. To do this, use the syntax
[[ensures return_variable: expr(return_variable)]]
Where return_variable
any valid expression for a variable.
In other words, the preconditions are intended to declare the constraints imposed on the arguments taken by the function, and the postconditions to declare the constraints imposed on the return value of the function.
Preconditions and postconditions are considered to be part of the function interface, while statements are part of its implementation.
Predicates preconditions are always calculated immediately before the execution of the function. Postconditions are executed immediately after being passed by the control function to the calling code.
If an exception is thrown in the function, the postconditions will not be checked.
Postconditions are checked only in case of normal completion of the function.
If an exception is raised while checking the expression in the contract, then std::terminate()
will be called.
Preconditions and postconditions are always described outside the function body and cannot access local variables.
If preconditions and postconditions describe a contract for a public class method, they cannot have access to private and protected class fields. If the class method is protected, then there is access to the protected and public data of the class, but there is no private one.
The last restriction is completely logical, given that the contract is part of the method interface.
Statements (invariants) are always described in the body of a function or method. By design, they are part of the implementation. And, accordingly, can have access to all available data. This includes local function variables and private and protected class fields.
We define two preconditions, one post-condition and one invariant:
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; }
The public method precondition cannot refer to a protected or private field:
struct X { //protected: int m = 5; public: int foo(int n) [[expects: n < m]] { return n*n; } };
Modification of variables inside expressions described by contract attributes is not allowed. If this is broken, it will be UB.
The expressions described in the contracts should not have side effects. Although compilers can verify this, this is not their responsibility. Violation of this requirement is considered unspecified behavior.
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; } };
The requirement not to change the state of the program in contract expressions will become obvious a little lower when I talk about contract modifier levels and assembly modes.
Now I’ll just note that the correct program should work just as if there were no contracts at all.
As I noted above, in the contract you can specify any number of preconditions and postconditions.
All of them will be checked in order. But preconditions are always checked before executing the function, and postconditions immediately after exiting it.
This means that the preconditions are always checked first, as illustrated in the following example:
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 {...}
Expressions in postconditions can refer not only to the return value of the function, but also to the arguments of the function.
int foo(int &n) [[ ensures: expr(n) ]];
In this case, you can omit the return value ID.
If a postcondition refers to a function argument, then this argument is considered at the exit point of the function , and not at the entry point, as is the case with preconditions.
There is no way to refer to the original (at the function entry point) value in a postcondition.
example :
void incr(int &n) [[ expects: 3 == n ]] [[ ensures: 4 == n ]] {++n;}
Predicates in contracts can refer to local variables only if the lifetime of these variables corresponds to the predicate's computation time.
For example, for constexpr
functions, you cannot refer to local variables unless they are known at compile time.
example :
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; }
You cannot define contracts for a function pointer, but you can assign a function pointer to the address of the function for which the contract is defined.
example :
int foo(int n) [[expects: n < 10]] { return n*n; } int (*pfoo)(int n) = &foo;
Calling pfoo(100)
will violate the contract.
The classic implementation of the concept of contracts suggests that preconditions can be relaxed in subclasses, postconditions and invariants can be strengthened in subclasses.
In a C ++ implementation, this is not the case.
First, invariants in C ++ 20 are part of the implementation, not the interface. For this reason, they can be both strengthened and weakened. If there is no assert
in the implementation of the virtual function, it will not be inherited.
Secondly, it is required that when inheriting a function, the ODRs are identical.
And, since the preconditions and postconditions are part of the interface, then in the heir they must be exactly the same.
At the same time, the description of preconditions and postconditions for inheritance can be omitted. But if they are declared, they must exactly match the definition in the base class.
example :
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; } };
Unfortunately, the example above does not work in the experimental compiler as expected.
If the foo
from Derived2
contract, it will not be inherited from the base class. In addition, the compiler allows you to determine for a subclass a contract that does not match the base contract.
Another experimental compiler error :
the syntax should be correct
virtual int foo(int n) override [[expects: n < 10]] {...}
However, in this form, I received a compilation error
inheritance1.cpp:20:36: error: expected ';' at end of declaration list virtual int foo(int n) override ^ ;
and had to be replaced by
virtual int foo(int n) [[expects: n < 10]] override {...}
I think this is due to the peculiarity of the experimental compiler, and syntax correct code will work in the release versions of compilers.
Verification of contract predicates may incur additional computational costs.
Therefore, it is common practice to check contracts in the developer and test builds and ignore them in the release build.
For these purposes, the standard offers three levels of contract modifiers. With the help of modifiers and compiler keys, the programmer can control which contacts will be checked in the assembly, and which ones will be ignored.
default
- this modifier is used by default. It is assumed that the computational cost of checking the execution of an expression with this modifier is small compared with the cost of calculating the function itself.audit
- this modifier assumes that the computational cost of checking the execution of an expression is significant compared to the cost of calculating the function itself.axiom
- this modifier is used if the expression is declarative. Not checked at runtime. It is used to document the interface of a function, to be used by static analyzers and the compiler optimizer. Expressions with the axiom
modifier axiom
never evaluated at run time.Example
[[expects: expr]] // default [[expects default: expr]] // default [[expects axiom : expr]] // Run-time [[expects audit : expr]] //
Using modifiers, you can determine which checks in which versions of your builds will be used and which ones will be disabled.
It should be noted that even if the check is not performed, the compiler has the right to use the contract for low-level optimizations. And although contract verification can be disabled with a compilation flag, contract violation leads to undefined program behavior.
At the discretion of the compiler, means may be provided to include checking expressions marked as axiom
.
In our case, this is a compiler option.
-axiom-mode=<mode>
-axiom-mode=on
enables the axioms mode and, accordingly, turns off the verification of assertions with the identifier axiom
,
-axiom-mode=off
turns off the axiom mode and, accordingly, turns on verification of assertions with the identifier axiom
.
example :
int foo(int n) [[expects axiom: n < 10]] { return n*n; }
The program can be compiled with three different levels of verification:
off
turns off all expression tests in contracts.default
only expressions with the default
modifier are checked.audit
extended mode when all checks are performed with the default
and audit
modifiersHow exactly to implement the installation of the verification level is left to the discretion of the compiler developers.
In our case, the compiler option is used for this.
-build-level=<off|default|audit>
The default is -build-level=default
As already mentioned, the compiler can use contracts for low-level optimizations. For this reason, despite the fact that at the time of execution, some predicates in contracts (depending on the level of verification) may not be computed, their failure leads to undefined behavior.
I will postpone the examples of application of assembly levels until the next section, where they can be made visible.
Depending on the options with which the program is going, in case of breach of contract there may be different scenarios of behavior.
By default, breaching a contract causes the program to crash, calling std::terminate()
. But the programmer can override this behavior by giving his handler and telling the compiler to continue the program after a breach of contract.
When compiling, you can install a violation handler called when a contract is violated.
The way to implement the installation handler is given to the discretion of the creators of the compiler.
In our case it is
-contract-violation-handler=<violation_handler>
The handler signature must be
void(const std::contract_violation& info)
or
void(const std::contract_violation& info) noexcept
std::contract_violation
equivalent to the following definition:
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; };
Thus, the processor allows you to get enough comprehensive information about exactly where and under what conditions a breach of contract occurred.
If the violation handler is set, then in case of a contract violation, by default, immediately after its execution, std::abort()
will be called std::abort()
std::terminate()
is called without specifying the handler).
The standard assumes that compilers provide tools that allow programmers to continue executing a program after a breach of contract.
The method of implementing these tools is left to the discretion of the compiler developers.
In our case, this is a compiler option.
-fcontinue-after-violation
The options -fcontinue-after-violation
and -contract-violation-handler
can be set independently of each other. For example, you can set -fcontinue-after-violation
, but not set -contract-violation-handler
. In the latter case, after the breach of contract, the program will simply continue to work.
The possibility of continuing the work of the program after the breach of contract is specified by the standard, but care should be taken with this opportunity.
Technically, the behavior of the program after the breach of contract is not defined, even if the programmer explicitly indicated that the program should continue to work.
This is due to the ability of the compiler to perform low-level optimizations per contract execution.
Ideally, if a breach of contract occurred, you need to record diagnostic information as soon as possible and shut down the program. You need to understand exactly what you are doing allowing the program to work after a violation.
Define your handler and with its help intercept the breach of contract
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; }
And consider an example of breach of contract:
#include "violation_handler.h" int foo(int n) [[expects: n < 10]] { return n*n; } int main() { foo(100); // <-- contract violation return 0; }
Compile the program with the options -contract-violation-handler=violation_handler
and -fcontinue-after-violation
and run
$ bin/example8-handling.bin line_number : 4 file_name : example8-handling.cpp function_name : foo comment : n < 10 assertion_level : default
Now you can give examples that demonstrate the behavior of the program when a contract is violated at different levels of assembly and contract modes.
Consider the following example :
#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; }
If you build it with the option -build-level=off
then, as expected, the contracts will not be checked.
Gathering with the default
level (with the option -build-level=default
), we get the following output:
$ 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
And the assembly with the level of audit
will give:
$ 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
may throw exceptions. In this case, you can configure the program so that the breach of contract leads to the release of an exception.
If the function with which contracts are described is marked as noexcept
and when checking the contract, a violation_handler
called that throws an exception, then std::terminate()
will be called.
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; }
If the flag is passed to the compiler: do not continue program execution after contract violation ( continuation mode=off
), but the violation handler handler throws an exception, std::terminate()
will be forcibly called.
Contracts are non-intrusive runtime checks. They play a very important role in ensuring the quality of the released software.
C ++ is used very widely. And for sure there will be a sufficient number of claims to the specification of contracts. In my subjective opinion, the implementation turned out quite comfortable and intuitive.
C ++ 20 contracts will make our programs even more reliable, fast, and understandable. I look forward to their implementation in compilers.
PS
In PM, they tell me that it is likely that in the final edition of the standard, the expects
and ensures
will ensures
replaced with pre
and post
, respectively.
Source: https://habr.com/ru/post/443766/
All Articles