Author:halw

Date:2008-12-16T02:27:18.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@140 abb3cda0-5349-4a8f-a601-0c33ac3a8c38

documentation/current/platform-specifics/microsoft-windows/net/eiffel-net-language/eiffel-net/design-contract-and-assertions.wiki

@@ -59,8 +59,8 @@ feature -- Access
 
 Below is the code for a procedure <code>set_second</code> which receives an argument of type <code>INTEGER</code> and sets the value of the <code>second</code> feature to the argurment. 
 <code>
-	set_second (s: INTEGER) is
+    set_second (s: INTEGER)
-			-- Set the second from `s'
+            -- Set the second from `s'.
         do
             second := s
         end
@@ -70,8 +70,8 @@ The routine is simple enough, but there is a problem with it. Suppose a client c
 
 Consider though what we can do with Design by Contract. We will add a precondition assertion to <code>set_second</code> that expresses the need for valid arguments. 
 <code>
-	set_second (s: INTEGER) is
+    set_second (s: INTEGER)
-			-- Set the second from `s'
+            -- Set the second from `s'.
         require
             valid_argument_for_second: 0 <= s and s <= 59
         do
@@ -79,14 +79,14 @@ Consider though what we can do with Design by Contract. We will add a preconditi
         end
 </code>
 
-The precondition is introduced by the keyword " <code> require </code>". The text " <code> valid_argument_for_second </code>" is the label for the assertion clause. The boolean expression "0 <= <code> s </code> and <code> s </code> <= 59" says that a good value for <code> s </code> will be between 0 and 59 inclusive. 
+The precondition is introduced by the keyword "<code>require</code>". The text "<code>valid_argument_for_second</code>" is the label for the assertion clause. The boolean expression "<code>0 <= s and s <= 59</code>" says that a good value for <code>s</code> will be between 0 and 59 inclusive. 
 
 Remember that the precondition specifies those things that must be true if <code>set_second</code> has a chance of working correctly. As such, upon execution, the body of this routine will never be executed if an attempt is made to call it in a state that does not meet its precondition. Instead, the caller will incur a precondition violation exception. We will investigate more about what exceptions mean further in [[Exception Mechanism|Exception Mechanism]] . 
 
 So, what about a postcondition? We noted earlier that a postcondition should make a statement of what will be true in the case that the routine does its work correctly. For <code>set_second</code> this means that after it finishes, the query <code>second</code> should have the same value as the argument that was received from the caller. Below is the feature with the postcondition added. 
 <code>
-	set_second (s: INTEGER) is
+    set_second (s: INTEGER)
-			-- Set the second from `s'
+            -- Set the second from `s'.
         require
             valid_argument_for_second: 0 <= s and s <= 59
         do
@@ -96,7 +96,7 @@ So, what about a postcondition? We noted earlier that a postcondition should mak
         end
 </code>
 
-The postcondition is introduced by the keyword " <code> ensure </code>". Here the expression " <code> second </code> = <code> s </code>" makes certain that the routine did actually do the necessary work to ensure that the value of <code> second </code> matches the value of the argument received. 
+The postcondition is introduced by the keyword "<code>ensure</code>". Here the expression "<code>second = s</code>" makes certain that the routine did actually do the necessary work to ensure that the value of <code>second</code> matches the value of the argument received. 
 
 As you look at the postcondition, you may be tempted to think that the one-line body of the routine is so simple as to make the postconditon unnecessary. To answer this concern we need to look again for a moment at software specification.
 
@@ -104,8 +104,8 @@ As you look at the postcondition, you may be tempted to think that the one-line
 
 If we remove the instructions from a routine and leave its signature, header comment and assertions, we have a specification for the routine.
 <code>
-	set_second (s: INTEGER) is
+    set_second (s: INTEGER)
-			-- Set the second from `s'
+            -- Set the second from `s'.
         require
             valid_argument_for_second: 0 <= s and s <= 59
         ensure
@@ -152,7 +152,6 @@ The class invariant is an assertion like precondition and postcondition, but the
 How would we code the class invariant for <code>TIME_OF_DAY</code>? An instance would be valid if its hour were between 0 and 23 inclusive, minute were between 0 and 59 inclusive, and its second were between 0 and 59 inclusive. We can code the invariant as shown below. 
 <code>
 invariant
-
     hour_valid: 0 <= hour and hour <= 23
     minute_valid: 0 <= minute and minute <= 59
     second_valid: 0 <= second and second <= 59
@@ -202,7 +201,7 @@ From our example above you may have gotten the idea that contracts are really us
 <code>
 feature -- Element change
 
