Re: SPARK problem with unconstrained arrays

[phil.clayton@lineone.net]

On Tuesday, 3 March 2015 09:41:35 UTC, Maciej Sobczak  wrote:
> After some exploration I can answer my own question: empty slices.
> 
> Solution: add precondition to the Find_Min procedure:
> 
>     procedure Find_Min (A : in My_Array; I : out Index)
>         with Pre => A'First <= A'Last,
>              -- ...

Interestingly, this precondition was known to be necessary before your package body even existed: in the postcondition, there is no way that the predicate
  I in A'Range
could be satisfied if A is empty (and A does not change because it is an 'in' parameter).

There is a theoretical method for determining a 'minimum' precondition of a specification - that is, the condition under which the specification is achievable.  Just existentially quantify over the 'changed' variables, in your case I:

  ∃ I : Index ⦁
    I ∈ A'Range ∧
      (∀ J : A'Range ⦁ A (I) ≤ A (J)) 

That's a predicate whose only free variable is A, so it says something about A.  Unfortunately, it's not obvious what.  That's probably equivalent to A is not empty in the context of A : My_Array.  In one direction the proof is trivial but in the other, you probably have to start by showing that a non-empty set of integers has a least element...  It's this sort of thing that gave formal methods a bad name.

Phil