Design by contract and control inversion

Design by contract and control inversion

[Yannick Duchêne (Hibou57)]

Hi all,

I wondered if there are known idioms to express predicates for callbacks,  
which may be via access to subprogram or interface/tagged types. Control  
inversion seems to not be easily mixable with design by contract. An  
example to make it clearer.

Say a type `T` has a method with expect either an access to subprogram or  
an interface:


     type T is private;

     procedure Expect_Handler
       (Me : T;
        Handler : not null access
           procedure (Context : T));

     type H is interface;

     procedure Handle
       (Me : H; Context : T)
        is abstract;

     procedure Expect_Handler
       (Me : T;
        Handler : H'Class);


Now let say the type `T` has different properties, and one is always  
`True` when no handler in currently invoked, and always `False` when an  
handler is currently running (which may be nesting), so that from inside  
of any `Handle` interface method of subprogram, then that property will  
always be `False`, and that I want it to be part of the specification.

I can't make it a precondition for the `Handle` method of type `H`, that  
would not be clean and not what's really intended. Worst, I can't express  
anything at all with the access to subprogram case.

The only thing I could imagine, is to create a second type, `U`,  
re‑interfacing `T`, and passed to the handlers instead of `T`:


     type T is private;

     type U (<>) is limited private;

     procedure Expect_Handler
       (Me : T;
        Handler : not null access
           procedure (Context : U));

     type H is interface;

     procedure Handle
       (Me : H; Context : U)
        is abstract;

     procedure Expect_Handler
       (Me : T;
        Handler : H'Class);


And in the private part, one of `U` or `T` wraps the other (within a  
record). Not that clean, but at least, `T` and `U` can expose different  
properties, and `U` is only used to be passed as parameters to handlers.  
This construct is not only interesting for design by contract, as it also  
allows to expose a different subprogram set for both type; as an example,  
in the real thing I did, `U` only gets a subset of the subprograms  
applicable to `T`.

Do you believe that's the best way to do? Or is this too much tricky and  
you know another idiom?


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Design by contract and control inversion

[Yannick Duchêne (Hibou57)]

Le Wed, 31 Oct 2012 20:28:30 +0100, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> The only thing I could imagine, is to create a second type, `U`,  
> re‑interfacing `T`, and passed to the handlers instead of `T`:
>
>
>      type T is private;
>
>      type U (<>) is limited private;
>
> […]
>
> […] in the real thing I did, `U` only gets a subset of the subprograms  
> applicable to `T`.

May make one feels it would be better to expression the subset relation  
with a type relation, i.e. type `T` would be a derived type of `U` (hence,  
`U`'s properties, is a subset of that of `T`).

Unfortunately, doing this:


     type U (<>) is tagged limited private;

     type T is new U with private;


… leads into an issue: you want to disallow any instance of `U` to be  
created (the reason of the unknown discriminant), but this also disallow  
instantiation of `T` as‑is, as `T` inherits the unknown discriminant. Can  
have a `Create` or `Instance` function, but would be cleaner to be able to  
get ride of this unknown discriminant. If `T` adds capabilities to `U`, it  
should be able to get ride of it, isn't it?

That make me feel again that use of the unknown discriminant is too much  
like a hack, when you just want to disallow instantiation from the client  
side. Would be nice to have something to directly express it, not  
involving any discriminants, which is a separate concept (indeed, the full  
view of the type, does not have, and does not need any).

There use to be thread on that topic, but can't remember which one it was.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Design by contract and control inversion

[Adam Beneschan]

On Wednesday, October 31, 2012 12:28:33 PM UTC-7, Hibou57 (Yannick Duchêne) wrote:
> Hi all, 
> 
> I wondered if there are known idioms to express predicates for callbacks,   
> which may be via access to subprogram or interface/tagged types. Control   
> inversion seems to not be easily mixable with design by contract. An   
> example to make it clearer. 
> 
> Say a type `T` has a method with expect either an access to subprogram or   
> an interface: 
> 
> 
>      type T is private; 
> 
>      procedure Expect_Handler 
>        (Me : T; 
>         Handler : not null access 
>            procedure (Context : T)); 
> 
>      type H is interface; 
> 
>      procedure Handle 
>        (Me : H; Context : T) 
>         is abstract; 
> 
>      procedure Expect_Handler 
>        (Me : T; 
>         Handler : H'Class); 
> 
> 
> Now let say the type `T` has different properties, and one is always   
> `True` when no handler in currently invoked, and always `False` when an   
> handler is currently running (which may be nesting), so that from inside   
> of any `Handle` interface method of subprogram, then that property will   
> always be `False`, and that I want it to be part of the specification. 


Let me see if I understand correctly.  You have a package that defines
T and some operations on T, including Expect_Handler (which in real
life would probably be some useful operation on T that could call the
callback).  (1) You want human users of the package to know that, when
they write the procedure My_Handler that will be passed to
Expect_Handler, that My_Handler can count on a particular property of
T being false.  (2) You also want users to know that they can count on
that property of T being true at other times.

Well, the first thing to do is to write a comment in your package
specification saying so.  

It seems that you want something more formal than just a comment,
though.  While I can understand why you'd want to do this, I don't
think it's feasible in Ada.  As far as #1 is concerned, Ada doesn't
have a syntax for adding preconditions or postconditions to an
access-procedure parameter.  I can see how this feature might be
useful, so that when Expect_Handler calls Handler.all, the compiler
would generate the checks before and/or after the call.  But it
doesn't exist right now.  As for #2, I can't imagine any language ever
supporting anything like this, since I can't even imagine how one
would express the concept of "other times" in a computer language.

My concern is that you're trying to come up with a "solution", but
you're thinking of solutions that, in my opinion, will make the
specification more obscure to a reader.  What's the gain in that?  To
me, "design by contract" is more of an approach to software design,
rather than a language feature; language features can help support
this design approach, but the language features are not themselves
"design by contract".  (Thus, I think your earlier statement that
"control inversion seems not be easily mixable with design by
contract" is a fallacy; I think they go together just fine, it's just
that we don't yet know how to add language support for it yet.)

To me, the important thing is that you have the contract in mind when
you design the package, and you express it in a way so that other
programmers who are using this package will know what conditions are
expected of their code, and what conditions they have a right to
expect from yours.  If the only way to do that is with comments, then
do it that way.  But since that's the important thing, trying to come
up with a tricky or idiomatic "solution" to your problem would tend to
defeat your purpose more than to serve it.  Unless, that is, there's
some other purpose you really, really need to accomplish.  If so, then
you'll probably have to provide more specific details about the code
you're trying to design.

Just my opinion.....  I'm sure others will differ.

                                -- Adam

Re: Design by contract and control inversion

[Yannick Duchêne (Hibou57)]

Le Thu, 01 Nov 2012 21:29:49 +0100, Adam Beneschan <adam@irvine.com> a  
écrit:
> Let me see if I understand correctly.  You have a package that defines
> T and some operations on T, including Expect_Handler (which in real
> life would probably be some useful operation on T that could call the
> callback).  (1) You want human users of the package to know that, when
> they write the procedure My_Handler that will be passed to
> Expect_Handler, that My_Handler can count on a particular property of
> T being false.  (2) You also want users to know that they can count on
> that property of T being true at other times.

Yes, that's it.

> It seems that you want something more formal than just a comment,
> though.  While I can understand why you'd want to do this, I don't
> think it's feasible in Ada.  As far as #1 is concerned, Ada doesn't
> have a syntax for adding preconditions or postconditions to an
> access-procedure parameter.  I can see how this feature might be
> useful, so that when Expect_Handler calls Handler.all, the compiler
> would generate the checks before and/or after the call.  But it
> doesn't exist right now.

I more hardly see the same with the interface type (instead of an access  
to sub-program).

> My concern is that you're trying to come up with a "solution", but
> you're thinking of solutions that, in my opinion, will make the
> specification more obscure to a reader.  What's the gain in that?

I tried, and when I saw this was too difficult, I gave up. I ended with  
the solution posted elsewhere in this thread, which is to use another type  
for the parameter passed to the handler. But that created some other  
issues worth to be discussed (will be back with it later).

>  To me, "design by contract" is more of an approach to software design,
> rather than a language feature; language features can help support
> this design approach, but the language features are not themselves
> "design by contract".

Not sure I've understood, but I will try. The comment seems interesting.

> To me, the important thing is that you have the contract in mind when
> you design the package, and you express it in a way so that other
> programmers who are using this package will know what conditions are
> expected of their code, and what conditions they have a right to
> expect from yours.  If the only way to do that is with comments, then
> do it that way.

I did it that way. For the time, “other programmers” is just me (some  
others may have opportunities to see it, but that's for a far later time).

> But since that's the important thing, trying to come
> up with a tricky or idiomatic "solution" to your problem would tend to
> defeat your purpose more than to serve it.

Sometime it's not easy to see if you just fail to properly setup a design  
which may be good, or if it's just the design which is wrong. At least,  
that's good experiments to remember about. I'm currently facing a similar  
question, trying to mimic SML's signatures using Ada generics and  
interface types.

I may post part of the specification in this thread, to request people for  
comments. Will be useful to know if whether or not it's clear enough and  
understandable (just don't expect anything wonderful, that's a stupidly  
simple thing apart of the question raised here).


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Design by contract and control inversion

[Yannick Duchêne (Hibou57)]

Le Fri, 02 Nov 2012 04:40:44 +0100, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> I may post part of the specification in this thread, to request people  
> for comments. Will be useful to know if whether or not it's clear enough  
> and understandable (just don't expect anything wonderful, that's a  
> stupidly simple thing apart of the question raised here).

Here is… reading Adam, I get the idea to post an excerpt to ensure it's  
intelligible enough. That does not really stand for the real thing, I'm  
just posting an intermediate thing, which is enough to looks useful, but  
lacks many things. Hope that's not too long for a Usenet post.

Although I decided to use a façade type, I still could not avoid to put  
some preconditions at multiple place. Comment explains why (in short,  
that's due to the remaining ability to access the object via other paths  
than the one provided to the handler sub-program).


     -- abc.ads

     package ABC is

        pragma Pure;

     end ABC;

     -- abc-sets.ads

     package ABC.Sets is

        pragma Pure;

     end ABC.Sets;

     -- abc-sets-base.ads

     generic

        type Element_Type is private;
        type Cardinal_Type is (<>);

     package ABC.Sets.Base is

        type Instance_Type is limited interface;

        Read_Unassigned   : exception;
        Update_Unassigned : exception;

        -- An implementation may raise the above exceptions, even
        -- when pre/post assertions are not enabled.

        --  
------------------------------------------------------------------------

        function Is_Assigned
          (Instance : Instance_Type)
           return Boolean
           is abstract;
        -- For pre/post assertions and defensive design.

        --  
------------------------------------------------------------------------

        procedure Add
          (Instance : in out Instance_Type;
           Element  : in Element_Type)
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance);

        procedure Add
          (Instance : in out Instance_Type;
           Other    : in Instance_Type)
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance) and
              Is_Assigned (Other);

        procedure Assign
          (Instance : in out Instance_Type;
           Element  : in Element_Type)
           is abstract
           with Post'Class =>
              Is_Assigned (Instance);

        procedure Assign
          (Instance : in out Instance_Type;
           Other    : in Instance_Type)
           is abstract
           with
              Pre'Class => Is_Assigned (Other),
              Post'Class => Is_Assigned (Instance);

        function Cardinal
          (Instance : in Instance_Type)
           return Cardinal_Type
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance);

        function Create
           return Instance_Type
           is abstract;
           -- `Is_Assigned` may or may not be `True`, depending
           -- on concrete implementation's choice.

        function Equal
          (Instance : in Instance_Type;
           Other    : in Instance_Type)
           return Boolean
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance) and
              Is_Assigned (Other);

        function Has
          (Instance : in Instance_Type;
           Element  : in Element_Type)
           return Boolean
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance);

        function Has
          (Instance : in Instance_Type;
           Other    : in Instance_Type)
           return Boolean
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance) and
              Is_Assigned (Other);

        procedure Remove
          (Instance : in out Instance_Type;
           Element  : in Element_Type)
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance);

        procedure Remove
          (Instance : in out Instance_Type;
           Other    : in Instance_Type)
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance) and
              Is_Assigned (Other);
           -- Concrete implementations must consider the case
           -- where `Instance` and `Other` refers (directly or indirectly)
           -- to the same object, whether what "object" is for the
           -- implementation.

     end ABC.Sets.Base;

     -- abc-sets-functional.ads

     -- Functional set.
     --
     -- The functional behaviour, its absence of dependencies to side
     -- effects during evaluation, provides optimization opportunities
     -- for concrete implementations.
     --
     -- A classic interface would leave, to create complex expressions,
     -- no other choices than using regular functions each returning
     -- a sub-expression. An alternative is to directly write to
     -- a target result object instead, avoiding returns from function
     -- and passing to functions parameters. A simple and safe  
implementation
     -- may still go this way, and use an result object per sub-expression.
     -- A optimized implementation may benefits from the enforced no-side
     -- effect behaviour (whether or not an element is set, does not depends
     -- on whether or not another element is set).

     with ABC.Sets.Base;

     generic

        with package Base is new ABC.Sets.Base (<>);

     package ABC.Sets.Functional is

        type Expression_Type is limited interface;
        subtype Expression_Class is Expression_Type'Class;
        -- Instead of a function returning a set, an expression,
        -- is a subprogram writing to a result target object. The
        -- concrete implementation is responsible for the object
        -- passed to be written to. The sub-program then write
        -- its sub-expression to it, using basic methods such as
        -- `Add`, `Remove` and so on.

        subtype Element_Type is Base.Element_Type;
        subtype Cardinal_Type is Base.Cardinal_Type;

        type Instance_Type is limited interface and Base.Instance_Type;
        subtype Instance_Class is Instance_Type'Class;

        type Instance_Write_Only_Type is limited interface;
        subtype Instance_Write_Only_Class is Instance_Write_Only_Type'Class;
        -- A restricted façade to an `Instance_Type`: no read methods,  
intended
        -- to be written to only, as a target result object. It enforce the
        -- functional semantic, via type safety. If an expression  
sub-program
        -- attempts to modify or read the target set (ex. using an object in
        -- its scope), then an error is raised. This case cannot avoided by
        -- type safety mechanisms, and runtime checks are still required to
        -- prevent it (see `Is_Being_Assigned`).

        Illegal_Assignment : exception;
        Illegal_Operation  : exception;
        Illegal_Read       : exception;
        Nesting_Limit      : exception;
        Self_Dependency    : exception;

        -- The above exceptions may be raised by an implementation, even
        -- when pre/post assertions are disabled.

        --  
