[patch #5873] Model checker and initial datasheet review

[Ben Pfaff]

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

                 Summary: Model checker and initial datasheet review
                 Project: PSPP
            Submitted by: blp
            Submitted on: Wednesday 04/18/2007 at 16:28
                Category: None
              Item Group: None
                  Status: Ready For Test/Review
             Assigned to: None
        Originator Email: 
             Open/Closed: Open
         Discussion Lock: Any

    _______________________________________________________

Details:

This set of changes implements a model checker and a PSPP syntax interface to
the model checker.  My goal is to check these into the main branch after
applying reviewers' comments; they are already in the simpler-proc branch.

These changes also include the current draft of the datasheet implementation
for use by the GUI.  This is because the datasheet code is currently the
model checker's only client, so it can serve as an example use of the model
checker for the enlightenment of reviewers.  I don't intend to immediately
check the datasheet code into the main branch, because it depends on the
casereader code that isn't yet in the main branch (and is not itself ready
for check-in), and because the datasheet's name is likely to change before
final check-in (and I don't think we came to a final decision on its new
name).  I'd still be happy to receive any or all feedback on the datasheet's
code or design.

A model checker is a tool for software testing and verification
that works by exploring all the possible states in a system and
verifying their internal consistency.  A conventional model
checker requires that the code in a system be translated into a
specification language.  The model checker then verifies the
specification, rather than the code.

This is instead an implementation-level model checker, which does
not require a separate specification.  Instead, the model checker
requires writing a second implementation of the system being
checked.  The second implementation can usually be made almost
trivial in comparison to the one being checked, because it's
usually acceptable for its performance to be comparatively poor,
e.g. O(N^2) instead of O(lg N), and thus to use much simpler
algorithms.

The "models" used by model checkers have little or nothing to do with the
"models" used in statistics.  I didn't use the prefix "model_" for that
reason; PSPP is about statistics, not about model checking, so it seems
better to reserve "model_" for statistical purposes.



    _______________________________________________________

File Attachments:


-------------------------------------------------------
Date: Wednesday 04/18/2007 at 16:28  Name: datasheet.tar.gz  Size: 32kB   By:
blp

<http://savannah.gnu.org/patch/download.php?file_id=12524>

    _______________________________________________________

Reply to this item at:

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

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