include/nana/eiffel.h

Go to the documentation of this file.
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

Generated on Sun Aug 21 04:18:13 2005 for Udanax-Green by doxygen1.3.4