Removed duplicate "end" keyword from "check" example code. From PR #16574.

Author:halw
Date:2010-01-20T15:50:00.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@404 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
halw
2010-01-20 15:50:00 +00:00
parent e872c10c5e
commit 38636dc7de

View File

@@ -153,7 +153,7 @@ Because of the call to <code>some_feature</code>, the routine will only work if
but this is not the only possible scheme; for example if an <code>create x</code> appears shortly before the call we know <code>x</code> is not void and do not need the protection. It is a good idea in such cases to use a <code>check</code> instruction to document this property, if only to make sure that a reader of the code will realize that the omission of an explicit test (justified or not) was not a mistake. This is particularly appropriate if the justification for not testing the precondition is less obvious. For example <code>x</code> could have been obtained, somewhere else in the algorithm, as <code>clone (y)</code> for some <code>y</code> that you know is not void. You should document this knowledge by writing the call as but this is not the only possible scheme; for example if an <code>create x</code> appears shortly before the call we know <code>x</code> is not void and do not need the protection. It is a good idea in such cases to use a <code>check</code> instruction to document this property, if only to make sure that a reader of the code will realize that the omission of an explicit test (justified or not) was not a mistake. This is particularly appropriate if the justification for not testing the precondition is less obvious. For example <code>x</code> could have been obtained, somewhere else in the algorithm, as <code>clone (y)</code> for some <code>y</code> that you know is not void. You should document this knowledge by writing the call as
<code> <code>
check check
x_not_void: x /= Void end x_not_void: x /= Void
-- Because x was obtained as a clone of y, -- Because x was obtained as a clone of y,
-- and y is not void because [etc.] -- and y is not void because [etc.]
end end