[patch #5873] Model checker and initial datasheet review

[Ben Pfaff]

Follow-up Comment #2, patch #5873 (project pspp):

Thanks for the review.

>Regarding the model checker, I haven't read the references you 
>gave, but it seems that it's important to realize that it's 
>testing only the model, and the 2nd implementation of it. Errors 
>in the real implementation will go unchecked. Could the 2nd 
>implementation not be a wrapper around the 1st? 

I think that you misunderstand.  The model checker essentially *compares* the
two implementations.  Any differences between them will be found (given a few
provisos).  Thus, any error in either implementation will be found, as long
as both implementations don't have the *same* error.

>There's a typo on model-checker.h:90 

Thanks, fixed.

>mc_get_options, mc_get_results and mc_get_aux could take const arguments. 

Ditto.

>The 2nd arg of mc_run could also be const ? 

Actually, no, it destroys that argument.

> In mc_options_set_hash_bits, from whence comes the number 31 ? 
>Should this be higher on 64 bit machines? 

I wanted a value such that (1u << hash_bits) is guaranteed to be
well-defined.  I'll rewrite it as CHAR_BIT * sizeof (unsigned int) - 1 to
make this more clear.

>I'm not sure about the portability of gettimeofday 

There's a gnulib module that makes it portable, which I'm using (I didn't add
this change to the tarball, so you didn't spot it).

>The datasheet looks promising. I hope it'll be able to displace 
>much of the code in lib/gtksheet and probably 
>psppire-data-store.* and others. 

I've done some of that work in the simpler-proc branch already.  It compiles;
I haven't tried to run it yet.

>It will be necessary for struct datasheet to have a whole bunch 
>of user specified callback functions which get called whenever 
>something in the datasheet changes.  

OK.

>Presumably struct casereader is a different animal to the 
>structure that we currently have with that identifier? 

Yes, very much so.  Don't worry, I'll document it and put it up for review,
etc., before it gets into mainline.

> In datasheet_move_rows, the only thing the comments don't make 
>clear is whether or not the source and destination ranges are 
>permitted to overlap.

Overlap can't happen, because of the way that the move occurs.  I added the
following to the comment.  Does it make the way that the move occurs clear?

   Equivalent to
   deleting the given rows, then inserting them at what becomes
   position NEW_START after the deletion.

And similarly for datasheet_move_columns.





    _______________________________________________________

Reply to this item at:

  <http://savannah.gnu.org/patch/?5873>

_______________________________________________
  Message sent via/by Savannah
  http://savannah.gnu.org/