Re: Seeking for papers about tagged types vs access to subprograms

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 13-05-12 02:19 , Shark8 wrote:
> On Saturday, May 11, 2013 3:06:25 PM UTC-6, Niklas Holsti wrote:
>>
>> Well, why is Ada limited in this way? There is no real reason why an "in
>> out" parameter should have the same constraints on input and on output. 
> 
> What? Ada's not constrained like that, at least as you're implying:

When you declare an "in out" parameter, Ada now requires that you
specify the same subtype for both roles. In the example, if the File
parameter to Open is declared as "in out Closed_File", but Open tries to
change the parameter to (State => Is_Open, Handle => ...) a
Constraint_Error results at run-time.

> Given the types you have:
>>
>>    type File_State is (Is_Closed, Is_Open);
>>
>>    type File_Object (State : File_State := Is_Closed) is
>>    record
>>       case State is
>>       when Is_Closed => null;
>>       when Is_Open   => Handle : System.IO.File_Handle;
>>       end case;
>>    end record;
>>
>>    subtype Closed_File is File_Object (State => Is_Closed);
>>    subtype Open_File   is File_Object (State => Is_Open  ); 
> 
> the proper way to formulate _EXACTLY_ what you want is this:
> 
> procedure Read  (File : in out File_Object; ...)
>   with pre => File in Closed_File, post => file in Open_File;

(I think you mean "procedure Open" there, not "Read".)

As I said, it can be expressed with pre- and post-conditions in this
way, but then the parameter profile does not mention the subtypes and
instead uses the unconstrained type (here File_Object). As I also said,
I wanted the subtype changes to be visible in the subprogram profile, to
show more clearly (or at least, more traditionally) how the availability
of the subprogram depends on the state (i.e. the subtype) of the
parameter, and how it affects the state.

To condense my points:

1. The typestate concept, as implemented in the Plaid language, seems
(after my brief study of Plaid) to be implementable in Ada through
discriminated records with variants.

2. The influence of the current typestate of an object, on the set of
subprograms (operations) available for the object, can be represented as
constraints on the "in" subtype of the object, and the typestate changes
can be represented as the "out" subtype. In current Ada, of course, the
subtype checks in principle occur at run-time, so typestate correctness
is not checked at compile-time. Moreover, current Ada does not allow the
formal subtype (as written in the profile) to be different for the "in"
and "out" roles.

3. Those different "in" and "out" constraints can be implemented in Ada
2012 as pre/post-conditions, as you say.

4. A closer match to Plaid can be achieved if Ada is extended to allow
different subtypes for the "in" and "out" roles of an "in out" parameter.

As the pre/post-condition feature of Ada 2012 becomes more familiar,
perhaps the pre- and post-conditions will be seen as a more integrated
part of the subprogram's profile, and there is no reason to consider
changes to the formal subtypes allowed in the language (point 4).

On the other hand, it seems to me that there are other cases, not
perhaps related to typestate, where it would be natural to specify
different "in" and "out" subtypes for an "in out" parameter. Something
as simple as:

   procedure Increment (Counter : in out Natural)

could become

   -- Extended Ada:
   procedure Increment (
      Counter : in  Natural range 0 .. Natural'Last - 1
                out Positive);

Of course, all such different in/out constraints can be expressed using
the "heavy guns" of pre/post-conditions, so perhaps this suggestion is
out of date after Ada 2012. Any compiler powerful enough to do useful
typestate analysis based on the formal parameter subtypes is probably
able to do the same analysis using the corresponding
pre/post-conditions, at least when the conditions take the simple form
"parameter in subtype".

It is interesting that Randy thinks his ideas regarding a future
replacement for Ada resemble the typestate concept, but that the
typestate concept as implemented in Plaid seems to be implementable in
Ada 2012. Perhaps Randy's ideas go much further than this, however.

--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .