Re: Design by contract and control inversion

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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