mirrors/eiffel-org
1
0
Fork 0
mirror of https://github.com/EiffelSoftware/eiffel-org.git synced 2026-08-21 06:11:12 +02:00
Code Issues Packages Projects Releases Wiki Activity

Author:jfiat

Browse Source 
Date:2009-03-27T14:35:11.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@210 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
jfiat
2009-03-27 14:35:11 +00:00
parent ac2d81f047
commit 5d5de7df3d
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
documentation/current/method/eiffel-tutorial-et/et-inheritance.wiki
+1 -1
View File
@@ -467,7 +467,7 @@ where the postcondition of some routine <code>q</code> implies the precondition
The rule, then, is that for the redefinition to be correct the new precondition ''pre' ''must be weaker than or equal to the original ''pre'', and the new postcondition ''post' ''must be stronger than or equal to the original ''post''. The rule, then, is that for the redefinition to be correct the new precondition ''pre' ''must be weaker than or equal to the original ''pre'', and the new postcondition ''post' ''must be stronger than or equal to the original ''post''.
Because it is impossible to check simply that an assertion is weaker or stronger than another, the language rule relies on different forms of the assertion constructs, <code>else require</code> and <code>then ensure</code>, for redeclared routines. They rely on the mathematical property that, for any assertions <code>p</code> and <code>q,</code> <code>p implies (p or q)</code>, and <code>(p and q) implies p</code>. For a precondition, using <code>require else</code> with a new assertion will perform an <code>or</code>, which can only weaken the original; for a postcondition, <code>ensure then</code> will perform an <code>and</code>, which can only strengthen the original. Hence the rule: Because it is impossible to check simply that an assertion is weaker or stronger than another, the language rule relies on different forms of the assertion constructs, <code>require else</code> and <code>ensure then</code>, for redeclared routines. They rely on the mathematical property that, for any assertions <code>p</code> and <code>q,</code> <code>p implies (p or q)</code>, and <code>(p and q) implies p</code>. For a precondition, using <code>require else</code> with a new assertion will perform an <code>or</code>, which can only weaken the original; for a postcondition, <code>ensure then</code> will perform an <code>and</code>, which can only strengthen the original. Hence the rule:
{{rule|name=Assertion Redeclaration|text=In the redeclared version of a routine, it is not permitted to use a require or ensure clause. Instead you may: Introduce a new condition with require else, for or-ing with the original precondition. Introduce a new condition with ensure then, for and-ing with the original postcondition. In the absence of such a clause, the original assertions are retained. }} {{rule|name=Assertion Redeclaration|text=In the redeclared version of a routine, it is not permitted to use a require or ensure clause. Instead you may: Introduce a new condition with require else, for or-ing with the original precondition. Introduce a new condition with ensure then, for and-ing with the original postcondition. In the absence of such a clause, the original assertions are retained. }}