commit c1553860d3a74b163109fb7d1b6fef272661da65 from: Sergey Bronnikov via: Sergey Bronnikov date: Thu Oct 12 13:36:13 2023 UTC moved to helpers.h commit - 64ab76a33013999bab9676ac929633cba0df828e commit + c1553860d3a74b163109fb7d1b6fef272661da65 blob - 4208f7658068a1e9f001a1cece8f0792f095eb12 (mode 644) blob + /dev/null --- c-dbc.c +++ /dev/null @@ -1,67 +0,0 @@ -/* - * Programming by Contract is a programming methodology - * which binds the caller and the function called to a - * contract. The contract is represented using Hoare Triple: - * {P} C {Q} - * where {P} is the precondition before executing command C, - * and {Q} is the postcondition. - * - * See also: - * http://en.wikipedia.org/wiki/Design_by_contract - * http://en.wikipedia.org/wiki/Hoare_logic - * http://dlang.org/dbc.html - */ - -#ifndef PBC_H_ -#define PBC_H_ - -#include - -/* - * Checks caller responsibility against contract - */ -#define REQUIRE(cond) assert(cond) - -/* - * Checks function reponsability against contract. - */ -#define ENSURE(cond) assert(cond) - -/* - * While REQUIRE and ENSURE apply to functions, INVARIANT - * applies to classes/structs. It ensures that intances - * of the class/struct are consistent. In other words, - * that the instance has not been corrupted. - */ -#define INVARIANT(invariant_fnc) do{ (invariant_fnc) } while (0); - -#else -#define REQUIRE(cond) do { } while (0); -#define ENSURE(cond) do { } while (0); -#define INVARIANT(invariant_fnc) do{ } while (0); - -#endif /* PBC_H_ */ - - -/* - -This is an _extremely_ simple example: - -int divide (int n, int d) -{ - int ans; - - REQUIRE(d != 0); - - ans = n / d; - - // As code is added to this function throughout its lifetime, - // ENSURE will assert that data will be returned - // according to the contract. Again this is an - // extremely simple example. :-D - ENSURE( ans == (n / d) ); - - return ans; -} - -*/