Re: SPARK and testing.

["Peter C. Chapin" <pcc482719@gmail.com>]

Peter C. Chapin wrote:

> 4. I might get lazy or run out of time and not complete all the proofs. 

I can elaborate on this a little more. In my case the program I'm working on
now needs to compute the minimum model of a collection of Datalog rules
(Datalog is a simple logic language that has been discussed as a possible
database query language). I don't know how to express such a complex, high
level characteristic as a SPARK '--#post' annotation.

What I need to say is that the information in an array Model_Area (an array of
tuples) is the minimum model implied by the Datalog rules in a different
array Storage_Area. It is well beyond my skills with SPARK to say such a
thing. I'm not saying that it is beyond SPARK's ability to express that
relationship, but for me it is just easier to explore the matter with a test
program.

Peter