#ifndef ASSERT_H
#define ASSERT_H
///////////////////////////////////////////////////////////////
//  assert.h    --  support for design by contract           //
//  ver 1.0                                                  //
//  Language:       Visual C++, ver 6.0                      //
//  Platform:       Micron Dual Pentium Pro 200, Win NT 4.0  //
//  Application:    CSE784, Pr2, Fall 1998                   //
//  Author:         Jim Fawcett, CST 2-187, Syracuse Univ.   //
//                  (315) 443-3948, fawcett@ECS.syr.edu      //
///////////////////////////////////////////////////////////////
//  Based on "Exception-Based Assertion Mechanism for C++    //
//  David Welch and Scott Strong                             //
//  Journal of Object Oriented Programming, July/August 1998 //
///////////////////////////////////////////////////////////////
/*
    Notes:
    ======
    This is an incomplete implementation of the code from the
    paper cited above.  I did not include either the FORALL or
    ESISTS constructs.

    I only tested REQUIRE, CHECK, INVARIANT, and ASSERT.  So
    that means that I did not test ENSURE, IMPLIES, NEVER_GET_HERE,
    BASE_INVARIANT, or USES_OLD.  Testing these is up to you!
*/

class Assertion;
typedef Assertion & AssertionRef;
typedef const Assertion & AssertionCref;

//----< ASSERTION exception >------------

#define ASSERTION(type, exp) \
  throw Assertion(Assertion::type,#type "("exp")",__FILE__,__LINE__)

//----< REQUIRE(exp) >-------------------

#if defined ALL_ASSERTIONS || defined ASSERT_REQUIRE
#define REQUIRE(exp) \
  if(!(exp)) { ASSERTION(Require,#exp); } else {;}
#else
#define REQUIRE(exp)
#endif

//----< ENSURE(exp) >--------------------

#if defined ALL_ASSERTIONS || defined ASSERT_ENSURE
#define ENSURE(exp) \
  if(!(exp)) { ASSERTION(Ensure,#exp); } else {;}
#else
#define ENSURE(exp)
#endif

//
//----< CHECK(exp) >---------------------

#if defined ALL_ASSERTIONS || defined ASSERT_CHECK
#define CHECK(exp) \
  if(!(exp)) { ASSERTION(Check,#exp); } else {;}
#else
#define CHECK(exp) if(!(exp)) {;} else {;}
#endif

//----< IMPLIES(exp1,exp2) >-------------

#if defined ALL_ASSERTIONS
#define IMPLIES(exp1,exp2) \
  if(exp1) {if(!(exp2)) {ASSERTION(Implies,#exp1","#exp2);}} else {;}
#else
#define IMPLIES(exp1,exp2)
#endif

//----< NEVER_GET_HERE >-----------------

#define NEVER_GET_HERE \
  throw Assertion( \
    Assertion::NeverGetHere,"NEVER_GET_HERE",__FILE__,__LINE__ \
  )

//----< INVARIANT >----------------------

#if defined ALL_ASSERTIONS
#define INVARIANT protected: virtual void invariant() const {
#define END_INVARIANT }
#define CHECK_INVARIANT invariant()
#else
#define INVARIANT
#define END_INVARIANT
#define CHECK_INVARIANT
#endif

//----< ASSERT for inside INVARIANT >----

#if defined ALL_ASSERTIONS
#define ASSERT(exp) \
if(!(exp)) { ASSERTION(Assert,#exp); } else {;}
#else
#define ASSERT(exp)
#endif

//----< BASE-INVARIANT >-----------------

#if defined ALL_ASSERTIONS
#define BASE_INVARIANT(ClassType) ClassType::invariant()
#else
#define BASE_INVARIANT(ClassType)
#endif

//

//----< USES_0LD >-----------------------

#if defined ALL_ASSERTIONS || defined ASSERT_ENSURE
#define USES_OLD(Type) Type old(*this)
#else
#define USES_OLD(Type)
#endif


class Assertion {

  public:
    
    enum Type { 
      Require,Ensure,Check,Assert,Implies,NeverGetHere,ForAll,ThereExists
    };
    
    Assertion(
      Type assertionType, const char* reason, const char* file, int line
    );
    Assertion(const Assertion &other);
    virtual ~Assertion();
    Assertion& operator=(const Assertion &other);
    const char* getReason() const;
    const char* getFile() const;
      int getLine() const;
     Type getType() const;

  private:
    char* theReason;
    char* theFile;
    int   theLine;
    Assertion::Type theType;
};

#endif