Re: SPARK and testing.

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Fri, 28 May 2010 14:59:38 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> 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.
I believe there is indeed some reification capabilities in SPARK. This is  
not just that easy. I don't believe it would be more easy anyway with  
other methods like B or VDM.

As long as you can write in SPARK, some pre/post matching an abstract data  
type property, you can do the same in SPARK. The matter is, how difficult  
it is. And when I see things about SPARK, it mostly talks about avoiding  
runtime error, and not so much about proving an ADT has this and that  
property. Which does not mean it is not possible.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.