From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: Re: Lost in translation (with SPARK user rules)
Date: Tue, 01 Jun 2010 07:42:20 +0200
Date: 2010-06-01T07:42:20+02:00 [thread overview]
Message-ID: <op.vdlwsuajule2fv@garhos> (raw)
In-Reply-To: op.vda45rsfule2fv@garhos
A little test I did right a few seconds ago.
Let a rule be of the form:
C1 may_be_deduced_from [C2, V].
Which is so that this one is valid too:
C2 may_be_deduced_from [C1, V].
So finally, C1 and C2 and both either conclusion or condition.
This may *logically* (not by pattern) match three other things:
C1 -> C2 may_be_deduced_from [V].
C2 -> C1 may_be_deduced_from [V].
C1 <-> C2 may_be_deduced_from [V].
Although only one would be required, which is
C1 <-> C2 may_be_deduced_from [V].
Instead one need to have (and write) all of:
C1 may_be_deduced_from [C2, V].
C2 may_be_deduced_from [C1, V].
C1 -> C2 may_be_deduced_from [V].
C2 -> C1 may_be_deduced_from [V].
C1 <-> C2 may_be_deduced_from [V].
Five rules instead of one, where one logical rule would be sufficient.
I wanted to get ride of this, with these generic rules, which I hoped will
help and solve this recurrent trick:
A may_be_deduced_from [B, B -> A].
A may_be_deduced_from [B, B <-> A].
B may_be_deduced_from [A, B <-> A].
B -> A may_be_deduced_from [B <-> A].
A -> B may_be_deduced_from [B <-> A].
I though this would ends to exact matches, and I would have only to write
rules of the form
C1 <-> C2 may_be_deduced_from [V].
... <-> ... may_be_deduced_from [...].
or of the form
C1 -> C2 may_be_deduced_from [V].
... -> ... may_be_deduced_from [...].
and expected I would have to write only this, avoiding duplications of
multiple equivalent forms (I expected these equivalent forms would be
deduced via the above generic rules). Unfortunately, and although this
looks like there should be exact matches after instantiations, this does
not work (rules does not match in Simplifier).
Now I really see why there is the restriction of user rules which are to
be defined on package or subprogram basis (while I still don't enjoy this)
: this test clearly demonstrate there is no way to write general rules,
these are always specifics to a VC or a set of VC for a given package or
subprogram. Or else, all logical equivalences need to be written
explicitly (which in turn requires great care when one want to review
rules, as duplication -- I know it after experiences -- does not help
safety and help to miss weakness).
Note: SPARK is still useful ;) with these words, I don't wanted to say it
is not good
--
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.
prev parent reply other threads:[~2010-06-01 5:42 UTC|newest]
Thread overview: 46+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-05-26 10:09 Lost in translation (with SPARK user rules) Yannick Duchêne (Hibou57)
2010-05-26 10:38 ` Phil Thornley
2010-05-26 10:57 ` Yannick Duchêne (Hibou57)
2010-05-26 14:15 ` Pascal Obry
2010-05-26 14:28 ` Dmitry A. Kazakov
2010-05-26 19:28 ` Yannick Duchêne (Hibou57)
2010-05-26 20:14 ` Dmitry A. Kazakov
2010-05-26 21:14 ` Yannick Duchêne (Hibou57)
2010-05-26 21:15 ` Yannick Duchêne (Hibou57)
2010-05-26 22:01 ` Peter C. Chapin
2010-05-27 12:32 ` Mark Lorenzen
2010-05-27 18:34 ` Pascal Obry
2010-05-27 19:18 ` Yannick Duchêne (Hibou57)
2010-05-28 9:39 ` Maciej Sobczak
2010-05-28 11:57 ` SPARK and testing. Was: " Peter C. Chapin
2010-05-28 12:59 ` SPARK and testing Peter C. Chapin
2010-05-28 23:06 ` Yannick Duchêne (Hibou57)
2010-05-26 19:16 ` Lost in translation (with SPARK user rules) Yannick Duchêne (Hibou57)
2010-05-26 19:32 ` Pascal Obry
2010-05-26 20:56 ` Yannick Duchêne (Hibou57)
2010-05-26 22:06 ` Peter C. Chapin
2010-05-27 18:39 ` Pascal Obry
2010-05-26 22:17 ` Peter C. Chapin
2010-05-27 10:11 ` Sockets package in SPARK (Was: Lost in translation (with SPARK user rules)) Jacob Sparre Andersen
2010-05-27 18:41 ` Pascal Obry
2010-05-27 19:20 ` Yannick Duchêne (Hibou57)
2010-05-28 7:43 ` Sockets package in SPARK Jacob Sparre Andersen
2010-05-27 8:13 ` Lost in translation (with SPARK user rules) Yannick Duchêne (Hibou57)
2010-05-27 10:55 ` Yannick Duchêne (Hibou57)
2010-05-27 11:32 ` Yannick Duchêne (Hibou57)
2010-05-27 11:41 ` Phil Thornley
2010-05-27 12:42 ` Yannick Duchêne (Hibou57)
2010-05-27 12:22 ` stefan-lucks
2010-05-27 11:37 ` Yannick Duchêne (Hibou57)
2010-05-27 11:57 ` Phil Thornley
2010-05-27 12:36 ` Yannick Duchêne (Hibou57)
2010-05-27 13:38 ` Phil Thornley
2010-06-03 2:44 ` Yannick Duchêne (Hibou57)
2010-05-27 19:53 ` Warren
2010-05-29 23:03 ` Yannick Duchêne (Hibou57)
2010-05-30 6:55 ` Yannick Duchêne (Hibou57)
2010-05-30 9:30 ` Phil Thornley
2010-05-30 9:46 ` Yannick Duchêne (Hibou57)
2010-05-30 9:26 ` Phil Thornley
2010-05-30 9:57 ` Yannick Duchêne (Hibou57)
2010-06-01 5:42 ` Yannick Duchêne (Hibou57) [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox