 |
Forums |
Admin  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.
-Charlie
|
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?
|
|
|
