[fpc-pascal] class contracts [[was: Re: Optional param modifier]]

[Martin Frb]

On 15/04/2019 09:41, Sven Barth via fpc-pascal wrote:
> Am 14.04.2019 um 23:48 schrieb Martin Frb:
>> type
>>   TFoo= class
>>      function DoTheFooThing(Foo1, Foo2: TFoo): Tbar;
>>         requires
>>            assigned(Foo1) or assigned(Foo2): 'Need at least 1 foo, 
>> for the connection';
>>         guarantees // better than ensure
>>            assigned(result);
>>            result.KnowsMyFoo = true: 'Connection exists';  // the 
>> =true is redundant
>>     procedure DoTheBar;
>>   end;
>>
>> It is to be noted, that requires and guarantees contain conditions 
>> (expressions), not pascal code. So technically it is ok, that they 
>> are in the interface and not implementation.
>> If I want something in the implementation, I can use normal "assert" 
>> (which by the way, have often great documenting value)
> The problem is that both "require" and "ensure" can check for fields 
> as well (think of a setter for example or something that changes the 
> state). Thus you could use a field name that the compiler does not yet 
> know. So you would need to order your methods in a order dictated by 
> the compiler due to the method's implementation instead of an order of 
> your own choosing.
>
> And yes, that would also be a problem with "class invariants", though 
> there it's more clear if we say that only identifiers can be used that 
> have been declared before as it's the same with properties and their 
> setters/getters.

Also to be ask if properties can have contract conditions. Especially 
thinking of indexed properties, where the index is a constant. Several 
properties using the same getter/setter (with diff index) may have 
different conditions for the contract.

Yes accessing fields is valid. Though easily leads to confusion what 
should and what should not be in the contract. (Yet that is not to be 
enforced...)
I saw an example, where the "ensure" of a setter checked that the field 
was set. That may be valid, but it also may have been something for a 
normal assert. Depends on the intend.
The ensure (again I prefer guarantees) is a contract. (between the 
class/method and someone else).
So if the check for the field is an internal detail, it should be a 
normal assert.  (the getter result, could be part of the contract then / 
that is different)

Only a normal assert is not quite the same. Contracts are checked too, 
if an inherited overwritten method is called. Assert are not (not if 
there is no call to inherited).
So a contract post condition could be used to make sure that any 
overwritten setter method will have changed the field. In that case the 
partner in the contract is the inherited class. And the post condition 
is less of a guarantee, but more a hidden requirement to the contract 
partner.

Anyway about the field order.... (and there could be circular 
requires/guarantees)
It would be an option to specify the contract details deferred

type
   TFoo= class
      function DoTheFooThing(Foo1, Foo2: TFoo): Tbar;
      procedure DoTheBar;
// need full declaration, could be overloaded // may skip param names?, 
just types should be ok
      requirements for DoTheFooThing(Foo1, Foo2: TFoo): Tbar;
            assigned(Foo1) or assigned(Foo2): 'Need at least 1 foo, for 
the connection';
      guarantees for DoTheFooThing(TFoo, TFoo): Tbar;
            assigned(result);
            result.KnowsMyFoo = true: 'Connection exists';  // the =true 
is redundant
   end;

Bit awkward because you need the full signature....
The compiler could allow both the "requires" right after the method, and 
the deferred "requirement for"

Alternative (but I do like that even less) named forward requirements
type
   TFoo= class
      function DoTheFooThing(Foo1, Foo2: TFoo): Tbar; requires 
'WhatTheFooWants';
      procedure DoTheBar;
      requirements for WhatTheFooWants;
            assigned(Foo1) or assigned(Foo2): 'Need at least 1 foo, for 
the connection';
   end;

That way, 2 methods could refer to the same requirements block.
Then it could even be possible to refer to several blocks....
      function DoTheFooThing(Foo1, Foo2: TFoo): Tbar; requires 
'WhatTheFooWants', 'TheFooSpecials';

But this will make it hard to read. Especially in the reverse, if you 
are in a named requirement block, it is not easy to find all methods 
that are affected by it.

Anyway just throwing in some ideas and possibilities.