Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 27.10.15 21:04, Dmitry A. Kazakov wrote:
> On Tue, 27 Oct 2015 17:43:36 +0100, G.B. wrote:
>
>> On 27.10.15 16:26, Dmitry A. Kazakov wrote:
>>> How do you know if some callers would not appreciate Status_Error as
>>> a possible outcome?
>>
>> Actually, this situation is what contracts are made for,
>> I think:
>> as a caller, you say what you want the procedure to do,
>> or else you don't sign this contract. I.e., a redesign
>> via ECR is in order before you sign.
>
> Sure, except that you don't subscribe the contract you cannot fulfill.

Yes, an impasse is a possible situation when negotiating contracts.
The interests of the business people will give way to at least
one resolution.

> The point can be summarized this way. If an exception is a part of the
> contract then Status_Error is much better than Constraint_Error

"Better than Assertion_Error?" I understand we are going to get

    subtype Open_File is File with Predicate =>
       Is_Open(Open_File) or else raise Status_Error with "...";

If the Predicate is associated with a subtype, the "specializing"
message after WITH cannot very special. It can be more special when
associated with a subprogram, though. But it can be special in
any case.
  
> If the contract is not to raise, then, firstly, there is no
> way to enforce it,

Enforcing it appears possible in the above case, at least for each
single program involving file objects, IIUC.

> and, secondly, if there were a way, proving no
> Status_Error would be no harder than no Constraint_Error. Ergo, no use.
  
Whenever one defines "use" to have the same meaning as "proof",
then the argument is an elaborate tautology. Now that will be an almost
useless definition 8-)

However, another use of predicates is to document assumptions.
If the assumptions are correct, but the compiler cannot determine
their truth, should we hide the assumptions?

Is it possible to redesign the subtypes etc below, making them
private types instead, so that the compiler "knows" all objects
to have the desired properties? What's the impact on O(?)?

package Conj is

    --
    --  dumb tests; we actually know all the numbers, the point is
    --  to be able to refer to them in assumptions, for the contract.
    --

    subtype Candidate is Positive range 2 .. Positive'Last;

    function Is_Prime (N : Candidate) return Boolean
      is (not (for Some X in 2 .. Candidate'Pred(N) => N rem X = 0));

    subtype Known_Range is Natural
      range 0 .. Natural'Min (Natural'Last, 4 * 10**17);

    subtype GN is Known_Range with Predicate =>   --  dynamic
      (if
         GN >= 4 and GN rem 2 = 0
       then (for Some A in 2 .. GN =>
               (for Some B in 2 .. GN =>
                  Is_Prime (A) and Is_Prime (B)
                  and GN = A + B)));

end Conj;

Running an unnecessary test may burn a CPU core,

with Conj;
procedure Test_Conj
is
    Test : constant Conj.GN := 1234567890;
begin
    null;
end Test_Conj;