mirrors/eiffel-org
1
0
Fork 0
mirror of https://github.com/EiffelSoftware/eiffel-org.git synced 2025-12-06 23:02:28 +01:00
Code Issues Packages Projects Releases Wiki Activity

Author:halw

Browse Source 
Date:2009-03-27T20:47:18.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@211 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
halw
2009-03-27 20:47:18 +00:00
parent 5d5de7df3d
commit 051ba553db
6 changed files with 49 additions and 39 deletions
Download Patch File Download Diff File Expand all files Collapse all files

BIN
documentation/current/method/_images/VGCC_error.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 22 KiB

3
documentation/current/method/_images/VGCC_error.png.data Normal file
View File

@@ -0,0 +1,3 @@
title=VGCC error
author=halw
path=content/vgcc-error

12
documentation/current/method/eiffel-tutorial-et/et-agents.wiki
View File

@@ -28,7 +28,7 @@ where <code>r</code> is the name of a routine of the enclosing class. This is an
your_icon.click_actions.extend (agent your_routine)
</code>
This adds to the end of <code>my_icon.click_actions</code> -- the list of agents associated with the "click" event for <code>my_icon</code>, denoting an icon in the application's user interface -- an agent representing <code>your_routine</code>. Then when a user clicks on the associated icon at execution, the EiffelVision 2 mechanisms will call the procedure <code>call</code> on every agent of the list, which for this agent will execute <code>your_routine</code>. This is a simple way to associate elements of your application, more precisely its "business model" (the processing that you have defined, directly connected to the application's business domain), with elements of its GUI.
This adds to the end of <code>your_icon.click_actions</code> -- the list of agents associated with the "click" event for <code>your_icon</code>, denoting an icon in the application's user interface -- an agent representing <code>your_routine</code>. Then when a user clicks on the associated icon at execution, the EiffelVision 2 mechanisms will call the procedure <code>call</code> on every agent of the list, which for this agent will execute <code>your_routine</code>. This is a simple way to associate elements of your application, more precisely its "business model" (the processing that you have defined, directly connected to the application's business domain), with elements of its GUI.
Similarly although in a completely different area, you may request the integration of a function <code>your_function</code> over the interval <code>0..1</code> through a call such as
<code>
@@ -50,7 +50,7 @@ An agent <code>agent</code> <code>r</code> built from a procedure <code>r</code>
Among the features of <code>ROUTINE</code> and its descendants the most important are <code>call</code>, already noted, which calls the associated routine, and <code>item</code>, appearing only in <code>FUNCTION</code> and yielding the result of the associated function, which it obtains by calling <code>call</code>.
As an example of using these mechanisms, here is how the function <code>integral</code> could look like in our <code>INTEGRATOR</code> example class. The details of the integration algorithm (straight forward, and making no claims to numerical sophistication) do not matter, but you see, in the highlighted line, the place were we evaluate the mathematical function associated with <code>f</code>, by calling <code>item</code> on <code>f</code>:
As an example of using these mechanisms, here is how the function <code>integral</code> could look like in our <code>INTEGRATOR</code> example class. The details of the integration algorithm (straight forward, and making no claims to numerical sophistication) do not matter, but you see the place were we evaluate the mathematical function associated with <code>f</code>, by calling <code>item</code> on <code>f</code>:
<code>
integral (f: FUNCTION [ANY, TUPLE [REAL], REAL]; low, high: REAL): REAL
-- Integral of `f' over the interval [`low', `high']
@@ -69,7 +69,7 @@ As an example of using these mechanisms, here is how the function <code>integral
until
x > high
loop
Result := Result + step * f.item ([x])
Result := Result + step * f.item ([x]) -- Here item is applied to f
x := x + step
end
end
@@ -80,7 +80,7 @@ Function <code>integral</code> takes three arguments: the agent <code>f</code> r
Result := Result + step * f.item ([x])
</code>
we don't directly pass <code>x</code> to <code>item</code>; instead, we pass a one-element tuple <code>[x]</code>, using the syntax for manifest tuples introduced in [[10 Other Mechanisms#Tuple_types|"Tuple types"]] . You will always use tuples for the argument to <code>call</code> and <code>item</code>, because these features must be applicable to any routine, and so cannot rely on a fixed number of arguments. Instead they take a single tuple intended to contain all the arguments. This property is reflected in the type of the second actual generic parameter to <code>f</code>, corresponding to <code>ARGS</code> (the formal generic parameter of <code>FUNCTION</code>): here it's <code>TUPLE [REAL]</code> to require an argument such as <code>[ x]</code>, where <code>x</code> is of type <code>REAL</code>.
we don't directly pass <code>x</code> to <code>item</code>; instead, we pass a one-element tuple <code>[x]</code>, using the syntax for manifest tuples introduced in [[10 Other Mechanisms#Tuple_types|"Tuple types"]] . You will always use tuples for the argument to <code>call</code> and <code>item</code>, because these features must be applicable to any routine, and so cannot rely on a fixed number of arguments. Instead they take a single tuple intended to contain all the arguments. This property is reflected in the type of the second actual generic parameter to <code>f</code>, corresponding to <code>ARGS</code> (the formal generic parameter of <code>FUNCTION</code>): here it's <code>TUPLE [REAL]</code> to require an argument such as <code>[x]</code>, where <code>x</code> is of type <code>REAL</code>.
Similarly, consider the agent that the call seen above:
<code>
@@ -179,7 +179,7 @@ even though the two procedures used in the agents have quite different forms. We
end
</code>
so that it doesn't take an argument: it is normally called on its target, as in <code>my_account.deposit_one_grand</code>. In contrast, the other routine has an argument:
so that it doesn't take an argument: it is normally called on its target, as in <code>your_account.deposit_one_grand</code>. In contrast, the other routine has an argument:
<code>
add_to_n (x: INTEGER)
-- Add `x' to the value of `total'.
@@ -196,5 +196,7 @@ where <code>total</code> is an integer attribute of the enclosing class. Without
Agents provide a welcome complement to the other mechanisms of Eiffel. They do not conflict with them but, when appropriate -- as in the examples sketched in this section -- provide clear and expressive programming schemes, superior to the alternatives.
{{SeeAlso|[[Event Programming with Agents]] }}

