Re: SPARK

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

Ok, from some branch of this thread, you may have learned a question have  
raised about which one of “assert” or “check” should be used to write  
in-text proofs where the Simplifier could not prove it it/his/her self.

The answer to this is so much important that I give the answer to it from  
the root of this thread, instead of from the latter leaf.

So it is : Use Check, not Assert.

Here is a concrete example of what you can do with Check and which does  
not work with Assert. The example is detailed, I mean, exposes detailed  
proofs, over what may have been sufficient. This is because I like  
explicit and expressive things, and this was also to be sure nobody could  
miss a single step of the proof and nobody could have any doubt about the  
usefulness of such a approach in software conception. That's also the  
reason why the exercise upon which this is based, was a bit modified (like  
using two intermediate variables instead of subexpressions.. I do that  
oftenly on my side).

Here is :


    procedure Limit
      (X     : in out Integer;
       Lower : in     Integer;
       Upper : in     Integer)
    --# pre    Lower < Upper;
    --# post  ((X~ < Lower) -> (X = Lower)) and
    --#       ((X~ > Upper) -> (X = Upper)) and
    --#       (X in Lower .. Upper);
    is
    begin
       if X < Lower then
          X := Lower;
       elsif X > Upper then
          X := Upper;
       end if;
    end Limit;

    function Percent_Of_Range
      (Data    : Integer;
       Lowest  : Integer;
       Highest : Integer) return Percent_Type
    --# pre    (Lowest < Highest) and
    --#        ((Highest - Lowest) <= Integer'Last) and
    --#        (((Highest - Lowest) * 100) <= Integer'Last);
    is
       Local_Data : Integer;
       Part       : Integer;
       Whole      : Integer;
    begin
       Local_Data := Data;
       -- Local copy of Data to be allowed to modify it. We only need
       -- a modified version locally, the caller does not need this.

       Limit
         (X     => Local_Data, -- in out.
          Lower => Lowest,     -- in
          Upper => Highest);   -- in.

       Part  := Local_Data - Lowest;
       Whole := Highest - Lowest;

       -- We are to prove that ((Part * 100) / Whole) is in 0 .. 100.

       -- (1) Prove that Part >= 0.
       --# check Local_Data in Lowest .. Highest;
       --# check Local_Data >= Lowest;
       --# check (Local_Data - Lowest) >= 0;
       --# check Part >= 0;

       -- Given (1), it's obvious that (Part * 100) >= 0.

       -- (2) Prove that Whole is > 0.
       --# check Lowest < Highest;
       --# check Highest > Lowest;
       --# check (Highest - Lowest) > 0;
       --# check Whole > 0;

       -- Given (2), it's obvious that ((Part * 100) / Whole) is valid.
       -- Given (1) and (2), it's obvious that ((Part * 100) / Whole) >= 0.

       -- (3) Prove that (Whole >= Part). This is required for (4) which is
       --    to come.
       --# check Local_Data in Lowest .. Highest;
       --# check Highest >= Local_Data;
       --# check (Highest - Lowest) >= (Local_Data - Lowest);
       --# check Whole >= Part;

       -- (4) Prove that ((Part * 100) / Whole) is less or equal to 100.
       --# check Part <= Whole;
       --# check (Part * 100) <= (Whole * 100);
       --# check ((Part * 100) / Whole) <= ((Whole * 100) / Whole);
       --# check ((Part * 100) / Whole) <= 100;

       -- (5) Prove that the subexpression (Part * 100) will not
       --     commit an overflow.
       --# check (((Highest - Lowest) * 100) <= Integer'Last);
       --# check (Whole * 100) <= Integer'Last;
       --# check Part <= Whole;
       --# check (Part * 100) <= Integer'Last;

       -- Given (1), we know ((Part * 100) / Whole) >= 0.
       -- Given (4), we know ((Part * 100) / Whole) <= 100.
       -- Given (5), we we know (Part * 100) will not commit an overflow.
       -- Given (1) and (2) and(5), the following statement is then proved  
to
       -- be valid and meaningful.

       return Percent_Type ((Part * 100) / Whole);

    end Percent_Of_Range;

A working example of a step by step proof of every things required to be  
proven.

Waaw... I like it so much, I love it. This is the way I was thinking  
software should be built for so long ! I was waiting for such a thing for  
about 14 years you know !

I use to learn about VDM when I was younger, hire books about it in  
libraries, use to think about creating my own implementation of VDM, but  
failed to find the language specification (and was frightened about the  
idea to setup my own language in this area).

And now, I see SPARK can do nearly the same.

Well, although wonderful, that's still not perfect : why is there a  
Checker (which I didn't used here) and why no provision to write in-text  
what is done with the Checker ? That's what I was attempting to do here.  
It works, but I miss something like explicit “from (1) and (2) infer ....  
” etc. I cannot give names or numbers to Check clauses and cannot  
explicitly refer to these. I cannot nor explicitly refer to precondition  
in inferences (like in (5), where the reference to a precondition is  
implicit, not explicit).

Is there some provision for such a thing ?

Yes, I may wish too much... that's not perfect, while still wonderful. Do  
you feel too ? :)


-- 
There is even better than a pragma Assert: an --# assert (or a --#  
check... question pending)