SPARK understand me very well... me neither

SPARK understand me very well... me neither

[Yannick Duchêne (Hibou57)]

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

Re: SPARK understand me very well... me neither

[Yannick Duchêne (Hibou57)]

I have looked at it again, and cannot do better than stopping here:


    package Functions is
       function Multiply (A, B : Natural) return Natural;
       --# pre (A /= 0) -> (B <= (Integer'Last / A));
       --# return A * B; -- Implies commutativity on Multiply arguments
    end Functions;

    package body Functions is
       function Multiply (A, B : Natural) return Natural
       is
          Result : Natural;
       begin
          --# check (A = 0) -> ((A * B) = 0);
          --# check (A = 0) -> ((B * A) <= Integer'Last);
          --# check not (A = 0) -> (B <= (Integer'Last / A));
          --# check not (A = 0) -> ((B * A) <= (Integer'Last / A) * A);
          --# check not (A = 0) -> ((Integer'Last / A) * A <= Integer'Last);
          --# check not (A = 0) -> ((B * A) <= Integer'Last);
          -- Here is a gap which I cannot cross
          --# assert (A * B) <= Integer'Last;
          Result := A * B;
          return Result;
       end Multiply;
    end Functions;


Where I have marked “Here is a gap which I cannot cross”. A is either 0 or  
not 0, as (A = 0) -> ((B * A) <= Integer'Last) and
not (A = 0) -> ((B * A) <= Integer'Last) is proved, then (A * B) <=  
Integer'Last should be proved as well, as this finally turns into Any Case  
-> (A * B) <= Integer'Last. But no way to do, this only works with an  
if-then statement, and cannot do without it (and I do not want user rules  
here). I had a look at “SPARK/lib/checker/rules/LOGIC.RUL” to see what  
SPARK knowns from inborn, but just found these sole rules about “->” :


    /*** Other handy logical equivalences (DeMorgan, etc.) ***/

    logical(1):     not (A or B)     &   (not A) and (not B)     
are_interchangeable.
    logical(2):     not (A and B)    &   (not A) or (not B)      
are_interchangeable.
    logical(3):     A -> B           &   (not A) or B            
are_interchangeable.
    logical(4):     A <-> B          &   (A -> B) and (B -> A)   
are_interchangeable.
    logical(5):     A -> (B -> C)    may_be_replaced_by         (A and B)  
-> C.


And I would not want to turn X -> Y into (not X) or Y, as this would not  
create a nice example.

Note: you can see a concrete example of what I meant talking about P1 ->  
Pn when removing conditional statements. The four --#check prefixed with  
“not (A = 0) ->  ... ” match what was beneath the branch in the  
conditional statement where A /= 0. Do you see ?

Well, probably statements with logical branches, like if-then, or case,  
cannot be handle as easily using pure logical expressions. It had far less  
difficulties to fill the gap I point above when there was the if-then  
statement ; while without it, although with equivalent logical  
expressions, it cannot.

Re: SPARK understand me very well... me neither

[Phil Thornley]

On 14 Aug, 05:57, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> I have looked at it again, and cannot do better than stopping here:
>
>     package Functions is
>        function Multiply (A, B : Natural) return Natural;
>        --# pre (A /= 0) -> (B <= (Integer'Last / A));
>        --# return A * B; -- Implies commutativity on Multiply arguments
>     end Functions;
>
>     package body Functions is
>        function Multiply (A, B : Natural) return Natural
>        is
>           Result : Natural;
>        begin
>           --# check (A = 0) -> ((A * B) = 0);
>           --# check (A = 0) -> ((B * A) <= Integer'Last);
>           --# check not (A = 0) -> (B <= (Integer'Last / A));
>           --# check not (A = 0) -> ((B * A) <= (Integer'Last / A) * A);
>           --# check not (A = 0) -> ((Integer'Last / A) * A <= Integer'Last);
>           --# check not (A = 0) -> ((B * A) <= Integer'Last);
>           -- Here is a gap which I cannot cross
>           --# assert (A * B) <= Integer'Last;
>           Result := A * B;
>           return Result;
>        end Multiply;
>     end Functions;
>
[...]

I'm going to question this way of completing proofs in SPARK.

Yannick, I realise that you are an enthusiast for this but it's not
the way that the job is done in practice - it doesn't scale up for
real problems.  When it takes seven proof statements to (fail to)
prove a simple multiplication then this method isn't practicable for
the sorts of expressions that appear in the real-world models of
embedded systems.

So we shouldn't be publicising this approach in sites such as Rossetta
Code.


For this particular example, I don't understand why you haven't used
the obvious precondition:
--# pre A * B in Integer;
which not only removes the need for all those 'check' statements but
also allows the function to have Integer parameters and return value
(rather then being restricted to Natural).

The version of the precondition that will work best (measured by
leaving the lowest number of unproven VCs) depends on how the calling
code ensures that it meets the precondition.

The easiest way to achieve this (for general purpose functions like
Multiply) is by having the subtypes of the parameters as constrained
as possible, so, as long as the bounds on the two terms are small
enough, meeting this simpler version of the precondition is
automatic.  With your version of the precondition, most calls of the
function are likely to generate an unproven VC that the user then has
to deal with.

OTOH, if the bounds of the parameter subtypes can't ensure the
precondition, then the program has to use a defensive check, in which
case your version of the precondition may work better (if the
defensive check is exactly that precondition).

In a well-designed program, the subtype constraints should match the
usage of the variables of the subtypes and I would expect defensive
checks to be quite rare. (It could be argued that a defensive check
indicates a failure - or at least a weakness - in the design.) They
mainly occur as checks on values coming in across the system boundary.

Where a defensive check is required then I would provide a user-rule
that allows the relevant precondition to be proved from the check that
is made.

So I would much prefer the simple and obvious version of the
precondition and code to be the version on Rosetta Code so that anyone
browsing that site for information about SPARK doesn't get a wrong
view of the language.

Cheers,

Phil

Re: SPARK understand me very well... me neither

[Yannick Duchêne (Hibou57)]

Le Sat, 14 Aug 2010 18:04:23 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> Yannick, I realise that you are an enthusiast for this but it's not
> the way that the job is done in practice - it doesn't scale up for
> real problems.  When it takes seven proof statements to (fail to)
> prove a simple multiplication then this method isn't practicable for
> the sorts of expressions that appear in the real-world models of
> embedded systems.

That is precisely the matter I was wondering about. It appears all my  
attempt always end to be too much complicated.

> So we shouldn't be publicising this approach in sites such as Rossetta
> Code.
OK.


> For this particular example, I don't understand why you haven't used
> the obvious precondition:
> --# pre A * B in Integer;
Because I did not knew this was feasible. May be due to a background: I  
use to write less or more formal comment in Pascal or Ada source, to show  
that this and that was valid or how this could be valid. So all my attempt  
so far was focusing on the How Be Valid (and though SPARK was working this  
way also). If i understand you, there is a more declarative approach. Is  
that it ?

> The version of the precondition that will work best (measured by
> leaving the lowest number of unproven VCs) depends on how the calling
> code ensures that it meets the precondition.
This is one of the reason I am thinking about the How Be Valid. Balancing  
your way and the (not so good) way I used so far, I would say one says  
How, the other does not.

> The easiest way to achieve this (for general purpose functions like
> Multiply) is by having the subtypes of the parameters as constrained
> as possible, so, as long as the bounds on the two terms are small
> enough, meeting this simpler version of the precondition is
> automatic.
Yes. That is exactly what I had in a Pascal application I remember of. I  
had a kind of screen area, and I had to be sure the area could always be  
computed without overflow. I defined a type for area, and a type for  
height and width, so that the maximum of width and height could never  
commit an overflow and area could always be computed in any case. This fat  
more simple to check for that checking less constrained width and height  
would not commit an overflow.

The reason why I did not used it here, is because I did not see a  
legitimate way to restrict the input type beside of the result type.

> OTOH, if the bounds of the parameter subtypes can't ensure the
> precondition, then the program has to use a defensive check, in which
> case your version of the precondition may work better (if the
> defensive check is exactly that precondition).
That is the case where input cannot be constrained, which is, if this has  
to be fully general and generic. While the way I exposed with the Pascal  
example above, is better whenever possible.

> In a well-designed program, the subtype constraints should match the
> usage of the variables of the subtypes
Agree, except that I could not see a way to restrict here.

> So I would much prefer the simple and obvious version of the
> precondition and code to be the version on Rosetta Code so that anyone
> browsing that site for information about SPARK doesn't get a wrong
> view of the language.
That is the target and the reason why I posted the question here. Hopfully  
I get the good anwser.

Wish I had read such a reply priorly, this would have save me lot of  
headache.

Will try to revisit all my approach with this ideas in mind.

Hope you are not too much tired with my beginner's questions.

-- 
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.

Re: SPARK understand me very well... me neither

[Phil Thornley]

On 14 Aug, 17:44, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Le Sat, 14 Aug 2010 18:04:23 +0200, Phil Thornley  
> <phil.jpthorn...@gmail.com> a écrit:
[...]
> > For this particular example, I don't understand why you haven't used
> > the obvious precondition:
> > --# pre A * B in Integer;
>
> Because I did not knew this was feasible.
OK - that seems a pretty good reason :-)

[...]
> > In a well-designed program, the subtype constraints should match the
> > usage of the variables of the subtypes
>
> Agree, except that I could not see a way to restrict here.

For a general purpose function such as this the author can't define
sensible subtypes for the individual inputs because the condition that
the function relies on is itself a function of both of the inputs.
That's why there has to be a precondition.  The job of the author is
always to come up with the weakest precondition that does the job.

For the Multiply function the weakest possible precondition is the
condition that Multiply requires - that the product of the two actual
parameters is a valid Integer.

[...]
> Hope you are not too much tired with my beginner's questions.
Not a problem - and it's one of the functions of c.l.a to provide a
forum for such questions.  (You'll know when I get tired of answering
because I'll stop :-)

Cheers,

Phil

Re: SPARK understand me very well... me neither

[Yannick Duchêne (Hibou57)]

Le Sat, 14 Aug 2010 21:08:43 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
>> Le Sat, 14 Aug 2010 18:04:23 +0200, Phil Thornley  
>> <phil.jpthorn...@gmail.com> a écrit:
> [...]
>> > For this particular example, I don't understand why you haven't used
>> > the obvious precondition:
>> > --# pre A * B in Integer;
>>
>> Because I did not knew this was feasible.
> OK - that seems a pretty good reason :-)
If you feel so, nothing bad so :)