16
documentation/current/method/eiffel-tutorial-et/et-dynamic-structure-execution-model.wiki
View File

@@ -277,7 +277,7 @@ meaning that, at the time of each call, the value of each formal will be set to
In the routine body, it is not permitted to change the value of a formal argument, although it is possible to change the value of an attached object through a procedure call such as <code>formal_1.some_procedure ( ... )</code> .
==Infix and prefix notation==
==Infix and prefix notations==
Basic types such as <code>INTEGER</code> are, as noted, full-status citizens of Eiffel's type system, and so are declared as classes (part of the Kernel Library). <code>INTEGER</code>, for example, is characterized by the features describing integer operations: plus, minus, times, division, less than, and so on.
@@ -288,22 +288,22 @@ With the dot notation seen so far, this would imply that simple arithmetic opera
instead of the usual
<code>
i + j
</code>
This would be awkward. Infix and prefix features solve the problem, reconciling the object-oriented view of computation with common notational practices of mathematics. The addition function is declared in class <code>INTEGER</code> as
This would be awkward. Infix and prefix notations solve the problem, reconciling the object-oriented view of computation with common notational practices of mathematics. The addition function is declared in class <code>INTEGER</code> as
<code>
infix "+" (other: INTEGER): INTEGER
plus alias "+" (other: INTEGER): INTEGER
do
...
end
</code>
Such a feature has all the properties and prerogatives of a normal "identifier" feature, except for the form of the calls, which is infix, as in <code>i + j</code> , rather than using dot notation. An infix feature must be a function, and take exactly one argument. Similarly, a function can be declared as <code>prefix "-" </code>, with no argument, permitting calls of the form <code>-3</code> rather than <code>(3).negated</code> .
Such a feature has all the properties and prerogatives of both normal "identifier-dot" notation and infix notation. This allowing invoking <code>plus</code> using either notation: <code>i.plus (j)</code> or <code>i + j</code> . A feature such as <code>plus</code> allowing infix notation must be a function, and take exactly one argument.
Prefix notation is allowed as well. A function can be declared as <code>opposite alias "-" </code>, with no argument, permitting calls of the form <code>-3</code> rather than <code>(3).opposite</code> .
Predefined library classes covering basic types such as <code>INTEGER</code>, <code>CHARACTER</code>, <code>BOOLEAN</code>, <code>REAL</code>, <code>DOUBLE</code> are known to the Eiffel compiler, so that a call of the form <code>j + i</code>, although conceptually equivalent to a routine call, can be processed just as efficiently as the corresponding arithmetic expression in an ordinary programming language. This brings the best of both worlds: conceptual simplicity, enabling Eiffel developers, when they want to, to think of integers and the like as objects; and efficiency as good as in lower-level approaches.
Infix and prefix features are available to any class, not just the basic types' predefined classes. For example a graphics class could use the name <code>infix "|-|"</code> for a function computing the distance between two points, to be used in expressions such as
Infix and prefix notations are available to any class, not just the basic types' predefined classes. For example a graphics class could use the name <code>distance alias "|-|"</code> for a function computing the distance between two points, to be used in expressions such as
<code>
point1 |-| point2
</code>
@@ -354,7 +354,7 @@ expanded class
feature -- Basic operations
infix "+" (other: INTEGER): INTEGER
plus alias "+" (other: INTEGER): INTEGER
do
...
end

