Forums | Admin

Discussion Forums: open-discussion

Start New Thread Start New Thread


By: Charles Mills
RE: Order of preconditions [ reply ]  
2004-10-29 17:57
Yeah, nice catch. That was a bug in the example. The invariants were suppost to be:
inv: self != NULL
inv: (self->length > 0 and self->array != NULL)
or (self->length == 0 and self->array == NULL)
I made that change in CVS a few hours ago and just uploaded a new package.
The installation on the new package is also much cleaner.
I added deinstallation instructions to the FAQ on the wiki, for cleanly removing the old package. I will also be adding a Ruby Gem soon.

By: Marc Verwerft
Order of preconditions [ reply ]  
2004-10-29 16:48
In the array example I saw that the following invariant for the array type T exists:

context Array_T
inv: (self->length > 0 and self != NULL)
or (self->length == 0 and self == NULL)

This invariant is translated into the following C-code (e.g. Array_get):

/* Invariants: */
if (!((((array->length > 0 && array != NULL)) || ((array->length == 0 && array == NULL))))) {
dbc_error("array.ocl:9: Array_get(): " "invariant failed");

As a general practice it is better to first test that the array is NOT a NULL pointer before dereferencing it. I know it comes down to reversing the order of the test, but you might want to stress that for newcomers in the C world ;-)

Just a hint for fixing in the documentation.

As a second thought, would it be possible to do this automagically in dbc?