But what seems important to me and I would to underline, was also that if  
I did not knew this was possible, this was because it was fr from my mind.  
And this was far from my mind, because looking at it as-is, I would have  
said “what does it prove ? what does it offer ?”. In short, this looks  
like a bad logical interface to me.

Well, as said, the case is special here : an example posted at Rosetta,  
and this have special requirements.

But if this was for a real project, I am pretty sure I would have insisted  
to go on with a pre-condition which would have offered something  
(something to help the client of the function to setup a valid context or  
to prove a given invokation context is valid). As-is, I feel this simply  
discharge all of the proof responsibility on the client side. That is why  
this kind of idea was very far from my mind. Otherwise, about the use of "  
... in Type_Name" in a Check or Assert SPARK annotation, this is thing  
already done multiple me for me. This was just in the particular context,  
the one of a --# pre annonation, I've never imagine this could be an  
option.

By the way, that is true the proof may become very complex (at least  
relatively compared to the function is applies to). But it goes with proof  
as it goes with implementation : once done, this is done and you can invok  
the method/function as many time as you want.

The pre-condition also may seems complex too. But this may be valuable, or  
be a better logical interface in the long run, if this help the clients to  
figure out how and when the function may be legitimately used. That is the  
purpose of an interface after all.

I do not mean I desagree with you here, I just do not want to focus too  
much on that “I did not knew it was possible” which is mostly anecdotal  
here. The reason why I did not had this alternative in mind is far more  
important.

