cline@sunshine.ece.clarkson.edu (Marshall Cline) (06/08/89)
In article <77300029@p.cs.uiuc.edu> johnson@p.cs.uiuc.edu writes: [...deleted stuff...] >I think that assertions are one of the most attractive things about >Eiffel... >Eiffel assertions are a first step to making the theory of software >verification practical... It seems obvious to me that they will help >make software a lot more reliable. >It is interesting to note that our operating system written in C++ >makes heavy use of assertions. A student implemented assertions >using a macro package... ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^ More more more. I'm salivating thinking about it. Do you mean that the grad student simply created a standard way to state assertions? Are they (the assertions) usable in any formal way? Ie: Do you sometimes expand them into: #define assertion(bool_expr) if (!(bool_expr)) print_nasty_msg() Or do you have tools that formally check method correctness which use the assertions as constraints??? More more more. Tell me more! Seriously: I'm interested in this line of thought, being that I have a software engineering bent. Given the flavor of this newsgroup, perhaps others would be interested as well. Waddayasay? Wanna post the macros? Cheers. Marshall -- ________________________________________________________________ Marshall P. Cline ARPA: cline@sun.soe.clarkson.edu ECE Department UseNet: uunet!sun.soe.clarkson.edu!cline Clarkson University BitNet: BH0W@CLUTX Potsdam, NY 13676 AT&T: (315) 268-6591
paul@sun600.UUCP (Paul E. Black) (06/09/89)
Here's our version of an "assert" (run-time check) macro.
/* *created "Wed Oct 9 13:16:25 1985" *by "Paul E. Black" */
/* *modified "Mon Oct 19 13:20:35 1987" *by "Paul E. Black" */
/*------------------------------------------------------------------------*/
/*
* This file contains a macro definition for ASSERT. In your code you
* can place statements like:
* ASSERT(0 <= row && pNodePtr->rowSize > 3);
* If your program is compiled with RIGOROUS defined, for example
* cc -DRIGOROUS ..., the assertion is checked. If RIGOROUS is not
* defined, the assertion creates no code. Therefore you can ASSERT
* very complex or time consuming things, e.g. foo should be in a table,
* which you would not want to check during normal operation.
*
* This ASSERT differs from the C standard "assert" in that no exit()
* or abort() occurs: there is only a message to stderr. Also the
* default is that ASSERT does nothing and must be turned on, whereas
* "assert" is on as a default and must be turned off.
*/
/*------------------------------------------------------------------------*/
#ifdef RIGOROUS
#define ASSERT(ex) {if (!(ex)) (void)fprintf(stderr,"ex not true in %s, line %d\n",__FILE__,__LINE__);}
#else
#define ASSERT(ex)
#endif
Paul E. Black | UUCP: ...{pyramid,amdahl,ames}!oliveb!cirrusl!paul
CIRRUS LOGIC, Inc. | Internet: cirrusl!paul@olivetti.com
1463 Centre Pointe Dr. | Voice: 408-945-8305 extension 210
Milpitas, CA 95035 USApcg@aber-cs.UUCP (Piercarlo Grandi) (06/09/89)
In article <764@cirrusl.UUCP> paul@sun600 (Paul E. Black) writes: Here's our version of an "assert" (run-time check) macro. [ ... ] #ifdef RIGOROUS #define ASSERT(ex) {if (!(ex)) (void)fprintf(stderr,"ex not true in %s, line %d\n",__FILE__,__LINE__);} #else #define ASSERT(ex) #endif This is a bit lame... :-). If you create a class for assertions, with constructors and destructors, you can have them automatically checked at block entry and exit; general idea is: { ENSURE(entry-condition,exit-condition); .... } where ENSURE expands to an immediate check for entry-condition, and wraps up exit-condition in some destructor of a dummy object. With G++, if you use wrappers, you can even have some contrived form of class invariants. In general constructors and destructors in C++ allow you to define almost fully general entry-exit functions (I posted some months ago two small classes, for clean exception handling and tracing, that use this aspect of the language). In practice the only limit is the non easy problem of non local dynamic control transfers; in theory destructors ought to be called whenever the current block instance is passivated and constructors whenever it is activated. (in the general case, not in C++ yet (:->), you can reenter and leave a block *instance* many times). Notably, setjmp/longjmp does ignore destructors... This is a well known problem; BS supposedly is thinking about macaroni and catch/throw and continuations ... :-> -- Piercarlo "Peter" Grandi | ARPA: pcg%cs.aber.ac.uk@nsfnet-relay.ac.uk Dept of CS, UCW Aberystwyth | UUCP: ...!mcvax!ukc!aber-cs!pcg Penglais, Aberystwyth SY23 3BZ, UK | INET: pcg@cs.aber.ac.uk
cowan@marob.masa.com (John Cowan) (06/13/89)
In article <764@cirrusl.UUCP> paul@sun600 (Paul E. Black) writes: >#define ASSERT(ex) {if (!(ex)) (void)fprintf(stderr,"ex not true in %s, line %d\n",__FILE__,__LINE__);} Pfui. Note the Reiserism. Correct ANSI C would use #ex outside the quotes, rather than ex inside them. Does C++ make Reiserism standard? I hope not. -- John Cowan <cowan@marob.masa.com> or <cowan@magpie.masa.com> UUCP mailers: ...!uunet!hombre!{marob,magpie}!cowan Fidonet (last resort): 1:107/711 Aiya elenion ancalima!