Design by contract (DBC) and its application in C language

Want to make APP Same thing as WeChat , Can run small programs smoothly ？ | Experience will send you to Xinjiang 、 Huawei 、 Cherry keyboard ！>>>

Please indicate the source when reprinting

Author's contact information ：[email protected]

One 、 Preface

   In this week's training, I was exposed to contract design , After consulting a lot of materials, I still have a little knowledge , After communicating with colleagues and university tutors , Inspired , This paper records and summarizes the personal understanding of learning contract design .

Two 、 What is contract design ？

1、 summary

   Design by contract / Contract coding （Design by Contract(DbC), hereinafter referred to as DbC ） It's a way of designing computer software . This method describes , A software designer should define a formal... For a software component 、 accurate 、 Verifiable interface specifications , It extends abstract data types to prior conditions 、 A general definition of posteriori conditions and invariants . These norms are called “ contract ”, It's a metaphor , It's like a business contract / Conditions and responsibilities of the contract , For the above concepts , The following is a detailed description of .

notes ：Dbc Come of Eiffel Language , But its scope of application has nothing to do with language .

2、 Purpose

  Dbc The main purpose of this paper is to hope that the programmer can clearly define a module unit when designing a program （ Specifically object-oriented , Is an instance of a class ） What state should an operation be in before and after it is called .Dbc It's not a programming paradigm , It's a design style , A grammatical norm .

3、 Ideas

   Contract design emphasizes three concepts ： A priori condition , Post validation conditions and invariants .

• A priori condition ： For functions , It is expected that all modules that call it guarantee certain entry conditions , So it doesn't have to deal with situations that don't satisfy a priori condition , A priori condition occurs at the beginning of each function .
• Posttest conditions ： Ensure that specific properties are given when exiting , That is to say, what functions guarantee to do , The state of the function at completion , The fact that a function has this means that it will end , There's no endless cycle , A posteriori condition occurs at the end of each function .
• Invariant ： Assume at entry that , And keep certain properties on exit , Invariants are actually the intersection of preconditions and postconditions , Violating these operations will cause the program to throw an exception . From the perspective of the caller , The condition is always true , In the internal processing of a function , The invariant can be variable , But at the end of the function , When control returns to the caller , The invariant must be true .

4、 Six principles

（1） Distinguish between command and query . The query returns a result , But it doesn't change the visible nature of the object . Command to change the state of an object , But it doesn't necessarily return the result .

（2） Separate the basic query from the derived query . Query can be defined by derivation .

（3） For each derived query , Set a posterior condition , Use the results of one or more basic queries to define it . So we just need to know the value of the basic query , You can also know the value of the derived query .

（4） Write a posteriori condition for each command , Specify the value of each basic query . combination “ Define derived queries with basic queries ” Principles , We've been able to see the full visual effect of each command .

（5） For each query and command , Using an appropriate prior condition . A priori condition limits when a customer invokes queries and commands .

（6） Write invariants to define constant properties of objects . Class is the embodiment of some kind of abstraction , Focus on the most important attributes , To help readers build the correct conceptual model of class abstraction .

3、 ... and 、 Why use Dbc（ Importance ）

• Get better design ：Dbc Encourage programmers to think about things like “ What is the prior condition of a function ” Questions like this , This helps programmers to sort out the concept , The function gets a clearer description , At the same time, it limits the function calls , The results of illegal calls are also very clear .

• Ensure system robustness ： Systematic use of exceptions When routines are used illegally （ A priori condition failed ） Or the routine doesn't follow the contract （ A posteriori condition or invariant fails ） when , An exception will occur .

• More effective organization of communication between modules ： Define as accurately as possible the responsibility and authority of modules to communicate with each other .

• Improve reliability ： Writing contracts can help developers understand code better , Contracts help test （ Contracts can be closed or activated at any time ）.

• Simplify debugging ： A contract can fix a mistake firmly , Support during development Errors that are exposed at run time because the assertion is false will be accurately located .

• ......

  wait .

Four 、 How to use... In programming Dbc（C Language ）

   This is a brief description of Dbc The definition of 、 Its core concept and general idea , It can be seen that many programmers are doing more or less of these tasks in their normal programming . For example, at the beginning of the function definition, we can judge whether the given pointer parameter cannot be NULL, Or release the temporarily allocated memory block when the program exits . But in detail, it depends on personal habits , Some people like caller checking , Others like to be checked by callers .

  Eiffel The difference from these practices is that it is the only way to put a priori condition in grammatical form 、 Posteriori conditions and invariants are defined as the language of independent syntax blocks in the callee code , The key words are require、ensure、invariant.

   The following example is Eiffel Language , come from ：http://www.eiffel.com/developers/design_by_contract_in_detail.html

   Function description ： Define a generic class DICTIONARY [ELEMENT] Of put Method ;

   A priori condition ： The current number of elements count Less than capacity capacity, Key value key Not an empty string ;

   Posttest conditions ： There are elements in the dictionary x; Use health value key The acquired elements are x; Number of elements after operation count Equal to the number of elements before the operation old count Add one ;

   Invariant ： Element number count Greater than 0, Less than capacity capacity;

class DICTIONARY [ELEMENT]                
    feature
put (x: ELEMENT; key: STRING) is                
         -- Insert x so that it will be retrievable               
         -- through key.              
require
count <= capacity
not key.empty
        ensure  
has (x)        
item (key) = x  
count = old count + 1
    end  
     ... Interface specifications of other features ...                  
invariant  
0 <= count  
          count <= capacity  
end

   Rewrite it as C Language , As shown below ：

#include "stdio.h"
#include "assert.h"

/*  Dynamic array element structure （ hypothesis ） */
typedef struct _element_t {
 int x;
 char* key;
} element_t;

bool_t put(darray_t* darray, int x, const char* key) {
 /*  A priori condition (require) */
 assert(darray->size >= 0 && darray->size < darray->capacity);

 /*  Invariant （invariant） */
 assert(darray->size >= 0 && darray->size < darray->capacity);

 /* put operation  */
 uint32_t old_count = darray->size;
 element_t elm;
 elm.x = x;
 elm.key = TKMEM_CALLOC(1, tk_strlen(key) + 1);
 tk_strcpy(elm.key, key);
 darray_push(darray, &elm);

 /*  Posttest conditions （ensure） */
 element_t* elm_find = darray_find(darray, &elm);
 assert(elm_find != NULL && elm_find->x == x && tk_str_eq(elm_find->key, key) && darray->size == old_count + 1);

 /*  Invariant （invariant） again */
 assert(darray->size >= 0 && darray->size < darray->capacity);
    
 return TRUE;
}

notes ：

The above code calls AWTK Part of the library functions in , If you don't understand, please ask questions in the comments , Or private letters .

AWTK Of github Warehouse ：https://github.com/zlgopen/awtk

5、 ... and 、 summary

   Through the above study , It can be seen that Dbc In fact, the original meaning of the is very simple , Is to add assertions to the design program . And the so-called assertion , Reality is the assumption that has to be true , Only these assumptions are true , The program can be correct .Dbc The main assertion of the above-mentioned a priori condition , Post validation conditions and invariants .

   Last , I would like to thank my colleagues who have discussed with me and the university tutors who have taken the time to answer my questions .