bertrand@eiffel.UUCP (Bertrand Meyer) (02/09/90)
In message <226@eiffel.UUCP>, jacob@gore.com (Jacob Gore) asks with respect to the new form of creation operations (see ``Eiffel cleanup #1: The creation mechanis,'', <226@eiffel.UUCP>): > How exactly will the Invariant Rule read after this change? (It now > specifies a special case for the Create procedure.) Clearly, every creation procedure c must satisfy {defaults and pre_c} c {INV and post_c} where pre_c is the precondition of c, post_c is its postcondition, defaults is an assertion characterizing the object state resulting from default initializations, and INV is the class invariant. -- -- Bertrand Meyer bertrand@eiffel.com
jacob@gore.com (Jacob Gore) (02/10/90)
/ comp.lang.eiffel / bertrand@eiffel.UUCP (Bertrand Meyer) / Feb 8, 1990 / > > How exactly will the Invariant Rule read after this change? (It now > > specifies a special case for the Create procedure.) > > Clearly, every creation procedure c must satisfy > > {defaults and pre_c} c {INV and post_c} Yes, but if I understand the change correctly, a creation routine may be exported, in which case it also falls under the rule for exported routines: {INV and pre_c} c {INV and post_c} So, should there be a distinction between a creation routine being invoked during creation vs. it being invoked with a call? Jacob -- Jacob Gore Jacob@Gore.Com boulder!gore!jacob
bertrand@eiffel.UUCP (Bertrand Meyer) (02/17/90)
The question asked in <120013@gore.com> by jacob@gore.com (Jacob Gore) suggests its own answer: if a routine appears in both the creation clause and the export clause, it should satisfy both of the corresponding formal constraints. -- -- Bertrand Meyer bertrand@eiffel.com