I feel we understand each other on this point any way. Just wanted to  
makes it explicit.

I have also opened a thread on fr.comp.lang.ada based on this experience  
and your valuable comments, just to get more opportunity to have talks  
about “The Art and the Way to do”, as I feel there are far too much few  
about it :( (I mean, not enough talks and experiences testimony about  
SPARK).

Have a nice day! :)


Yannick

Re: SPARK understand me very well... me neither

[Yannick Duchêne (Hibou57)]

Le Sat, 14 Aug 2010 22:48:05 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> just to get more opportunity to have talks about “The Art and the Way to  
> do”, as I feel there are far too much few about it :( (I mean, not  
> enough talks and experiences testimony about SPARK).

And by the way, this makes me feel like I am the sole clumsy stupid idiot  
facing difficulties with SPARK. At least I would feel less lonesome  
(laughing).

Re: SPARK understand me very well... me neither

[Jeffrey Carter]

On 08/14/2010 01:48 PM, Yannick Duchêne (Hibou57) wrote:
> Le Sat, 14 Aug 2010 21:08:43 +0200, Phil Thornley
>>> > For this particular example, I don't understand why you haven't used
>>> > the obvious precondition:
>>> > --# pre A * B in Integer;
>
> But what seems important to me and I would to underline, was also that
> if I did not knew this was possible, this was because it was fr from my
> mind. And this was far from my mind, because looking at it as-is, I
> would have said “what does it prove ? what does it offer ?”. In short,
> this looks like a bad logical interface to me.

It doesn't prove anything, and it's not supposed to. It's a precondition. It 
says, "This precondition must be true for this operation to give correct 
results." It is the caller's duty to meet the precondition.

-- 
Jeff Carter
"To Err is human, to really screw up, you need C++!"
Stéphane Richard
63

--- news://freenews.netfront.net/ - complaints: news@netfront.net ---

Re: SPARK understand me very well... me neither

[Yannick Duchêne (Hibou57)]

Le Sat, 14 Aug 2010 23:50:08 +0200, Jeffrey Carter  
<spam.jrcarter.not@spam.not.acm.org> a écrit:
> It doesn't prove anything, and it's not supposed to. It's a  
> precondition. It says, "This precondition must be true for this  
> operation to give correct results." It is the caller's duty to meet the  
> precondition.
I understand that objection ; but in the mean time, isn't it the purpose  
of an interface to ease use and to help to manage things ? The  
precondition is part of the interface as much as the function signature is  
after all.

I will need some time to try an imagine new approachs.

The one I was using until now was more looking mathematical proof (by the  
way, the same kind of you may have with VDM or something of the like),  
that is a step by step hypothesis -> conclusion -> new hypothesis -> new  
conclusion, each possibly referring to previous conclusions. That is the  
reason why I oftenly number each step and refer to these in conclusions as  
“... -- from (x) and (y)” where x and y are numbers of previous steps.  
Indeed, this approach does not seems to be well suited with SPARK and ends  
into unsolvable things. The fact it does not only validate proof, but also  
tries to prove things it-self is an important fact with consequences. This  
is not really a validator, this is half validator and half automatic  
prover. And this impacts the way it works. You cannot expect it to follow  
your step-by-step proof (because it may use this or that hypothesis its  
own way, possibly going into long backtrackings or explorations), and you  
cannot expect it to prove every things automatically (that point is  
obvious). This makes it unfamiliar to me, so I will have to figure some  
other ways to do with it.

Will have some opportunities, as I would like to test it on some other  
Rosetta examples (along with some personal uses I am planning and already  
started to test).

Re: SPARK understand me very well... me neither

[Yannick Duchêne (Hibou57)]

Le Sat, 14 Aug 2010 23:50:08 +0200, Jeffrey Carter  
<spam.jrcarter.not@spam.not.acm.org> a écrit:
>> But what seems important to me and I would to underline, was also that
>> if I did not knew this was possible, this was because it was fr from my
>> mind. And this was far from my mind, because looking at it as-is, I
>> would have said “what does it prove ? what does it offer ?”. In short,
>> this looks like a bad logical interface to me.
>
> It doesn't prove anything, and it's not supposed to. It's a  
> precondition. It says, "This precondition must be true for this  
> operation to give correct results." It is the caller's duty to meet the  
> precondition.

Reading you again, I understand I did not choose the good words. I should  
have said “what does it defines ?” (like defining what a valid context is,  
in a concrete way). Otherwise yes, this does not have to prove anything,  
and this can't, because nothing is provable at this level.

-- 
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.

Re: SPARK understand me very well... me neither

[Yannick Duchêne (Hibou57)]

Le Sat, 14 Aug 2010 18:04:23 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> So I would much prefer the simple and obvious version of the
> precondition and code to be the version on Rosetta Code so that anyone
> browsing that site for information about SPARK doesn't get a wrong
> view of the language.
Updated with this added comment :

> Note: how do you ensure then “A * B in Natural” ? Either with
> a proof prior to Multiply invokation or using another form
> of Multiply where input A and B would be restricted to a range
> which ensures the resulting product is always valid. Exemple :
>    type Input_Type is range 0 .. 10;
>    type Result_Type is range 0 .. 100;
> and had a version of Multiply using these types.
> On the other hand, if arguments of Multiply are constants, this
> is provable straight away.

I wanted to add this comment, because the How is of a practicable  
importance.


-- 
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.