00001 /* 00002 * eiffel.h - an assertion checking scheme similar to Eiffel, 00003 * see pg 133 of the Eiffel book. 00004 * 00005 * Copyright (c) 1997 Phil Maker 00006 * All rights reserved. 00007 * 00008 * Redistribution and use in source and binary forms, with or without 00009 * modification, are permitted provided that the following conditions 00010 * are met: 00011 * 1. Redistributions of source code must retain the above copyright 00012 * notice, this list of conditions and the following disclaimer. 00013 * 2. Redistributions in binary form must reproduce the above copyright 00014 * notice, this list of conditions and the following disclaimer in the 00015 * documentation and/or other materials provided with the distribution. 00016 * 00017 * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND 00018 * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE 00019 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE 00020 * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE 00021 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL 00022 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS 00023 * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 00024 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 00025 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY 00026 * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF 00027 * SUCH DAMAGE. 00028 * 00029 * Id: eiffel.h,v 1.1.1.1 1997/11/23 11:45:50 pjm Exp 00030 */ 00031 00032 #ifndef _eiffel_h_ 00033 #define _eiffel_h_ 00034 00035 #ifdef __cplusplus 00036 extern "C" { 00037 #endif 00038 00039 #include <nana.h> 00040 00041 /* 00042 * EIFFEL_CHECK_LEVEL - this defines the various levels of checking. 00043 * 00044 * See page 133 of "Eiffel: the language" by Bertrand Meyer. 00045 */ 00046 00047 typedef enum { 00048 CHECK_NO, /* no assertion checking */ 00049 CHECK_REQUIRE, /* only require, i.e. method preconditions */ 00050 CHECK_ENSURE, /* require+ensure, i.e. method pre/postconditions */ 00051 CHECK_INVARIANT, /* as ensure plus check class invariant on entry/exit */ 00052 CHECK_LOOP, /* as invariant plus loop invariants + variants */ 00053 CHECK_ALL /* everything including check statements */ 00054 } EIFFEL_CHECK_LEVEL; 00055 00056 /* 00057 * EIFFEL_CHECK - the level of checking to be done for this compile. 00058 * This can be overridden, e.g. by compiling with -DEIFFEL_CHECK=CHECK_ALL 00059 */ 00060 00061 #ifndef EIFFEL_CHECK 00062 #define EIFFEL_CHECK CHECK_REQUIRE 00063 #endif 00064 00065 /* 00066 * invariant() - each class using this library should provide a method 00067 * called invariant() which returns true if the object is 00068 * consistent, false otherwise. This method will be called by the 00069 * checking macros below. Since some classes don't have class 00070 * invariants we will define a default one which always succeeds. 00071 */ 00072 00073 static inline bool invariant() { 00074 return true; 00075 } 00076 00077 /* 00078 * EIFFEL_DOEND - if EIFFEL_DOEND is defined then (at the suggestion 00079 * of Bertrand Meyer (Eiffel's author)) we define the DO and END 00080 * macros which check the class invariant on method entry/exit. To 00081 * use these macros your methods should look something like: 00082 * 00083 * // if EIFFEL_DOEND is defined 00084 * void Stack::push(int n) 00085 * DO 00086 * REQUIRE(..) ; // note this is optional 00087 * .. 00088 * if(x >= 10) { 00089 * ... 00090 * } 00091 * END 00092 * 00093 * if EIFFEL_DOEND is not defined then we revert to the old 00094 * behaviour where invariants are checked by REQUIRE and ENSURE 00095 * calls. For example: 00096 * 00097 * // if EIFFEL_DOEND is not defined 00098 * void Stack::push(int n) 00099 * { 00100 * REQUIRE(x <= 10); // note this is required if you 00101 * ... // wish to check invariants 00102 * ENSURE(...); 00103 * } 00104 */ 00105 00106 #ifdef EIFFEL_DOEND 00107 00108 #define DO { IG(invariant(), EIFFEL_CHECK >= CHECK_INVARIANT); 00109 #define END IG(invariant(), EIFFEL_CHECK >= CHECK_INVARIANT); } 00110 #define REQUIRE(e) IG(e, EIFFEL_CHECK >= CHECK_REQUIRE) 00111 #define ENSURE(e) IG(e, EIFFEL_CHECK >= CHECK_ENSURE) 00112 00113 #else 00115 /* 00116 * REQUIRE(e) - precondition for a method, this also checks the class 00117 * invariant. 00118 */ 00119 00120 #define REQUIRE(e) \ 00121 do { \ 00122 IG(e, EIFFEL_CHECK >= CHECK_REQUIRE); \ 00123 IG(invariant(), EIFFEL_CHECK >= CHECK_INVARIANT); \ 00124 } while(0) 00125 00126 /* 00127 * ENSURE(e) - postcondition for a method, this also checks the class 00128 * invariant 00129 */ 00130 00131 #define ENSURE(e) \ 00132 do { \ 00133 IG(e, EIFFEL_CHECK >= CHECK_ENSURE); \ 00134 IG(invariant(), EIFFEL_CHECK >= CHECK_INVARIANT); \ 00135 } while(0) 00136 00137 #endif /* defined EIFFEL_DOEND */ 00138 00139 /* 00140 * CHECK(e) - check an assertion in inline code. 00141 */ 00142 00143 #define CHECK(e) \ 00144 IG(e, EIFFEL_CHECK >= CHECK_ALL) 00145 00146 /* 00147 * INVARIANT(e) - loop invariant. 00148 */ 00149 00150 #define INVARIANT(e) \ 00151 IG(e, EIFFEL_CHECK >= CHECK_LOOP) 00152 00153 /* 00154 * VARIANT(e) - there is no support for variant checking yet, a syntax 00155 * exists buts it too ugly for me. Perhaps if someone is interested 00156 * I'll build it; personally I find termination the least of my problems! 00157 */ 00158 00159 #ifdef __cplusplus 00160 } 00161 #endif 00162 00163 #endif
1.3.4