SPARK and testing.
in [ADA]
|
Prev: SPARK and testing. Was: Lost in translation (with SPARK user rules)
Next: SPARK: What does it prove?
From: Peter C. Chapin on 28 May 2010 08:59 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
From: Yannick Duchêne (Hibou57) on 28 May 2010 19:06
Le Fri, 28 May 2010 14:59:38 +0200, Peter C. Chapin <pcc482719(a)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. |