On 26/02/2016 16:36, Damien Cassou wrote:
Alexandre Bergel <alexandre.ber...@me.com> writes:
I still do not understand. I would imagine something like:
foo
<precondition: #invariant>
<postcondition: #invariant>
self bar
Hi Damien,
Sorry for seeming pedantic but the concept is precise : when you express
an invariant it must be true for all code of your class.
(and they are several invariants for one class of course)
'Invariants' are conditions that do not change (hence the name)
they are about object state, they are not post or pre conditions they
are always true, in each methods, before and after
if you specify in which methods they are true, it means they could be
false in others and then they are not invariants by defintion ...
I have the same feeling. It looks strange to me that the precondition
itself decides where it applies. I have the impression that each method
should list its preconditions.
That said, I think your example would be:
foo
<precondition: myFooPrecondition>
<postcondition: myFooPostcondition>
or something like:
foo
<precondition: myFooPrecondition1, myFooPrecondition2 etc...>
<postcondition: myFooPostcondition1, myFooPostcondition2 etc...>
you would say in each method what check applies.
That could be possible and the result would be the same
IMHO a bit less flexible, but another option.
Q: where would you define the invariants ?
a method that is never call and is tagged ?
myFooInvariant1
<invariant>
--
Alain