-	replace (v: G) is
+    replace (v: G)
             -- Replace current item by `v'.
         require
             writable: writable
@@ -230,7 +229,7 @@ In the section [[Adding Class Features|Adding Class Features]] , we promised to
 
 One of these is the tendency of mature Eiffel programmers to write routines that are quite short. It should be clear by now that we wish to build a contract on each routine. The contract describes the semantics of the routine in a declarative fashion. In other words, it tells what the routine does, without giving an indication of how it does it.
 
-Try to imagine giving a declarative description of a routine that was 50 lines long. Hardly possible. So decomposition of complex computations into chunks small enough to describe with assertions is what gets done.
+Try to imagine giving a declarative description of a routine that was 50 lines long. This could get ugly. So experienced Eiffel developers decompose complex computations into chunks small enough to be described through a clear, concise set of assertions.
 
 ===Command/Query Separation===
 
@@ -254,8 +253,8 @@ One is that, as you can probably imagine, it is not a good thing to cause an exc
 
 The way to avoid this is to use the non-strict booleans "<code>and then</code>" and "<code>or else</code>". These forms of "<code>and</code>" and "<code>or</code>" do not force the checking of all conditions. As soon as a determination can be made, they stop checking. It is typical to see "<code>and then</code>" used to avoid applying a feature to a void reference in preconditons. Below is a creation procedure that uses a non-strict boolean in its precondition. 
 <code>
-	make (a_nm: STRING; a_offset: INTEGER) is
+    make (a_nm: STRING; a_offset: INTEGER)
-			-- Initalize with name `a_nm' and utcoffset `a_offset'
+            -- Initalize with name `a_nm' and utcoffset `a_offset'.
         require
             name_not_empty: a_nm /= Void and then not a_nm.is_empty
             offset_valid: a_offset >= -12 and a_offset <= 12
@@ -270,13 +269,13 @@ The way to avoid this is to use the non-strict booleans " <code> and then </code
 
 ===Replacing Inherited Feature Assertions===
 
-To replace a precondition on a feature you are effecting or redefining, you use the " <code> require </code> <code> else </code>" keywords to introduce new conditions. These conditions will be logically " <code> or </code>-ed" with the original precondition to form an new one. 
+To replace a precondition on a feature you are effecting or redefining, you use the "<code>require else</code>" keywords to introduce new conditions. These conditions will be logically "<code>or</code>-ed" with the original precondition to form an new one. 
 
-Likewise use "<code>and </code> <code> then </code>" to add conditions to a postcondition. The added conditions will be " <code> and </code>-ed" to the original. 
+Likewise use "<code>and then</code>" to add conditions to a postcondition. The added conditions will be "<code>and</code>-ed" to the original. 
 
 Below is an example of weakening a precondition. The first feature shown is from class <code>DYNAMIC_CHAIN</code> in the Base Library. 
 <code>
-	remove_left is
+    remove_left
             -- Remove item to the left of cursor position.
             -- Do not move cursor.
         require
@@ -288,9 +287,9 @@ Below is an example of weakening a precondition. The first feature shown is from
         end
 </code>
 
-The next feature is from <code> DYNAMIC_LIST </code>, a proper descendant of <code> DYNAMIC_CHAIN </code>. <code> DYNAMIC_LIST </code> weakens the precondition it inherited from <code> DYNAMIC_CHAIN </code>. Originally in <code> DYNAMIC_CHAIN </code>, " <code> index </code> > 1" was required for <code> remove_left </code>. In <code> DYNAMIC_LIST </code> either " <code> index </code> > 1" or " <code> not </code> <code> before </code>" (or both) will suffice. 
+The next feature is from <code>DYNAMIC_LIST</code>, a proper descendant of <code>DYNAMIC_CHAIN</code>. <code>DYNAMIC_LIST</code> weakens the precondition it inherited from <code>DYNAMIC_CHAIN</code>. Originally in <code>DYNAMIC_CHAIN</code>, "<code>index > 1</code>" was required for <code>remove_left</code>. In <code>DYNAMIC_LIST</code> either "<code>index > 1</code>" or "<code>not before</code>" (or both) will suffice. 
 <code>
-	remove_left is
+    remove_left
             -- Remove item to the left of cursor position.
             -- Do not move cursor.
         require else
@@ -305,7 +304,7 @@ Let's close this discussion of Design by Contract with one more interesting and
 
 The contract exists, even though you do not code it explicitly. If it were written out, it would look as follows.
 <code>
-	my_routine is
+    my_routine
             -- My descriptive header comment
         require
             True

documentation/current/platform-specifics/microsoft-windows/net/eiffel-net-language/eiffel-net/genericity.wiki

@@ -22,9 +22,7 @@ feature   -- Access
 
     item: ANY
             -- The thing currently pointed to by cursor
-
             ...
-
 feature   -- Element change
 
     put (new_item: ANY)