------------------------------------------------------------------------

        function Is_Being_Assigned
          (Instance : Instance_Type)
           return Boolean
           is abstract;
        -- Property used for runtime checks of the functional semantic (for  
the
        -- part of it which cannot be ensured by type safety).

        --  
------------------------------------------------------------------------

        procedure Add
          (Instance : in out Instance_Write_Only_Type;
           Element  : in Element_Type)
           is abstract;

        procedure Add
          (Instance   : in out Instance_Write_Only_Type;
           Expression : in Expression_Class)
           is abstract;

        procedure Add
          (Instance : in out Instance_Write_Only_Type;
           Other    : in Instance_Class)
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance_Type (Other)) and
              not Is_Being_Assigned (Instance_Type (Other));

        procedure Remove
          (Instance : in out Instance_Write_Only_Type;
           Element  : in Element_Type)
           is abstract;

        procedure Remove
          (Instance   : in out Instance_Write_Only_Type;
           Expression : in Expression_Class)
           is abstract;

        procedure Remove
          (Instance : in out Instance_Write_Only_Type;
           Other    : in Instance_Class)
           is abstract
           with Pre'Class =>
              Is_Assigned (Instance_Type (Other)) and
              not Is_Being_Assigned (Instance_Type (Other));

        --  
------------------------------------------------------------------------

        procedure Evaluate
          (Expression : in Expression_Type;
           Result     : in out Instance_Write_Only_Type'Class)
           is abstract;
           -- `Expression` has `in` mode, so that it can be the one
           -- returned by a function.
           --
           -- The `in` mode `Result` holds, does not mean it is readable
           -- (see some of the comments above). That's just required for any
           -- implementation to get a chance to be feasible.

        --  
------------------------------------------------------------------------

        -- `Expression`'s `Evaluate` methods, will receive `Instance`
        -- behind an `Instance_Write_Only_Type` façade.
        --
        -- During `Evaluate`, `Is_Being_Assigned (Instance)` is `True`.

        procedure Assign
          (Instance   : in out Instance_Type;
           Expression : in Expression_Class)
           is abstract
           with Post'Class =>
              Is_Assigned (Instance);
           -- The old status of the instance, may or may not be  
`Is_Assigned`.
           -- An implementation must support both cases.

        --  
------------------------------------------------------------------------

        -- Only root level modification allowed. No modification, nor read
        -- access allowed, while it is being evaluated by an expression
        -- sub-program (which may be nesting).

        overriding procedure Add
          (Instance : in out Instance_Type;
           Element  : in Element_Type)
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance);

        overriding procedure Add
          (Instance : in out Instance_Type;
           Other    : in Instance_Type)
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance) and
              not Is_Being_Assigned (Other);

        overriding procedure Assign
          (Instance : in out Instance_Type;
           Element  : in Element_Type)
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance);

        overriding procedure Assign
          (Instance : in out Instance_Type;
           Other    : in Instance_Type)
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance) and
              not Is_Being_Assigned (Other);

        overriding function Cardinal
          (Instance : in Instance_Type)
           return Cardinal_Type
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance);

        overriding function Equal
          (Instance : in Instance_Type;
           Other    : in Instance_Type)
           return Boolean
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance) and
              not Is_Being_Assigned (Other);

        overriding function Has
          (Instance : in Instance_Type;
           Element  : in Element_Type)
           return Boolean
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance);

        overriding function Has
          (Instance : in Instance_Type;
           Other    : in Instance_Type)
           return Boolean
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance) and
              not Is_Being_Assigned (Other);

        overriding procedure Remove
          (Instance : in out Instance_Type;
           Element  : in Element_Type)
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance);

        overriding procedure Remove
          (Instance : in out Instance_Type;
           Other    : in Instance_Type)
           is abstract
           with Pre'Class =>
              not Is_Being_Assigned (Instance) and
              not Is_Being_Assigned (Other);

     end ABC.Sets.Functional;



