[fpc-pascal] class contracts [[was: Re: Optional param modifier]]
Martin Frb
lazarus at mfriebe.de
Mon Apr 15 12:34:58 CEST 2019
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.
More information about the fpc-pascal
mailing list