17
documentation/current/method/eiffel-tutorial-et/et-inheritance.wiki
View File

@@ -467,7 +467,12 @@ 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''.
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:
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>, the following are true:
<code lang='text'>
1) p implies (p or q)
2) (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. }}
@@ -521,7 +526,7 @@ More generally, it is permitted to have any number of deferred features and at m
All this is not a violation of the Final Name rule (defined in [[9 Inheritance#Multiple_inheritance_and_renaming|"Multiple inheritance and renaming"]] ), since the name clashes prohibited by the rule involve two different features having the same final name; here the result is just one feature, resulting from the join of all the inherited versions.
Sometimes we may want to join ''effective'' features inherited from different parents, assuming again the features have compatible signatures. One way is to redefine them all into a new version; then they again become one feature, with no name clash in the sense of the Final Name rule. But in other cases we may simply want one of the inherited implementations to take over the others. The solution is to revert to the preceding case by '''uneffecting''' the other features; uneffecting an inherited effective feature makes it deferred (this is the reverse of effecting, which turns an inherited deferred feature into an effective one). The syntax uses the <code>undefine</code> subclause:
Sometimes we may want to join ''effective'' features inherited from different parents, assuming again the features have compatible signatures. One way is to redefine them all into a new version. That is, list each in a <code>redefine</code> clause, then write a redefined version of the feature. In this case, they again become one feature, with no name clash in the sense of the Final Name rule. But in other cases we may simply want one of the inherited implementations to take over the others. The solution is to revert to the preceding case by '''uneffecting''' the other features; uneffecting an inherited effective feature makes it deferred (this is the reverse of effecting, which turns an inherited deferred feature into an effective one). The syntax uses the <code>undefine</code> subclause:
<code>
class D
@@ -595,7 +600,7 @@ Thanks to inheritance, a concise class text may achieve a lot, relying on all th
This is part of the power of the object-oriented form of reuse, but can create a comprehension and documentation problem when the inheritance structures become deep: how does one understand such a class, either as client author or as maintainer? For clients, the Contract Form, entirely deduced from the class text, does not tell the full story about available features; and maintainers must look to proper ancestors for much of the relevant information.
These observations suggest ways to produce, from a class text, a version that is equivalent feature-wise and assertion-wise, but has no inheritance dependency. This is called the '''Flat Form''' of the class. It is a class text that has no inheritance clause and includes all the features of the class, immediate (declared in the class itself) as well as inherited. For the inherited features, the flat form must of course take account of all the feature adaptation mechanisms: renaming (each feature must appear under its final name), redefinition, effecting, uneffecting and export status change. For redeclared features, <code>else require</code> clauses are or-ed with the precursors' preconditions, and <code>then ensure</code> clauses are and-ed with precursors' postconditions. For invariants, all the ancestors' clauses are concatenated. As a result, the flat form yields a view of the class, its features and its assertions that conforms exactly to the view offered to clients and (except for polymorphic uses) heirs.
These observations suggest ways to produce, from a class text, a version that is equivalent feature-wise and assertion-wise, but has no inheritance dependency. This is called the '''Flat Form''' of the class. It is a class text that has no inheritance clause and includes all the features of the class, immediate (declared in the class itself) as well as inherited. For the inherited features, the flat form must of course take account of all the feature adaptation mechanisms: renaming (each feature must appear under its final name), redefinition, effecting, uneffecting and export status change. For redeclared features, <code>require else</code> clauses are or-ed with the precursors' preconditions, and <code>ensure then</code> clauses are and-ed with precursors' postconditions. For invariants, all the ancestors' clauses are concatenated. As a result, the flat form yields a view of the class, its features and its assertions that conforms exactly to the view offered to clients and (except for polymorphic uses) heirs.
As with the Contract Form ( [[8 Design by Contract (tm), Assertions and Exceptions#The_contract_form_of_a_class|"The contract form of a class"]] ), producing the Flat Form is the responsibility of tools in the development environment. In EiffelStudio, you will just click the "Flat" icon.
@@ -623,7 +628,7 @@ The Eiffel rule enables, once again, the software developer to craft the resulti
So to tune the repeated descendant, feature by feature, for sharing and replication it suffices to use renaming.
Doing nothing will cause sharing, which is indeedthe desired policy in most cases (especially those cases of unintended repeated inheritance: making <code>D</code> inherit from <code>A</code> even though it also inherits from <code>B</code>, which you forgot is already a descendant of <code>A</code>).
Doing nothing will cause sharing, which is indeed the desired policy in most cases (especially those cases of unintended repeated inheritance: making <code>D</code> inherit from <code>A</code> even though it also inherits from <code>B</code>, which you forgot is already a descendant of <code>A</code>).
If you use renaming somewhere along the way, so that the final names are different, you will obtain two separate features. It does not matter where the renaming occurs; all that counts is whether in the common descendant, <code>TEACHING_ASSISTANT</code> in the last figure, the names are the same or different. So you can use renaming at that last stage to cause replication; but if the features have been renamed higher you can also use last-minute renaming to avoid replication, by bringing them back to a single name.
@@ -684,7 +689,7 @@ class SORTABLE_ARRAY [G -> COMPARABLE]
</code>
making it '''constrained generic'''. The symbol <code>-></code> recalls the arrow of inheritance diagrams; what follows it is a type, known as the generic constraint. Such a declaration means that:
Within the class, you may apply the features of the generic constraint -- here the features of <code>COMPARABLE</code>: <code>infix "<"</code>, <code>infix "<"</code> etc. -- to expressions of type <code>G</code>.
Within the class, you may apply the features of the generic constraint -- here the features of <code>COMPARABLE</code>: <code>infix "<"</code>, <code>infix ">"</code> etc. -- to expressions of type <code>G</code>.
A generic derivation is only valid if the chosen actual generic parameter conforms to the constraint. Here you can use <code>SORTABLE_ARRAY [INTEGER]</code> since <code>INTEGER</code> inherits from <code>COMPARABLE</code>, but not <code>SORTABLE_ARRAY [COMPLEX]</code> if <code>COMPLEX</code> is not a descendant of <code>COMPARABLE</code>.
@@ -746,7 +751,7 @@ Assignment attempt is useful in the cases cited -- access to external objects be
==Covariance and anchored declarations==
The final property of Eiffel inheritance involves the rules for adapting not only the implementation of inherited features (through redeclaration of either kind, redeclaration and redefinition, as seen so far) and their contracts (through the Assertion Redeclaration rule), but also their types. More general than type is the notion of a feature's '''signature''', defined by the number of its arguments, their types, the indication of whether it has a result (that is to say, is a function or attribute rather than a procedure) and, if so, the type of the result.
The final property of Eiffel inheritance involves the rules for adapting not only the implementation of inherited features (through redeclaration of either kind, effecting and redefinition, as seen so far) and their contracts (through the Assertion Redeclaration rule), but also their types. More general than type is the notion of a feature's '''signature''', defined by the number of its arguments, their types, the indication of whether it has a result (that is to say, is a function or attribute rather than a procedure) and, if so, the type of the result.
In many cases the signature of a redeclared feature remains the same as the original's. But in some cases you may want to adapt it to the new class. Assume for example that class <code>ACCOUNT</code> has features
<code>

40
documentation/current/method/eiffel-tutorial-et/et-other-mechanisms.wiki
View File

@@ -10,7 +10,7 @@ The Eiffel's method obsession with extendibility, reusability and maintainabilit
Eiffel addresses this need through an original mechanism that also takes care of another important issue, poorly addressed by many design and programming approaches: initialization. The idea is simple: if instead of <code>do</code> the implementation of an effective routine starts with the keyword <code>once</code>, it will only be executed the first time the routine is called during a system execution (or, in a multi-threaded environment, the first time in each thread), regardless of what the caller was. Subsequent calls from the same caller or others will have no effect; if the routine is a function, it will always return the result computed by the first call -- object if an expanded type, reference otherwise.
In the case of procedures, this provides a convenient initialization mechanism. A delicate problem in the absence of a <code>once</code> mechanism is how to provide the users of a library with a set of routines which they can call in any order, but which all need, to function properly, the guarantee that some context had been properly set up. Asking the library clients to precede the first call with a call to an initialization procedure <code>setup</code> is not only user-unfriendly but silly: in a well-engineered system we will want to check proper set-up in every of the routines, and report an error if necessary; but then if we were able to detect improper set-up we might as well shut up and set up ourselves (by calling <code>setup</code>). This is not easy, however, since the object on which we call <code>setup</code> must itself be properly initialized, so we are only pushing the problem further. Making <code>setup</code> a <code>once</code> procedure solves it: we can simply include a call
In the case of procedures, this provides a convenient initialization mechanism. A delicate problem in the absence of a <code>once</code> mechanism is how to provide the users of a library with a set of routines which they can call in any order, but which all need, to function properly, the guarantee that some context had been properly set up. Asking the library clients to precede the first call with a call to an initialization procedure <code>setup</code> is not only user-unfriendly but silly: in a well-engineered system we will want to check proper set-up in every one of the routines, and report an error if necessary; but then if we were able to detect improper set-up we might as well shut up and set up ourselves (by calling <code>setup</code>). This is not easy, however, since the object on which we call <code>setup</code> must itself be properly initialized, so we are only pushing the problem further. Making <code>setup</code> a <code>once</code> procedure solves it: we can simply include a call
<code>
setup
</code>
@@ -71,48 +71,48 @@ A conditional instruction has the form
...
end
</code>
The <code>elseif</code> ... <code>then</code> ... part (of which there may be more than one) and the <code>else</code> ... part are optional. After <code>if</code> and <code>elseif</code> comes a boolean expression; after <code>then</code>, <code>elseif</code> and <code>else</code> come zero or more instructions.
The <code>elseif</code> ... <code>then</code> ... part (of which there may be more than one) and the <code>else</code> ... part are optional. After <code>if</code> and <code>elseif</code> comes a boolean expression; after <code>then</code> and <code>else</code> come zero or more instructions.
A multi-branch instruction has the form
<code>
inspect
''exp''
when ''v1'' then
''inst1''
when ''v2'' then
''inst2''
exp
when v1 then
inst
when v2 then
inst2
...
else
''inst0''
inst0
end
</code>
where the <code>else ''inst0''</code> part is optional, <code>exp</code> is a character or integer expression, ''v1'', ''v1'', ... are constant values of the same type as <code>exp</code>, all different, and ''inst0'', ''inst1'', ''inst2'', ... are sequences of zero or more instructions.
where the <code>else inst0</code> part is optional, <code>exp</code> is a character or integer expression, <code>v1</code>, <code>v1</code>, ... are constant values of the same type as <code>exp</code>, all different, and <code>inst0</code>, <code>inst1</code>, <code>inst2</code>, ... are sequences of zero or more instructions.
The effect of such a multi-branch instruction, if the value of <code>exp</code> is one of the ''vi'', is to execute the corresponding ''insti''. If none of the ''vi'' matches, the instruction executes ''inst0'', unless there is no <code>else</code> part, in which case it triggers an exception.
The effect of such a multi-branch instruction, if the value of <code>exp</code> is one of the <code>vi</code>, is to execute the corresponding <code>insti</code>. If none of the <code>vi</code> matches, the instruction executes <code>inst0</code>, unless there is no <code>else</code> part, in which case it triggers an exception.
{{note|Raising an exception is the proper behavior, since the absence of an <code>else</code> indicates that the author asserts that one of the values will match. If you want an instruction that does nothing in this case, rather than cause an exception, use an <code>else</code> part with an empty ''inst0''. In contrast, <code>if c then</code> ''inst'' <code>end</code> with no <code>else</code> part does nothing in the absence of an <code>else</code> part, since in this case there is no implied claim that <code>c</code> must hold. }}
{{note|Raising an exception is the proper behavior, since the absence of an <code>else</code> indicates that the author asserts that one of the values will match. If you want an instruction that does nothing in this case, rather than cause an exception, use an <code>else</code> part with an empty <code>inst0</code>. In contrast, <code>if c then</code> <code>inst</code> <code>end</code> with no <code>else</code> part does nothing in the absence of an <code>else</code> part, since in this case there is no implied claim that <code>c</code> must hold. }}
The loop construct has the form
<code>
from
''initialization''
initialization
until
''exit''
exit
invariant
''inv''
inv
variant
''var''
var
loop
''body''
body
end
</code>
where the <code>invariant</code> ''inv'' and <code>variant</code> ''var'' parts are optional, the others required. ''initialization'' and ''body'' are sequences of zero or more instructions; ''exit'' and ''inv'' are boolean expressions (more precisely, ''inv'' is an assertion); ''var'' is an integer expression.
where the <code>invariant</code> <code>inv</code> and <code>variant</code> <code>var</code> parts are optional, the others required. <code>initialization</code> and <code>body</code> are sequences of zero or more instructions; <code>exit</code> and <code>inv</code> are boolean expressions (more precisely, <code>inv</code> is an assertion); <code>var</code> is an integer expression.
The effect is to execute ''initialization'', then, zero or more times until ''exit'' is satisfied, to execute ''body''. (If after ''initialization'' the value of ''exit'' is already true, ''body'' will not be executed at all.) Note that the syntax of loops always includes an initialization, as most loops require some preparation. If not, just leave ''initialization''> empty, while including the <code>from</code> since it is a required component.
The effect is to execute <code>initialization</code>, then, zero or more times until <code>exit</code> is satisfied, to execute <code>body</code>. (If after <code>initialization</code> the value of <code>exit</code> is already true, <code>body</code> will not be executed at all.) Note that the syntax of loops always includes an initialization, as most loops require some preparation. If not, just leave <code>initialization</code> empty, while including the <code>from</code> since it is a required component.
The assertion ''inv'', if present, expresses a '''loop invariant''' (not to be confused with class invariants). For the loop to be correct, ''initialization'' must ensure ''inv'', and then every iteration of ''body'' executed when ''exit'' is false must preserve the invariant; so the effect of the loop is to yield a state in which both ''inv'' and ''exit'' are true. The loop must terminate after a finite number of iterations, of course; this can be guaranteed by using a '''loop variant''' ''var''. It must be an integer expression whose value is non-negative after execution of ''initialization'', and decreased by at least one, while remain non-negative, by any execution of ''body'' when ''exit'' is false; since a non-negative integer cannot be decreased forever, this ensures termination. The assertion monitoring mode, if turned on at the highest level, will check these properties of the invariant and variant after initialization and after each loop iteration, triggering an exception if the invariant does not hold or the variant is negative or does not decrease.
The assertion <code>inv</code>, if present, expresses a '''loop invariant''' (not to be confused with class invariants). For the loop to be correct, <code>initialization</code> must ensure <code>inv</code>, and then every iteration of <code>body</code> executed when <code>exit</code> is false must preserve the invariant; so the effect of the loop is to yield a state in which both <code>inv</code> and <code>exit</code> are true. The loop must terminate after a finite number of iterations, of course; this can be guaranteed by using a '''loop variant''' <code>var</code>. It must be an integer expression whose value is non-negative after execution of <code>initialization</code>, and decreased by at least one, while remaining non-negative, by any execution of <code>body</code> when <code>exit</code> is false; since a non-negative integer cannot be decreased forever, this ensures termination. The assertion monitoring mode, if turned on at the highest level, will check these properties of the invariant and variant after initialization and after each loop iteration, triggering an exception if the invariant does not hold or the variant is negative or does not decrease.
An occasionally useful instruction is <code>debug</code> <code>(</code>''Debug_key'', ... <code>)</code> ''instructions'' <code>end</code> where ''instructions'' is a sequence of zero or more instructions and the part in parentheses is optional, containing if present one or more strings, called debug keys. The EiffelStudio compiler lets you specify the corresponding <code>debug</code> compilation option: <code>yes</code>, <code>no</code>, or an explicit debug key. The ''instructions'' will be executed if and only if the corresponding option is on. The obvious use is for instructions that should be part of the system but executed only in some circumstances, for example to provide extra debugging information.
@@ -242,7 +242,7 @@ The study of genericity described arrays. Another common kind of container objec
TUPLE [X, Y, Z]
</code>
denoting a tuple of least three elements, such that the type of the first conforms to <code>X</code>, the second to <code>Y</code>, and the third to <code>Z</code>.
denoting a tuple of at least three elements, such that the type of the first conforms to <code>X</code>, the second to <code>Y</code>, and the third to <code>Z</code>.
You may list any number of types in brackets, including none at all: <code>TUPLE</code>, with no types in brackets, denotes tuples of arbitrary length.