(you were warned, that's nothing wonderful)


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Design by contract and control inversion

[Yannick Duchêne (Hibou57)]

Le Fri, 02 Nov 2012 09:59:53 +0100, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> […]
>      package ABC.Sets.Base is
>
> […]
>      package ABC.Sets.Functional is
>

Out of the primary topic, but a tiny tip I forgot while posting the  
excerpts (as it may be worth to people discovering Ada).

Replace the beginning of `ABC.Sets.Base`, with the following:


     package ABC.Sets.Base is

        package Formals is
           subtype Element_Type is Base.Element_Type;
           subtype Cardinal_Type is Base.Cardinal_Type;
        end Formals;


Then replace the beginning of `ABC.Sets.Functional` with the following:


     package ABC.Sets.Functional is

        package Formals is
           package Base renames Functional.Base;
        end Formals;


That's a useful tip, which will allow you to access the formal parameters  
of an instance of a generic package, whenever needed. Otherwise, as an  
example, `Base.Cardinal_Type` won't be visible from outside of its  
hierarchy, if ever you needed to refer to it this way. Instead of  
`Base.Cardinal_Type` you will then do `Base.Formals.Cardinal_Type`, and  
will be OK. This question used to be discussed about two years ago on this  
Usenet.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Design by contract and control inversion

[Shark8]

On Wednesday, October 31, 2012 1:28:33 PM UTC-6, Hibou57 (Yannick Duchêne) wrote:
> Hi all,
> 
> I wondered if there are known idioms to express predicates for callbacks,  
> which may be via access to subprogram or interface/tagged types.

Hm, it seems to me that you could have an intermediate/pass-through handler.
(It would be rather limited, unless you make pre-/post-condition parameters... and if you do that it could get cumbersome quick.)
[NOTE: Not compiled or checked, just brainstorming/psudocode.]

Type Obj_Handle is not null access Object'class;
Type Handler is Access Procedure ( A, B : Integer; C : Obj_Handle );

-- this version applies the same preconditions to all handlers.
Procedure Intermediate (A, B : Integer; C : Obj_Handle; D : Handler)
   with Inline, pre => A > 0 or B in positive'Range;

Procedure Intermediate (A, B : Integer; C : Obj_Handle; D : Handler) is
begin
   D( A, B, C );
end;

To extend these with pre-/post-conditions we could add another type and another parameter to the handler.

Type Condition is access function( P : Parameter ) return Boolean;
Type Conditions is record
  Pre, Post : Condition;
end record;

-- This version applies the psudo-pre/post-conditions, as supplied.
Procedure Intermediate (A, B : Integer; C : Obj_Handle; D : Handler; E : Conditions) with inline,
 pre  => (if condition'(E.Pre)  /= Null then E.Pre),
 post => (if condition'(E.Post) /= Null then E.Post);
Procedure Intermediate (A, B : Integer; C : Obj_Handle; D : Handler; E : Conditions) is
begin
   D( A, B, C );
end;


Or something like it, no?

Re: Design by contract and control inversion

[Yannick Duchêne (Hibou57)]

Le Fri, 02 Nov 2012 09:59:53 +0100, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
>      -- abc-sets-base.ads
>
>      generic
>
>         type Element_Type is private;
>         type Cardinal_Type is (<>);
>
>      package ABC.Sets.Base is

As it was posted, a note on this.

The `Cardinal_Type` is just a discrete type here, which may looks  
over‑generalized to somebodies, and indeed the standard Ada containers use  
a range type instead. The discrete type is enough even for a  
implementation, but if you wish to add pre/post condition on the  
cardinality in the specification, then a discrete type becomes a burden  
(unless you enjoy Peano arithmetic a lot). There's no real rule here, that  
just depends… Just still one thing: that's always OK to change from the  
discrete type to a range type, but not the opposite; so that may be better  
to start with the discrete type and change this later if required.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Design by contract and control inversion

[Yannick Duchêne (Hibou57)]

Le Fri, 02 Nov 2012 17:45:33 +0100, Shark8 <onewingedshark@gmail.com> a  
écrit:

> On Wednesday, October 31, 2012 1:28:33 PM UTC-6, Hibou57 (Yannick  
> Duchêne) wrote:
>> Hi all,
>>
>> I wondered if there are known idioms to express predicates for  
>> callbacks,
>> which may be via access to subprogram or interface/tagged types.
>
> Hm, it seems to me that you could have an intermediate/pass-through  
> handler.
> (It would be rather limited, unless you make pre-/post-condition  
> parameters... and if you do that it could get cumbersome quick.)
> [NOTE: Not compiled or checked, just brainstorming/psudocode.]
>
> Type Obj_Handle is not null access Object'class;
> Type Handler is Access Procedure ( A, B : Integer; C : Obj_Handle );
>
> -- this version applies the same preconditions to all handlers.
> Procedure Intermediate (A, B : Integer; C : Obj_Handle; D : Handler)
>    with Inline, pre => A > 0 or B in positive'Range;
>
> Procedure Intermediate (A, B : Integer; C : Obj_Handle; D : Handler) is
> begin
>    D( A, B, C );
> end;
>
> To extend these with pre-/post-conditions we could add another type and  
> another parameter to the handler.
>
> Type Condition is access function( P : Parameter ) return Boolean;
> Type Conditions is record
>   Pre, Post : Condition;
> end record;
>
> -- This version applies the psudo-pre/post-conditions, as supplied.
> Procedure Intermediate (A, B : Integer; C : Obj_Handle; D : Handler; E :  
> Conditions) with inline,
>  pre  => (if condition'(E.Pre)  /= Null then E.Pre),
>  post => (if condition'(E.Post) /= Null then E.Post);
> Procedure Intermediate (A, B : Integer; C : Obj_Handle; D : Handler; E :  
> Conditions) is
> begin
>    D( A, B, C );
> end;
>
>
> Or something like it, no?

Yes, that could do the trick. But this is a bit too much for a  
specification, and even could not find a place in a specification, as Ada  
2012 does not allow procedures in package specs (just functions), unless  
I'm wrong with it.

Your idea made me think how again the interface type is the best: just  
give the precondition you gave to `Intermediate`, to the handler method of  
the interface type.

The only thing which still make me wish I could have something like this  
with access to sub‑program, is that access to sub‑program can get an  
access to an inner sub‑program (as long as it not to be stored, which is  
the case here); you can't do this with an interface type, as a type  
defined in a nested scope is not usable (an issue similar to the access  
level with named access type).

By the way, I've dropped the initial design which was not safe enough.  
Instead of adding preconditions everywhere, I will have an object which  
returns two kind of objects, one for read access and one for write access,  
and the relevant preconditions to ensure you can't have both read and  
write access at the same time, will be only on the two functions returning  
these two views. That's safer and simpler. I will just have to resign to  
not have any‑more an object exposing the two views (I initially wanted too  
much).


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University