Prev: SPARK POGS: List the rules used by the Simplifier
From: Yannick Duchêne (Hibou57) on 13 Aug 2010 16:12
Hello,

I've opened a thread about it some months ago. Here is a new opportunity
to come back to this topic : help you (and me) and SPARK to better
understand each others. I am not talking about the language, ... about the
simplifier (and may a bit about the examiner which do a bit a the
simplifier's job).

User rules kept apart because this may be better to avoid it as much as
possible I feel, and because sometime this may be advised to strictly
avoid it (see below), guessing what the simplifier will be able to to with
this and that is a cool affair. There is a kind of feeling involved here,
and it is less predictable than the grammatical validity of a given
compilation unit.

This is always what I am facing. I had previous experiences which shown
using a lot of --# check to attempt to build a step by step proof can end
into a very long Simplifier execution time (I have meet a case where it
was needed as much as 20 minutes on a simple procedure... due to the
assert clauses I used). Although this may work nice, this technique has
some limits. This is at least what I have learned since my previous
experiences.

I have posted a second example for SPARK at Rosetta today,
http://rosettacode.org/wiki/Function_definition#SPARK , which uses an
if-then-elsif block. This works nice, validate nice, no trouble with this
one (just notice I needed two separate branches, one for A = 0 and another
for B = 0, because a single one for “(A = 0) or (B = 0)” was not provable
at all by the Simplifier).

I wanted to make this more light and simple, dropping this if-then-elsif
block. Doing so, I am facing some incomprehension between me and SPARK
(but as it is one of my friend, I feel it is worth the effort to still go
on with it).

I came to two points : the first one, I've already meet it in the past,
but never talked about it ; the second one, is hard to me, as I don't want
to rely on any user rule for examples posted at Rosetta.

The first one is that if I want to get ride of these if-then-elsif
branches, I do not know another way except using P1 -> Pn where P1 stands
for the same expressions as the ones which was in if-elsif condition
expressions. OK, this looks fine, except if I want to move multiple Check
or Assert outside of conditional branch, as I have to prefix all of these
with the "P1 -> " and if P1 is a quite complex expression, this can lead
to unreadable things (I am not just talking about the example at Rosetta
here).

I was wondering if it is good or bad practice to use language construct to
makes things provable instead of using Check and Assert. It seems to me,
language constructs may be more efficient is some cases, but I still would
like to read opinions about it.

The second one, is one of this so simple things I am failing to express :
I can get (A = 0) or not (A = 0) to validate successfully, but I can't get
(A = 0) or (A /= 0) to validate as much successfully (fails), while it can
prove (not (A = 0)) = (A /= 0). Can't understand this... And I have tried
many things.

This second point may turn back into the first, saying “finally, if it
works fine using a language construct, why would you want to avoid to use
this language construct ?”, or alternatively to discuss this oftenly
occurring question : how do I make it understand such a simple thing...
without using user rules here.

Pleased to read you
 | 
Pages: 1
Prev: SPARK POGS: List the rules used by the Simplifier