Re: Regarding helping out for PSPP also model checking packages

[Ben Pfaff]

"Avinash Malik" <address@hidden> writes:

>         I wanted to help out in the development of PSPP. Although I am not a
> Statistician, I am a computer engineer (Phd student) and am involved in
> developing Formal languages and operating systems for embedded system. From
> reading the website and going through the FAQ I still have a question? Besides
> statistical analysis does this platform also support( plan to support)
> model-checking features for languages. Although not strictly a statistical
> tool model-checking is very important tool to guarantee that certain
> properties of designed systems would be met. I design safety critical systems
> like brakes, air-bags etc.. which need to work when time comes. Thus
> mathematical analysis and checking becomes important.
>        I wanted to know that if I write a subroutine for model-checking
> languages would it have any chance of being included or am I knocking on the
> wrong door altogether. If it has no chance i would still like to contribute
> but since I am not a Statistician could you suggest a source which you guys
> particularly utilise to get the formulas to be implemented etc...

By model checking, I think you are referring to this kind of
approach to a proof of correctness:
         http://en.wikipedia.org/wiki/Model_checking

Model checking is certainly valuable and I've even worked on
related approaches, in a small way, in my work at Stanford.  But
I'm not sure that it's a good fit for PSPP.  Most PSPP analyses
process a large numbers of flat and uniformly typed tuples
(cases) using a small set of instructions (commands and
subcommands).  But model checking is sort of the other way
around, at least in my experience: you have a large number of
state-transition rules, etc., but there's no need for any input
data.

PSPP also doesn't have a suitable built-in language for
describing the rules that model checkers model.

So I am not sure that PSPP is a good place to try to implement a
model checker.
-- 
"Because computer source code is an expressive means for the exchange
 of information and ideas about computer programming, we hold that it
 is protected by the First Amendment."
--Hon. Boyce F. Martin, Jr., for the 6th Circuit Court, Junger vs. Daley