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

[Phil Thornley <phil.jpthornley@gmail.com>]

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