[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[patch #5873] Model checker and initial datasheet review

From: Ben Pfaff
Subject: [patch #5873] Model checker and initial datasheet review
Date: Sun, 22 Apr 2007 17:05:56 +0000
User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv: Gecko/20061205 Iceweasel/ (Debian-

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. 


>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.  


>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:


  Message sent via/by Savannah

reply via email to

[Prev in Thread] Current Thread [Next in Thread]