Updated documentation for 22.05

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

documentation/22.05/eiffel/Language_reference/index.wiki

@@ -0,0 +1,6 @@
+[[Property:title|Language reference]]
+[[Property:link_title|Language]]
+[[Property:weight|3]]
+[[Property:uuid|17412f30-0451-4b2b-bdec-578ca2e619a6]]
+
+

documentation/22.05/eiffel/Language_reference/quick-reference-eiffel-programming-language/Expressions/Conditional-expression.wiki

@@ -0,0 +1,32 @@
+[[Property:modification_date|Wed, 11 Sep 2019 23:28:26 GMT]]
+[[Property:publication_date|Wed, 11 Sep 2019 23:28:26 GMT]]
+[[Property:uuid|C652AC71-8BAD-4387-A46C-21C9F5C3A68F]]
+[[Property:weight|0]]
+[[Property:title|Conditional expression]]
+[[Property:link_title|Conditional]]
+
+[[Eiffel_programming_language_syntax#Conditionals|Conditional expressions]] compute a value using different expressions depending on one or more conditions. If all expressions have the same type, the conditional expression as a whole has this type as well:
+
+<e>
+   if time < noon then
+      "Good morning"
+   elseif time < evening then
+      "Good afternoon"
+   else
+      "Good evening"
+   end
+</e>
+
+has type `STRING`.
+
+If the types of the expressions are different, the [[Types#Common_ancestor_types|common ancestor type]] is used as a type of the whole expression.
+
+<e>
+   if time < noon then
+      "Good morning"
+   else
+      Void
+   end
+</e>
+
+has type `detachable STRING`.

documentation/22.05/eiffel/Language_reference/quick-reference-eiffel-programming-language/Expressions/Manifest-array.wiki

@@ -0,0 +1,85 @@
+[[Property:uuid|3C1A6DEF-A6F1-4E64-A0BE-C07BDB382C93]]
+[[Property:weight|0]]
+[[Property:title|Manifest array]]
+
+A manifest array is an expression denoting an array by simply listing its elements, as in  `<<1, 4, 9, 16, 25>>`. The lower index is always `1` and the upper index is the number of items,  `5` in this example.
+
+The type of a manifest array is always `ARRAY [T]` where  `T` is a type to which all the elements conform, `INTEGER` in the previous example. In case of a possible ambiguity you can make the type explicit, as in `{ARRAY [COMPARABLE]} <<7, "Eiffel">>`, where both  `INTEGER`, the type of `7`, and  `STRING`, the type of `"Eiffel"`, conform to `COMPARABLE`. 
+
+== What are manifest arrays good for? ==
+
+Use a manifest array to initialize an element by simply listing its initial elements. For example, with the declaration
+
+```eiffel
+squares: ARRAY [INTEGER]
+```
+
+you can initialize `squares` through
+
+```eiffel
+squares := <<1, 4, 9, 16, 25>>
+```
+
+This is simpler than the alternative, which would be to create the array explicitly and give a value to every element in turn:
+```eiffel
+	-- Arguments to `make_filled` are: default value, lower bound, upper bound.
+create squares.make_filled (0, 1, 5)
+squares [1] := 1
+squares [2] := 4
+squares [3] := 9 
+squares [4] := 16
+squares [5] := 25
+```
+
+The first form, with the manifest array, is shorter, but the effect is the same.
+
+Manifest arrays are normal arrays, not restricted in any way. You can for example add elements to them, as in
+
+```eiffel
+	-- Arguments to `force` are: value, position.
+squares.force (36, 6)	
+```
+
+which will resize the array to bounds 1 and 6.
+
+== Type of a manifest array: the implicit case ==
+
+If you do not explicitly specify an array type, the type of the manifest array is as follows:
+
+* For an empty manifest array  `<<>>`:  `ARRAY [NONE]`. (In the following cases we assume the array is not empty.)
+
+* If all elements are of the same exact type  `T`: `ARRAY [T]`.
+
+* If the types of all elements all conform to a type  `T`:  `ARRAY [T]`. Note that in this case `T` is unique since two different types cannot conform to each other. (The preceding case, all types identical, is a special case of this one, since a type conforms to itself.) 
+
+* Otherwise:  `ARRAY [ANY]`.
+
+As an example of the third case (conformance of all elements to one of them), assume  `POLYGON` and  `CIRCLE` both conform to  `FIGURE`. Then the manifest array  `<<a_polygon, a_figure, a_circle>>`, with `a_polygon` of type  `POLYGON` and so on, is  `ARRAY [FIGURE]`.
+
+== Type of a manifest array: the explicit case ==
+
+With the preceding rule, the type of   `<<7, "Eiffel">>` is the most general possible one, `ARRAY [ANY]`, since  `INTEGER` and  `STRING` do not conform to each other (either way). If you are not happy with this default type, you can make the array type explicit by writing it in braces:
+
+```eiffel
+{ARRAY [COMPARABLE]} <<7, "Eiffel">>
+```
+
+The rule in such a case is that in `{ARRAY [T]} <<element1, element2, ...>>` the types of all elements must conform to  `T`.
+
+As another example, with
+
+```eiffel
+figures: ARRAY [FIGURE]
+```
+
+you cannot assign  `<<a_polygon, a_circle>>` to `figures` since the type of the manifest array is `ARRAY [ANY]`. To make this assignment possible, use an explicit type:
+
+```eiffel
+figures := {ARRAY [FIGURE]} <<a_polygon, a_circle>>
+```
+
+You can also use this form to give an explicit type to an empty array, which would otherwise be of type `ARRAY [NONE]`. For example, with `figures` declared as above:
+
+```eiffel
+figures := {ARRAY [FIGURE]} <<>>
+```

documentation/22.05/eiffel/Language_reference/quick-reference-eiffel-programming-language/Expressions/index.wiki

@@ -0,0 +1,5 @@
+[[Property:uuid|F904B70B-4C34-459B-A146-E10C7EC30136]]
+[[Property:weight|0]]
+[[Property:title|Expressions]]
+
+[[Eiffel%20programming%20language%20syntax#Expressions|Expressions]] are used to compute a value at run-time and have an associated type at compile-time.

documentation/22.05/eiffel/Language_reference/quick-reference-eiffel-programming-language/Types.wiki

@@ -0,0 +1,44 @@
+[[Property:uuid|88764AFC-7DC5-4547-8B8C-4C0A489B0620]]
+[[Property:weight|0]]
+[[Property:title|Types]]
+
+== Common ancestor type ==
+
+A '''common ancestor type''' is a type computed for a list of types using the following algorithm:
+
+# Add `NONE` to the list of types (to make sure the list is never empty).
+# If there is a separate type in the list, add a mark `separate` in front of all non-separate types in the list.
+# If there is a detachable type in the list, add a mark `detachable` in front of all attached types in the list.
+# If there is a type in the list to which all other types conform, it is the common ancestor type.
+# Otherwise, add `ANY` to the list and repeat steps starting from step #2.
+
+
+Here are some examples:
+{|
+! Type list
+! Common ancestor type
+|-
+| (empty)
+| <e>NONE</e>
+|-
+| <e>BOOLEAN</e>
+| <e>BOOLEAN</e>
+|-
+| <e>BOOLEAN, BOOLEAN</e>
+| <e>BOOLEAN</e>
+|-
+| <e>INTEGER_32, REAL_64, COMPARABLE</e>
+| <e>COMPARABLE</e>
+|-
+| <e>INTEGER_32, REAL_64</e>
+| <e>ANY</e>
+|-
+| <e>INTEGER_32, detachable COMPARABLE</e>
+| <e>detachable COMPARABLE</e>
+|-
+| <e>INTEGER_32, separate COMPARABLE</e>
+| <e>separate COMPARABLE</e>
+|-
+| <e>detachable STRING, separate COMPARABLE</e>
+| <e>detachable separate COMPARABLE</e>
+|}

documentation/22.05/eiffel/Language_reference/quick-reference-eiffel-programming-language/eiffel-programming-language-reserved-words.wiki

@@ -0,0 +1,525 @@
+[[Property:modification_date|Thu, 13 Aug 2020 00:59:54 GMT]]
+[[Property:publication_date|Wed, 11 Sep 2019 14:10:27 GMT]]
+[[Property:title|Eiffel programming language reserved words]]
+[[Property:link_title|Reserved words]]
+[[Property:weight|1]]
+[[Property:uuid|047ce062-45de-f25c-f356-ee8ec0fc2d1d]]
+In the Eiffel programming language, there are certain words that are considered "reserved". These words have specific meanings recognized by the compiler. As such, it is invalid to attempt to use a reserved word as an ordinary language identifier.
+
+The reserved words listed in the ISO/ECMA standard are shown below with a brief explanation of their meanings. Links are given where appropriate to the syntax definitions and to descriptions in the online documentation. Occasionally, references to the June 2006 standard document are used and are recognizable as clause numbers in parentheses, i.e., three integers separated by dots, for example: (8.14.1)
+
+
+{{info|The list below includes all the Eiffel reserved words. Some of these words are considered ''language keywords'' while others are not. The distinction is that language keywords are reserved words that are used only as syntactical markers, and have no inherent semantic value. Examples are the keywords <code>do</code> and <code>end</code>. Non-keyword reserved words are those that do carry semantic value, such as <code>True</code> and <code>Current</code>.}}
+
+
+{{note|The set of reserved words supported by the Eiffel Software implementation may vary somewhat from those specified in the current standard. See the [[Differences between standard ECMA-367 and Eiffel Software implementation|"differences" chapter of the online documentation]] for information on these variances.}}
+ 
+
+==Reserved words==
+
+===across===
+
+Introduces an [[ET: Instructions#Loop|iteration]].
+
+===agent===
+
+Used to specify an [[ET: Agents|agent]]. 
+
+:[[Eiffel programming language syntax#Agents|Syntax.]]
+
+
+===alias===
+
+Used to identify an alternative or alias feature name. 
+
+:[[Eiffel programming language syntax#Feature names|Syntax.]]
+
+[[ET: The Dynamic Structure: Execution Model#Infix and prefix notations|Usage for infix/prefix notations.]]
+
+[[ET: The Static Picture: System Organization#External software|Usage in interfaces to external software.]]
+
+:[[Eiffel programming language syntax#External routines|Syntax.]]
+
+
+===all===
+
+Used in [[ET: Inheritance#Changing the export status|export adaptation]] to indicate that a chosen export status applies to all features inherited from a given parent.
+
+:[[Eiffel programming language syntax#Export adaptation|Syntax.]]
+
+
+===and===
+
+The logical conjunction [[Eiffel programming language syntax#Operators|operator]]. Strict when used alone, nonstrict when used with [[#then|then]].
+
+
+===as===
+
+Used when [[ET: Inheritance#Multiple inheritance and renaming|renaming]] features in descendant classes.
+
+:[[Eiffel programming language syntax#Rename clauses|Syntax.]]
+
+
+===assign===
+
+Used to designate [[ET: The Dynamic Structure: Execution Model#Abstraction|assigner commands]].
+
+:[[Eiffel programming language syntax#Assigner marks|Syntax.]]
+
+
+===attribute===
+
+Introduces an attribute body, as in [[Void-safety: Background, definition, and tools#Self-initializing attributes|self-initializing attributes]].
+
+:[[Eiffel programming language syntax#Attribute bodies|Syntax.]]
+
+
+===check===
+
+Identifies a [[ET: Other Mechanisms#Check|check instruction]].
+
+:[[Eiffel programming language syntax#Check instructions|Syntax.]]
+
+
+===class===
+
+Used in a class header in the declaration of a [[ET: The Dynamic Structure: Execution Model#A simple class|class]]. 
+
+:[[Eiffel programming language syntax#Class headers|Class header syntax.]]
+
+
+===convert===
+
+Used in converter clauses.
+
+:[[Eiffel programming language syntax#Converter clauses|Syntax.]]
+
+Used in feature names for operator aliases, supporting mixed type expressions causing a conversion of the target (8.5.14).
+
+:[[Eiffel programming language syntax#Feature names|Syntax.]]
+
+
+===create===
+
+In the creators part of a class, introduces those procedures which can be used to [[ET: The Dynamic Structure: Execution Model#Creating and initializing objects|initialize instances]].
+
+:[[Eiffel programming language syntax#Creators parts|Syntax.]]
+
+Introduces a  [[ET: The Dynamic Structure: Execution Model#Creating and initializing objects|creation instruction]].
+
+:[[Eiffel programming language syntax#Creation instructions|Syntax.]]
+
+Introduces a creation expression (8.20.18)
+
+:[[Eiffel programming language syntax#Creation expressions|Syntax.]]
+
+In [[ET: Inheritance#Constrained genericity|constrained genericity]], introduces a list of names of features which can be used as creation procedures with a generic class for a particular formal generic parameter. (8.12.10)
+
+:[[Eiffel programming language syntax#Generic constraints|Syntax.]]
+
+
+===Current===
+
+A predefined entity indicating the current object. 
+
+:[[Eiffel programming language syntax#Entities and variables|Entity syntax.]]
+
+:[[Eiffel programming language syntax#Types|Anchored types syntax.]]
+
+
+===debug===
+
+Introduces a [[ET: Other Mechanisms#Debug|debug instruction]].
+
+:[[Eiffel programming language syntax#Debug Instructions|Syntax.]]
+
+
+===deferred===
+
+Used in class header to indicate a [[ET: Inheritance#Deferred features and classes|deferred class]].
+
+:[[Eiffel programming language syntax#Class headers|Syntax.]]
+
+Used in routine body to indicate a [[ET: Inheritance#Deferred features and classes|deferred feature]].
+
+:[[Eiffel programming language syntax#Routine bodies|Syntax.]]
+
+
+===do===
+
+Introduces a sequence of instructions as a routine body, as shown in the [[ET: Hello World|Hello World]] example.
+
+:[[Eiffel programming language syntax#Routine bodies|Syntax.]]
+
+
+===else===
+
+Used in [[ET-_Instructions#Conditional|conditional]] and [[ET-_Instructions#Multi-branch|multi-branch]] instructions to introduce a sequence of instructions to be executed in the case that no specified conditions are met.
+
+:[[Eiffel programming language syntax#Conditionals|Conditional syntax.]]
+
+:[[Eiffel programming language syntax#Multi-branch instructions|Multi-branch syntax.]]
+
+Used in a [[Conditional_expression|conditional expression]] to compute a value in the case that no specified conditions are met.
+
+:[[Eiffel programming language syntax#Conditionals|Conditional expression syntax.]]
+
+Used as part of the double reserved word <code>or else</code>, the semi-strict disjunction operator.
+
+:[[Eiffel programming language syntax#Operators|Syntax.]]
+
+Used after the reserved word [[#require|<code>require</code>]] as a precondition extension, allowing the weakening of an inherited precondition (8.10.3).
+
+:[[Eiffel programming language syntax#Assertions|Syntax.]]
+
+
+===elseif===
+
+Used in [[ET-_Instructions#Conditional|conditional]] instructions to effect a "multi-branch" choice instruction.
+
+:[[Eiffel programming language syntax#Conditionals|Syntax.]]
+
+Used in a [[Conditional_expression|conditional expression]] to effect a "multi-branch" choice to compute of a value.
+
+:[[Eiffel programming language syntax#Conditionals|Conditional expression syntax.]]
+
+
+===end===
+
+Serves to terminate several Eiffel programming language constructs.
+
+:Syntax for:
+::[[Eiffel programming language syntax#Class declarations|Class declarations]]
+::[[Eiffel programming language syntax#Feature bodies|Feature bodies]]
+::[[Eiffel programming language syntax#Inheritance parts|Inheritance parts]]
+::[[Eiffel programming language syntax#Check instructions|Check instructions]]
+::[[Eiffel programming language syntax#Generic constraints|Generic constraints: renaming and constraint creators]]
+::[[Eiffel programming language syntax#Conditionals|Conditional instructions]]
+::[[Eiffel programming language syntax#Multi-branch instructions|Multi-branch instructions]]
+::[[Eiffel programming language syntax#Conditionals|Conditional expressions]]
+::[[Eiffel programming language syntax#Loops|Loops]]
+::[[Eiffel programming language syntax#Debug instructions|Debug instructions]]
+
+
+===ensure===
+
+Introduces a [[ET: Design by Contract (tm), Assertions and Exceptions#Expressing assertions|postcondition]].
+
+When followed by the reserved word [[#then|<code>then</code>]] denotes a postcondition extension, allowing the strengthening of an inherited postcondition (8.10.3).
+
+:[[Eiffel programming language syntax#Assertions|Syntax.]]
+
+
+===expanded===
+
+Used in a class header to indicate that a class is [[ET: The Dynamic Structure: Execution Model#Type categories|expanded]].
+
+:[[Eiffel programming language syntax#Class headers|Syntax.]]
+
+
+===export===
+
+Used to [[ET: Inheritance#Changing the export status|change the export status]] (availability to clients) of inherited features.
+
+:[[Eiffel programming language syntax#Export adaptation|Syntax.]]
+
+
+===external===
+
+Denotes an [[ET: The Static Picture: System Organization#External software|external routine]]. External routines are commonly defined to interface with [[C externals|C external routines]] and [[C++ Externals|C++ external routines]].
+
+:[[Eiffel programming language syntax#External routines|Syntax]]
+
+
+===False===
+
+Boolean manifest constant. 
+
+:[[Eiffel programming language syntax#Manifest constants|Syntax.]]
+
+
+===feature===
+
+Introduces a [[ET: Hello World|feature clause]].
+
+:[[Eiffel programming language syntax#Feature parts|Syntax.]]
+
+
+===from===
+
+Used in [[ET: Other Mechanisms#Loop|loop]] initialization.
+
+:[[Eiffel programming language syntax#Loops|Syntax.]]
+
+
+===frozen===
+
+Used in a class header to mark a class explicitly as frozen. A frozen class prohibits it from serving as a "conforming parent" to other classes. (8.4.5).
+
+:[[Eiffel programming language syntax#Class headers|Syntax.]]
+
+Used in a feature declaration to mark a feature as frozen. A frozen feature cannot be redefined by heir classes.
+
+:[[Eiffel programming language syntax#New feature lists|Syntax.]]
+
+Used with a formal generic parameter to indicate that conformance of generic derivations of the class require identical actual generic parameters. (8.12.3)
+
+:[[Eiffel programming language syntax#Formal generic parameters|Syntax.]]
+
+
+===if===
+
+Used to introduce a [[ET-_Instructions#Conditional|conditional]].
+
+:[[Eiffel programming language syntax#Conditionals|Conditional syntax.]]
+
+Used to introduce a [[Conditional_expression|Conditional expression]].
+
+:[[Eiffel programming language syntax#Conditionals|Conditional expression syntax.]]
+
+
+===implies===
+
+The semi-strict logical implication [[Eiffel programming language syntax#Operators|operator]].
+
+
+===inherit===
+
+Used in an [[ET: Inheritance|inherit]] clause.
+
+:[[Eiffel programming language syntax#Inheritance parts|Syntax.]]
+
+
+===inspect===
+
+Introduces a [[ET-_Instructions#Multi-branch|multi-branch]] instruction.
+
+:[[Eiffel programming language syntax#Multi-branch instructions|Syntax.]]
+
+
+===invariant===
+
+Used to introduce an invariant assertion as a [[ET: Design by Contract (tm), Assertions and Exceptions#Class invariants|class invariant]] or [[ET: Instructions#Loop|loop invariant]].
+
+:[[Eiffel programming language syntax#Assertions|Assertions syntax.]]
+
+:[[Eiffel programming language syntax#Class declarations|Syntax of class declaration including class invariant.]]
+
+:[[Eiffel programming language syntax#Loops|Syntax of loop including loop invariant.]]
+
+
+===like===
+
+Used in the declaration of an [[ET: Inheritance#Covariance and anchored declarations|anchored]] entity.
+
+:[[Eiffel programming language syntax#Types|Syntax.]]
+
+
+===local===
+
+Introduces the [[ET: The Dynamic Structure: Execution Model#Entities|local variable]] declarations in a feature body.
+
+:[[Eiffel programming language syntax#Feature bodies|Feature bodies syntax.]]
+
+:[[Eiffel programming language syntax#Local variables|Local variable declarations syntax.]]
+
+
+===loop===
+
+Introduces a [[ET: Other Mechanisms#Loop|loop]] body.
+
+:[[Eiffel programming language syntax#Loops|Syntax.]]
+
+
+===not===
+
+The logical negation [[Eiffel programming language syntax#Operators|operator]].
+
+
+===note===
+
+Used to begin a Notes part, in a [[Eiffel programming language syntax#Class declarations|class declaration]], a [[Eiffel programming language syntax#Feature declarations|feature declaration]], or a [[Eiffel programming language syntax#Check instructions|check instruction]].
+
+:[[Eiffel programming language syntax#Notes|Syntax.]]
+
+
+===obsolete===
+
+Used to mark [[ET: Other Mechanisms#Obsolete features and classes|obsolete features and classes]].
+
+:[[Eiffel programming language syntax#Feature declarations|Feature declarations syntax.]]
+
+:[[Eiffel programming language syntax#Class declarations|Class declarations declarations syntax.]]
+
+:[[Eiffel programming language syntax#Obsolete marks|Obsolete mark syntax.]]
+
+
+===old===
+
+Introduces an ''old expression''. Old expressions are valid only in the  [[ET: Design by Contract (tm), Assertions and Exceptions#Postconditions|postconditions]] of routines.
+
+:[[Eiffel programming language syntax#Old postcondition expressions|Syntax.]]
+
+
+===once===
+
+Used to introduce [[ET: Other Mechanisms#Once routines and shared objects|once routines]] and once string expressions.
+
+:[[Eiffel programming language syntax#Routine bodies|Once routine syntax.]]
+
+:[[Eiffel programming language syntax#Expressions|Once string syntax.]]
+
+
+===only===
+
+Used in an ''only postcondition clause''. (8.9.11)
+
+:[[Eiffel programming language syntax#"Old" postcondition expressions|Syntax.]]
+
+
+===or===
+
+The logical disjunction [[Eiffel programming language syntax#Operators|operator]]. Strict when used alone, nonstrict when used with [[#else|else]].
+
+
+===Precursor===
+
+Allows a redefined routine to access the routine it redefines, i.e, its [[ET: Inheritance#Redefinition|precursor]].
+
+:[[Eiffel programming language syntax#Precursor|Syntax.]]
+
+
+===redefine===
+
+Used in an [[Eiffel programming language syntax#Inheritance parts|inheritance part]] of a [[Eiffel programming language syntax#Class declarations|class declaration]] to list those inherited features which, in the heir class, will receive new implementations, specifications, or both, i.e, those features being [[ET: Inheritance#Redefinition|redefined]].
+
+:[[Eiffel programming language syntax#Redefinition|Redefine syntax.]]
+
+
+===rename===
+
+Used in an [[Eiffel programming language syntax#Inheritance parts|inheritance part]] of a [[Eiffel programming language syntax#Class declarations|class declaration]] to [[ET: Inheritance#Multiple inheritance and renaming|provide alternative names]] for inherited features in an heir class.
+
+Used to rename features in a [[Eiffel programming language syntax#Generic constraints|generic constraint]]. (8.12.8).
+
+:[[Eiffel programming language syntax#Rename clauses|Syntax.]]
+
+
+===require===
+
+Introduces a [[ET: Design by Contract (tm), Assertions and Exceptions#Expressing assertions|precondition]]. 
+
+When followed by the reserved word [[#else|<code>else</code>]] denotes a precondition extension, allowing the weakening of an inherited precondition (8.10.3).
+
+:[[Eiffel programming language syntax#Assertions|Syntax.]]
+
+
+
+===rescue===
+
+Introduces a [[ET: Design by Contract (tm), Assertions and Exceptions#Exception handling|rescue clause]] in a [[Eiffel programming language syntax#Feature bodies|feature body]].
+
+:[[Eiffel programming language syntax#Rescue clauses|Syntax.]]
+
+
+===Result===
+
+A predefined [[ET: The Dynamic Structure: Execution Model#Entities|entity]] used to represent the final result of a function.
+
+:[[Eiffel programming language syntax#Entities and variables|Syntax.]]
+
+
+===retry===
+
+An [[Eiffel programming language syntax#Instructions|instruction]] valid only in [[Eiffel programming language syntax#Rescue clauses|rescue clauses]] and used to [[ET: Design by Contract (tm), Assertions and Exceptions#Exception handling|re-execute the routine]] in which it appears.
+
+:[[Eiffel programming language syntax#Rescue clauses|Syntax.]]
+
+
+===select===
+
+Used in an [[Eiffel programming language syntax#Inheritance parts|inheritance part]] of a [[Eiffel programming language syntax#Class declarations|class declaration]] to resolve possible ambiguities related to polymorphism and dynamic binding in the presence of  [[ET: Inheritance#Repeated inheritance and selection|repeated inheritance]].
+
+:[[Eiffel programming language syntax#Select clauses|Syntax.]]
+
+
+===separate===
+
+Used to support  [[Concurrent programming with SCOOP]].
+
+
+===then===
+
+Used in [[ET-_Instructions#Conditional|conditional]] and [[ET-_Instructions#Multi-branch|multi-branch]] instructions to introduce a sequence of instructions to be executed in the case that a condition is met.
+
+:[[Eiffel programming language syntax#Conditionals|Conditional syntax.]]
+
+:[[Eiffel programming language syntax#Multi-branch instructions|Multi-branch syntax.]]
+
+Used in a [[Conditional_expression|conditional expression]] to compute of a value in the case that a condition is met.
+
+:[[Eiffel programming language syntax#Conditionals|Conditional expression syntax.]]
+
+Used as part of the double reserved word <code>and then</code>, the semi-strict conjunction operator.
+
+:[[Eiffel programming language syntax#Operators|Syntax.]]
+
+Used after the reserved word [[#ensure|<code>ensure</code>]] as a postcondition extension, allowing the strengthening of an inherited postcondition (8.10.3).
+
+:[[Eiffel programming language syntax#Assertions|Syntax.]]
+
+
+===True===
+
+Boolean manifest constant. 
+
+:[[Eiffel programming language syntax#Manifest constants|Syntax.]]
+
+
+===TUPLE===
+
+Denotes a [[ET: Other Mechanisms#Tuple types|TUPLE type]].
+
+:[[Eiffel programming language syntax#Tuple types|Syntax.]]
+
+
+===undefine===
+
+Used in an [[Eiffel programming language syntax#Inheritance parts|inheritance part]] of a [[Eiffel programming language syntax#Class declarations|class declaration]] to  [[ET: Inheritance#Joining and uneffecting|uneffect]] an inherited feature.
+
+:[[Eiffel programming language syntax#Undefine clauses|Syntax.]]
+
+
+===until===
+
+Used in [[ET: Other Mechanisms#Loop|loop]] initialization.
+
+:[[Eiffel programming language syntax#Loops|Syntax.]]
+
+
+===variant===
+
+Introduces a [[ET: Instructions#Loop|loop variant]].
+
+:[[Eiffel programming language syntax#Variants|Syntax.]]
+
+
+===Void===
+
+A predefined entity name representing a [[ET: The Dynamic Structure: Execution Model#Basic operations|void (a.k.a., null) reference]]. 
+
+
+===when===
+
+Used in a [[ET-_Instructions#Multi-branch|multi-branch instruction]] to introduce cases.
+
+:[[Eiffel programming language syntax#Multi-branch instructions|Syntax.]]
+
+
+===xor===
+
+The exclusive disjunction [[Eiffel programming language syntax#Operators|operator]].
+
+
+
+

documentation/22.05/eiffel/Language_reference/quick-reference-eiffel-programming-language/eiffel-programming-language-syntax.wiki

@@ -0,0 +1,785 @@
+[[Property:modification_date|Mon, 29 Jul 2019 16:52:51 GMT]]
+[[Property:publication_date|Mon, 29 Apr 2019 14:08:51 GMT]]
+[[Property:title|Eiffel programming language syntax]]
+[[Property:link_title|Syntax]]
+[[Property:weight|0]]
+[[Property:uuid|4CB56AD5-1586-41F6-9E81-085F47E992DC]]
+The syntax specification shown here is a less complete and less formal version of that which is in the Eiffel ISO/ECMA standard document. The format is BNF-E. The Language Specification section of the standard document includes an overview of BNF-E. 
+
+There are a few parts of the syntax that are either non-production or non-representable in BNF-E. Some of these have been omitted from the following specification. These omitted parts of the syntax definition add to the precision of the specification, but knowledge of them is not always vital for developers. 
+
+In the BNF-E representation, generally non-terminals which are defined in the same group of productions in which they are used are not linked. However when a non-terminal is defined outside a group in which it is used, it is linked to the group in which it is defined.
+
+__TOC__
+
+The following section contains those non-production elements of the specification that are used later in the BNF-E specification.
+
+==Eiffel non-production elements==
+
+===Identifiers===
+
+An '''identifier''' is a sequence of one or more alphanumeric [[#Characters|characters]] of which the first is a letter. 
+
+The definition is augmented by the rule that Identifiers are not valid if they are the same as one of the language's reserved words.
+
+===Characters===
+
+Characters are either:
+
+* All 32-bit, corresponding to Unicode and to the Eiffel type CHARACTER_32.
+* All 8-bit, corresponding to 8-bit extended ASCII and to the Eiffel type CHARACTER_8
+
+===Reals===
+
+A real -- specimen of Real -- is made of the following elements, in the order given:
+
+* An optional decimal [[#Integers|Integer]], giving the integral part.
+* A required "." (dot).
+* An optional decimal [[#Integers|Integer]], giving the fractional part.
+* An optional exponent, which is the letter ''e'' or ''E'' followed by an optional [[#Manifest constants|Sign]] and a decimal [[#Integers|Integer]].
+
+No intervening character (blank or otherwise) is permitted between these elements. The integral and fractional parts may not both be absent.
+
+===Strings===
+
+A string -- specimen of construct String -- is a sequence of zero or more manifest characters.
+
+===Simple strings===
+
+A simple string -- specimen of Simple_string -- is a [[#Strings|String]] consisting of at most one line (that is to say, containing no embedded new-line manifest character), possibly containing [[#Special characters|codes for special characters]].
+
+===Special characters===
+
+{| border="2"
+|+ Special Characters and Their Codes
+|-
+! Character 
+! Code 
+! Mnemonic name
+|-
+| @ || %A || At-sign
+|-
+| BS || %B || Backspace
+|-
+| ^ || %C || Circumflex
+|-
+| $ || %D || Dollar
+|-
+| FF || %F || Form feed
+|-
+| \ || %H || Backslash
+|-
+| ~ || %L || Tilde
+|-
+| NL (LF) || %N || Newline
+|-
+| `` ` `` || %Q || Backquote
+|-
+| CR || %R || Carriage return
+|-
+| # || %S || Sharp
+|-
+| HT || %T || Horizontal tab
+|-
+| NUL || %U || Null
+|-
+| | || %V || Vertical bar
+|-
+| % || %% || Percent
+|-
+| ' || %' || Single quote
+|-
+| " || %" || Double quote
+|-
+| [ || %( || Opening bracket
+|-
+| ] || %) || Closing bracket
+|-
+| { || %< || Opening brace
+|-
+| } || %> || Closing brace
+|}
+
+* `%/123/` represents the character with decimal code `123` .
+* And only for manifest character (for now)
+** `'%/0x2200/'`  represents the character with hexadecimal code U+2200 = '∀' (note `'%/0x2200/' = '%/8704/'` )
+** `'%/0c21000/'` in octal
+** `'%/0b10001000000000/'` in binary
+
+
+===Line wrapping parts===
+
+A sequence of characters consisting of the following, in order:
+* % (percent character)
+* Zero or more blanks or tabs
+* New line (Line feed)
+* Zero or more blanks or tabs
+* % (percent character)
+
+Line wrapping parts are used as separators between one [[#Simple strings|Simple_string]] and the next in a [[#Manifest strings|Basic_manifest_string]] so that the string can be split across lines.
+
+===New line===
+
+A specimen of New_line is a New Line. 
+
+
+==Eiffel BNF-E Syntax==
+
+
+===Class names ===
+Class_name ::= [[#Identfiers|Identifier]] 
+
+===Class declarations ===
+Class_declaration ::= <nowiki>[</nowiki>[[#Notes|Notes]]<nowiki>]</nowiki> 
+[[#Class headers|Class_header]] <nowiki>[</nowiki>[[#Formal generic parameters|Formal_generics]]<nowiki>]</nowiki> 
+
+<nowiki>[</nowiki>[[#Obsolete marks|Obsolete]]<nowiki>]</nowiki> 
+
+<nowiki>[</nowiki>[[#Inheritance parts|Inheritance]]<nowiki>]</nowiki>
+
+<nowiki>[</nowiki>[[#Creators parts|Creators]]<nowiki>]</nowiki>
+
+<nowiki>[</nowiki>[[#Converter clauses|Converters]]<nowiki>]</nowiki> 
+
+<nowiki>[</nowiki>[[#Feature parts|Features]]<nowiki>]</nowiki> 
+
+<nowiki>[</nowiki>[[#Notes|Notes]]<nowiki>]</nowiki>
+
+<nowiki>[</nowiki>[[#Assertions|Invariant]]<nowiki>]</nowiki> 
+
+<nowiki>[</nowiki>[[#Notes|Notes]]<nowiki>]</nowiki>
+
+<code>end</code>
+
+===Notes ===
+Notes ::= <code>note</code> Note_list
+
+Note_list ::= {Note_entry ";" ...}* 
+
+Note_entry ::= Note_name Note_values 
+
+Note_name ::= [[#Identifiers|Identifier]] ":" 
+
+Note_values ::= {Note_item ","...}+ 
+
+Note_item ::= [[#Identifiers|Identifier]] | [[#Manifest constants|Manifest_constant]] 
+
+===Class headers ===
+Class_header ::= <nowiki>[Header_mark]</nowiki> <code>class</code> [[#Class names|Class_name]] 
+
+Header_mark ::= <code>deferred</code> | <code>expanded</code> | <code>frozen</code> 
+
+===Obsolete marks ===
+Obsolete ::= <code>obsolete</code> Message 
+
+Message ::= [[#Manifest strings|Manifest_string]] 
+
+===Feature parts ===
+Features ::= Feature_clause+ 
+
+Feature_clause ::= <code>feature</code> <nowiki>[</nowiki>[[#Clients|Clients]]<nowiki>]</nowiki> <nowiki>[</nowiki>[[#Feature parts|Header_comment]]<nowiki>]</nowiki> Feature_declaration_list 
+
+Feature_declaration_list ::= {[[#Feature declarations|Feature_declaration]] ";" ...}* 
+
+Header_comment ::= [[#Comments|Comment]] 
+
+===Feature declarations ===
+Feature_declaration ::= [[#New feature lists|New_feature_list]] Declaration_body 
+
+Declaration_body ::= <nowiki>[</nowiki>[[#Formal argument and entity declarations|Formal_arguments]]<nowiki>] [Query_mark] [Feature_value] </nowiki>
+
+Query_mark ::= Type_mark <nowiki>[</nowiki>[[#Assigner marks|Assigner_mark]]<nowiki>]</nowiki> 
+
+Type_mark ::= ":" [[#Types|Type]] 
+
+Feature_value ::= <nowiki>[Explicit_value] </nowiki>
+<nowiki>[</nowiki>[[#Obsolete parts|Obsolete]]<nowiki>]</nowiki> 
+<nowiki>[</nowiki>[[#Feature parts|Header_comment]]<nowiki>]</nowiki> 
+<nowiki>[</nowiki>[[#Feature bodies|Attribute_or_routine]]<nowiki>]</nowiki> 
+
+Explicit_value ::= "=" [[#Manifest constants|Manifest_constant]] 
+
+
+===New feature lists ===
+New_feature_list ::= {New_feature "," ...}+ 
+
+New_feature ::= <nowiki>[</nowiki><code>frozen</code><nowiki>]</nowiki> [[#Feature names|Extended_feature_name]]
+
+
+===Feature bodies ===
+Attribute_or_routine ::= <nowiki>[</nowiki>[[#Assertions|Precondition]]<nowiki>]</nowiki> 
+<nowiki>[</nowiki>[[#Local variable declarations|Local_declarations]]<nowiki>]</nowiki> 
+Feature_body 
+<nowiki>[</nowiki>[[#Assertions|Postcondition]]<nowiki>]</nowiki> 
+<nowiki>[</nowiki>[[#Rescue clauses|Rescue]]<nowiki>]</nowiki> 
+<code>end</code>
+
+Feature_body ::= [[#Routine bodies|Deferred]] | [[#Routine bodies|Effective_routine]] | [[#Attribute bodies|Attribute]]
+
+
+===Feature names ===
+Extended_feature_name ::= Feature_name <nowiki>[Alias]</nowiki> 
+
+Feature_name ::= [[#Identfiers|Identifier]] 
+
+Alias ::= <code>alias</code> '"' Alias_name '"' <nowiki>[</nowiki><code>convert</code><nowiki>]</nowiki>
+
+Alias_name ::= [[#Operators|Operator]] | Bracket 
+
+Bracket ::= "<nowiki>[ ]</nowiki>" 
+
+
+===Operators ===
+Operator ::= Unary | Binary 
+
+Unary ::= <code>not</code> | "+" | "-" | Free_unary 
+
+Binary ::= <nowiki>"+" | "-" | "*" | "/" | "//" | "\\" | "^" | ".." | "<" | ">" | "<=" | ">=" |</nowiki> <code>and</code> | <code>or</code> | <code>xor</code> | <code>and</code> <code>then</code> | <code>or</code> <code>else</code> | <code>implies</code> | Free_binary
+
+{{note| Free_unary and Free_binary are free operators that are distinct from (respectively) the ''standard'' unary and binary operators (one- or two-character symbols) explicitly listed in the Unary and Binary productions. See ''Definition: Free operator'' in the standard for more precision.}}
+
+
+===Assigner marks ===
+Assigner_mark ::= <code>assign</code> [[#Feature names|Feature_name]]
+
+
+===Inheritance parts ===
+Inheritance ::= Inherit_clause+ 
+
+Inherit_clause ::= <code>inherit</code> <nowiki>[Non_conformance]</nowiki> Parent_list 
+
+Non_conformance ::= "{" NONE "}" 
+
+Parent_list ::= {Parent ";" ...}+ 
+
+Parent ::= [[#Types|Class_type]] <nowiki>[Feature_adaptation]</nowiki>
+
+Feature_adaptation ::= <nowiki>[</nowiki>[[#Undefine clauses|Undefine]]<nowiki>]</nowiki> 
+<nowiki>[</nowiki>[[#Redefinition|Redefine]]<nowiki>]</nowiki> 
+<nowiki>[</nowiki>[[#Rename clauses|Rename]]<nowiki>]</nowiki> 
+<nowiki>[</nowiki>[[#Export adaptation|New_exports]]<nowiki>]</nowiki> 
+<nowiki>[</nowiki>[[#Select clauses|Select]]<nowiki>]</nowiki> 
+<code>end</code> 
+
+
+
+===Rename clauses ===
+Rename ::= <code>rename</code> Rename_list 
+
+Rename_list ::= {Rename_pair "," ...}+ 
+
+Rename_pair ::= [[#Feature names|Feature_name]] <code>as</code> [[#Feature names|Extended_feature_name]] 
+
+
+===Clients ===
+Clients ::= "{" Class_list "}" 
+
+Class_list ::= {[[#Class names|Class_name]] "," ...}+
+
+
+
+===Export adaptation ===
+New_exports ::= <code>export</code> New_export_list 
+
+New_export_list ::= {New_export_item ";" ...}+ 
+
+New_export_item ::= [[#Clients|Clients]] <nowiki>[</nowiki>[[#Feature parts|Header_comment]]<nowiki>]</nowiki> Feature_set 
+
+Feature_set ::= Feature_list | <code>all</code> 
+
+Feature_list ::= {[[#Feature names|Feature_name]] "," ...}+
+
+
+
+===Formal argument and entity declarations ===
+Formal_arguments ::= "(" [[#Formal argument and entity declarations|Entity_declaration_list]] ")" 
+
+Entity_declaration_list ::= {Entity_declaration_group ";" ...}+ 
+
+Entity_declaration_group ::= Identifier_list [[#Feature declarations|Type_mark]] 
+
+Identifier_list ::= {[[#Identfiers|Identifier]] "," ...}+ 
+
+
+===Routine bodies ===
+Deferred ::= <code>deferred</code> 
+
+Effective_routine ::= Internal | [[#External routines|External]] 
+
+Internal ::= Routine_mark [[#Instructions|Compound]] 
+
+Routine_mark ::= <code>do</code> | Once 
+
+Once ::= <code>once</code> <nowiki>[</nowiki> "("Key_list ")" <nowiki>]</nowiki> 
+
+Key_list ::= {[[#Manifest strings|Manifest_string]] "," ...}+
+
+
+===Local variable declarations ===
+Local_declarations ::= <code>local</code> <nowiki>[</nowiki>[[#Formal argument and entity declarations|Entity_declaration_list]]<nowiki>]</nowiki>
+
+
+===Instructions ===
+Compound ::= {Instruction ";" ...}* 
+
+Instruction ::= [[#Creation instructions|Creation_instruction]] | [[#Feature calls|Call]] | [[#Assignments|Assignment]] | [[#Assigner calls|Assigner_call]] | [[#Conditionals|Conditional]] | [[#Multi-branch instructions|Multi_branch]] 
+| [[#Loops|Loop]] | [[#Debug instructions|Debug]] | [[#Precursor|Precursor]] | [[#Check instructions|Check]] | [[#Rescue clauses|Retry]]
+
+
+===Assertions ===
+Precondition ::= <code>require</code> <nowiki>[</nowiki><code>else</code><nowiki>]</nowiki> Assertion 
+
+Postcondition ::= <code>ensure</code> <nowiki>[</nowiki><code>then</code><nowiki>]</nowiki> Assertion <nowiki>[</nowiki>[[#"Only" postcondition clauses|Only]]<nowiki>]</nowiki> 
+
+Invariant ::= <code>invariant</code> Assertion 
+
+Assertion ::= {Assertion_clause ";" ...}* 
+
+Assertion_clause ::= <nowiki>[</nowiki>Tag_mark<nowiki>]</nowiki> Unlabeled_assertion_clause 
+
+Unlabeled_assertion_clause ::= [[#Expressions|Boolean_expression]] | [[#Comments|Comment]] | `class`
+
+Tag_mark ::= Tag ":" 
+
+Tag ::= [[#Identfiers|Identifier]] 
+
+{{Note|Unlabeled_assertion_clause of the form `class` can be used only in a postcondition. It marks a feature that does not depend on object state and can be called without a target object using non-object call of the form `{CLASS_NAME}.feature_name (arguments)`.}}
+
+
+==="Old" postcondition expressions ===
+Old ::= <code>old</code> [[#Expressions|Expression]]
+
+
+==="Only" postcondition clauses ===
+Only ::= <code>only</code> <nowiki>[</nowiki>[[#Export adaptation|Feature_list]]<nowiki>]</nowiki>
+
+
+===Check instructions ===
+Check ::= <code>check</code> [[#Assertions|Assertion]] <nowiki>[</nowiki>[[#Notes|Notes]]<nowiki>]</nowiki> <code>end</code>
+
+
+===Variants ===
+Variant ::= <code>variant</code> <nowiki>[</nowiki>[[#Assertions|Tag_mark]]<nowiki>]</nowiki> [[#Expressions|Expression]]
+
+
+===Precursor ===
+Precursor ::= <code>Precursor</code> [Parent_qualification] <nowiki>[</nowiki>[[#Actual arguments|Actuals]]<nowiki>]</nowiki> 
+
+Parent_qualification ::= "{" [[#Class names|Class_name]] "}"
+
+
+===Redefinition ===
+Redefine ::= <code>redefine</code> [[#Export adaptation|Feature_list]]
+
+
+===Undefine clauses ===
+Undefine ::= <code>undefine</code> [[#Export adaptation|Feature_list]]
+
+
+===Types ===
+Type ::= Class_or_tuple_type | [[#Formal generic parameters|Formal_generic_name]] | Anchored 
+
+Class_or_tuple_type ::= Class_type | [[#Tuple types|Tuple_type]] 
+
+Class_type ::= [Attachment_mark] [[#Class names|Class_name]] <nowiki>[</nowiki>[[#Actual generic parameters|Actual_generics]]<nowiki>]</nowiki> 
+
+Attachment_mark ::= "?"  |  "!" 
+
+Anchored ::= [Attachment_mark] <code>like</code> Anchor 
+
+Anchor ::= [[#Feature names|Feature_name]] | <code>Current</code>
+
+
+===Actual generic parameters ===
+Actual_generics ::= <nowiki>"[" Type_list "]"</nowiki>
+
+Type_list ::= {[[#Types|Type]] "," ...}+
+
+
+===Formal generic parameters ===
+Formal_generics ::= <nowiki>"[" Formal_generic_list "]"</nowiki>
+
+Formal_generic_list ::= {Formal_generic ","...}+ 
+
+Formal_generic ::= <nowiki>[</nowiki><code>frozen</code><nowiki>]</nowiki> Formal_generic_name <nowiki>[</nowiki>[[#Generic constraints|Constraint]]<nowiki>]</nowiki> 
+
+Formal_generic_name ::= <nowiki>[?]</nowiki> [[#Identfiers|Identifier]]
+
+
+===Generic constraints ===
+Constraint ::= "->" Constraining_types <nowiki>[Constraint_creators]</nowiki> 
+
+Constraining_types ::= Single_constraint | Multiple_constraint 
+
+Single_constraint ::= [[#Types|Type]] [Renaming] 
+
+Renaming ::= [[#Rename clauses|Rename]] <code>end</code>
+
+Multiple_constraint ::= "{" Constraint_list "}" 
+
+Constraint_list ::= {Single_constraint "," ...}+ 
+
+Constraint_creators ::= <code>create</code> [[#Export adaptation|Feature_list]] <code>end</code>
+
+
+===Manifest arrays ===
+Manifest_array ::= <nowiki>[</nowiki>Manifest_array_type<nowiki>]</nowiki> <code><<</code> Expression_list <code>>></code>
+
+Manifest_array_type ::= <code>{</code> [[#Types|Type]] <code>}</code>
+
+Expression_list ::= {[[#Expressions|Expression]] <code>,</code> ...}*
+
+
+===Tuple types ===
+Tuple_type ::= <code>TUPLE</code> <nowiki>[Tuple_parameter_list]</nowiki>
+
+Tuple_parameter_list ::= <nowiki>"[" Tuple_parameters "]"</nowiki>
+
+Tuple_parameters ::= [[#Actual generic parameters|Type_list]] | [[#Formal argument and entity declarations|Entity_declaration_list]]
+
+
+===Manifest tuples ===
+Manifest_tuple ::= <nowiki>"["</nowiki> [[#Manifest arrays|Expression_list]] <nowiki>"]"</nowiki>
+
+
+===Converter clauses ===
+Converters ::= <code>convert</code> Converter_list 
+
+Converter_list ::= {Converter ","...}+ 
+
+Converter ::= Conversion_procedure | Conversion_query 
+
+Conversion_procedure ::= [[#Feature names|Feature_name]] "(" "{" [[#Actual generic parameters|Type_list]] "}" ")" 
+
+Conversion_query ::= [[#Feature names|Feature_name]] ":" "{" [[#Actual generic parameters|Type_list]] "}"
+
+
+===Select clauses ===
+Select ::= <code>select</code> [[#Export adaptation|Feature_list]]
+
+
+===Conditionals ===
+Conditional ::= <code>if</code> Then_part_list <nowiki>[Else_part]</nowiki> <code>end</code> 
+
+Then_part_list ::= {Then_part <code>elseif</code> ...}+ 
+
+Then_part ::= [[#Expressions|Boolean_expression]] <code>then</code> [[#Instructions|Compound]] 
+
+Else_part ::= <code>else</code> [[#Instructions|Compound]]
+
+
+Conditional_expression ::= <code>if</code> Then_part_expression_list <code>else</code> [[#Expressions|Expression]] <code>end</code> 
+
+Then_part_expression_list ::= {Then_part_expression <code>elseif</code> ...}+ 
+
+Then_part_expression ::= [[#Expressions|Boolean_expression]] <code>then</code> [[#Expressions|Expression]] 
+
+
+===Multi-branch instructions ===
+Multi_branch ::= <code>inspect</code> [[#Expressions|Expression]] <nowiki>[When_part_list] [Else_part]</nowiki> <code>end</code> 
+
+When_part_list ::= When_part+ 
+
+When_part ::= <code>when</code> Choices <code>then</code> [[#Instructions|Compound]] 
+
+Choices ::= {Choice "," ...}+ 
+
+Choice ::= [[#Constants|Constant]] | [[#Manifest constants|Manifest_type]] | Constant_interval | Type_interval 
+
+Constant_interval ::= [[#Constants|Constant]] ".." [[#Constants|Constant]] 
+
+Type_interval ::= [[#Manifest constants|Manifest_type]] ".." [[#Manifest constants|Manifest_type]]
+
+
+===Loops ===
+Loop ::=<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<nowiki>[</nowiki>Iteration<nowiki>]</nowiki><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<nowiki>[</nowiki>Initialization<nowiki>]</nowiki><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<nowiki>[</nowiki>[[#Assertions|Invariant]]<nowiki>]</nowiki><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<nowiki>[</nowiki>Exit_condition<nowiki>]</nowiki><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Loop_body<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<nowiki>[</nowiki>[[#Variants|Variant]]<nowiki>]</nowiki><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<code>end</code> 
+
+Iteration ::= <code>across</code> [[#Expressions|Expression]] <code>as</code>  [[#Identfiers|Identifier]]
+
+Initialization ::= <code>from</code> [[#Instructions|Compound]] 
+
+Exit_condition ::= <code>until</code> [[#Expressions|Boolean_expression]] 
+
+Loop_body ::=<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<code>loop</code> [[#Instructions|Compound]] |<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<code>all</code> [[#Expressions|Boolean_expression]] |<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<code>some</code> [[#Expressions|Boolean_expression]]
+
+
+===Debug instructions ===
+Debug ::= <code>debug</code> <nowiki>[</nowiki> "("[[#Routine_bodies|Key_list]] ")" ] [[#Instructions|Compound]] <code>end</code>
+
+
+===Attribute bodies ===
+Attribute ::= <code>attribute</code> [[#Instructions|Compound]]
+
+
+===Entities and variables ===
+Entity ::= Variable | Read_only 
+
+Variable ::= Variable_attribute | Local 
+
+Variable_attribute ::= [[#Feature names|Feature_name]] 
+
+Local ::= [[#Identfiers|Identifier]] | <code>Result</code> 
+
+Read_only ::= Formal | Constant_attribute | <code>Current</code> 
+
+Formal ::= [[#Identfiers|Identifier]] 
+
+Constant_attribute ::= [[#Feature names|Feature_name]]
+
+
+===Creators parts ===
+Creators ::= Creation_clause+ 
+
+Creation_clause ::= <code>create</code> <nowiki>[</nowiki>[[#Clients|Clients]]<nowiki>]</nowiki> <nowiki>[</nowiki>[[#Feature parts|Header_comment]]<nowiki>]</nowiki> Creation_procedure_list 
+
+Creation_procedure_list ::= {Creation_procedure ","...}+ 
+
+Creation_procedure ::= [[#Feature names|Feature_name]]
+
+
+===Creation instructions ===
+Creation_instruction ::= <code>create</code> <nowiki>[Explicit_creation_type]</nowiki> Creation_call 
+
+Explicit_creation_type ::= "{" [[#Types|Type]] "}" 
+
+Creation_call ::= [[#Entities and variables|Variable]] [Explicit_creation_call] 
+
+Explicit_creation_call ::= "." [[#Feature calls|Unqualified_call]]
+
+
+===Creation expressions ===
+Creation_expression ::= <code>create</code> [[#Creation instructions|Explicit_creation_type]] <nowiki>[</nowiki>[[#Creation instructions|Explicit_creation_call]]<nowiki>]</nowiki>
+
+
+===Equality expressions ===
+Equality ::= [[#Expressions|Expression]] Comparison [[#Expressions|Expression]] 
+
+Comparison ::= "=" | "/=" | "~" | "/~"
+
+
+===Assignments ===
+Assignment ::= [[#Entities and variables|Variable]] ":=" [[#Expressions|Expression]]
+
+
+===Assigner calls ===
+Assigner_call ::= [[#Expressions|Expression]] ":=" [[#Expressions|Expression]]
+
+
+===Feature calls ===
+Call ::= Object_call | Non_object_call 
+
+Object_call ::= <nowiki>[Target "."] Unqualified_call </nowiki>
+
+Unqualified_call ::= [[#Feature names|Feature_name]] <nowiki>[</nowiki>[[#Actual arguments|Actuals]]<nowiki>]</nowiki> 
+
+Target ::= [[#Entities and variables|Local]] | [[#Entities and variables|Read_only]] | Call | Parenthesized_target 
+
+Parenthesized_target ::= <code>(</code> [[#Expressions|Expression]] <code>)</code>
+
+Non_object_call ::= "{" [[#Types|Type]] "}" "." Unqualified_call
+
+
+===Actual arguments ===
+Actuals ::= "(" Actual_list ")" 
+
+Actual_list ::= {[[#Expressions|Expression]] "," ...}+
+
+
+===Object test ===
+Object_test ::= "{" [[#Identfiers|Identifier]] ":" [[#Types|Type]] "}" [[#Expressions|Expression]]
+
+
+===Rescue clauses ===
+Rescue ::= <code>rescue</code> [[#Instructions|Compound]] 
+
+Retry ::= <code>retry</code>
+
+
+===Agents ===
+Agent ::= Call_agent | Inline_agent 
+
+Call_agent ::= <code>agent</code> [[#Call agent bodies|Call_agent_body]] 
+
+Inline_agent ::= <code>agent</code> <nowiki>[</nowiki>[[#Formal argument and entity declarations|Formal_arguments]]<nowiki>]</nowiki> <nowiki>[</nowiki>[[#Feature declarations|Type_mark]]<nowiki>]</nowiki> <nowiki>[</nowiki>[[#Feature bodies|Attribute_or_routine]]<nowiki>]</nowiki> <nowiki>[</nowiki>[[#Call agent bodies|Agent_actuals]]<nowiki>]</nowiki>
+
+
+===Call agent bodies ===
+Call_agent_body ::= Agent_qualified | Agent_unqualified 
+
+Agent_qualified ::= Agent_target ". " Agent_unqualified 
+
+Agent_unqualified ::= [[#Feature names|Feature_name]] [Agent_actuals] 
+
+Agent_target ::= Entity | Parenthesized | [[#Manifest constants|Manifest_type]] 
+
+Agent_actuals ::= "(" Agent_actual_list ")" 
+
+Agent_actual_list ::= {Agent_actual "," ...}+ 
+
+Agent_actual ::= [[#Expressions|Expression]] | Placeholder 
+
+Placeholder ::= <nowiki>[</nowiki>[[#Manifest constants|Manifest_type]]<nowiki>]</nowiki> "?"
+
+
+===Expressions ===
+Expression ::= Basic_expression | Special_expression 
+
+Basic_expression ::= [[#Entities and variables|Read_only]] | [[#Entities and variables|Local]] | [[#Feature calls|Call]] | [[#Precursor|Precursor]] | [[#Equality expressions|Equality]] | Parenthesized | [[#"Old" postcondition expressions|Old]] | 
+[[#Operator expressions|Operator_expression]] | [[#Bracket expressions|Bracket_expression]]  | [[#Creation expression|Creation_expression]] | [[#Conditionals|Conditional_expression]]
+
+Special_expression ::= [[#Manifest constants|Manifest_constant]] | [[#Manifest arrays|Manifest_array]] | [[#Manifest tuples|Manifest_tuple]] | [[#Agents|Agent]] | [[#Object test|Object_test]] | Once_string | 
+Address 
+
+Parenthesized ::= "(" Expression ")" 
+
+Address ::= "$" [[#Entities and variables|Variable]] 
+
+Once_string ::= <code>once</code> [[#Manifest strings|Manifest_string]] 
+
+Boolean_expression ::= Basic_expression | [[#Manifest constants|Boolean_constant]] | [[#Object test|Object_test]]
+
+
+===Operator expressions ===
+Operator_expression ::= Unary_expression | Binary_expression 
+
+Unary_expression ::= Unary Expression 
+
+Binary_expression ::= [[#Expressions|Expression]] [[#Operators|Binary]] [[#Expressions|Expression]]
+
+
+===Bracket expressions ===
+Bracket_expression ::= Bracket_target "[" [[#Actual arguments|Actuals]] "]" 
+
+Bracket_target ::= [[#Feature calls|Target]] | [[#Expressions|Once_string]] | [[#Manifest constants|Manifest_constant]] | [[#Manifest tuples|Manifest_tuple]]
+
+
+===Constants ===
+Constant ::= [[#Manifest constants|Manifest_constant]] | Constant_attribute 
+
+Constant_attribute ::= [[#Feature names|Feature_name]]
+
+
+===Manifest constants ===
+Manifest_constant ::= [Manifest_type] Manifest_value 
+
+Manifest_type ::= "{" [[#Types|Type]] "}"
+
+Manifest_value ::= Boolean_constant |  
+Character_constant |  
+Integer_constant |  
+Real_constant |  
+[[#Manifest strings|Manifest_string]] | 
+Manifest_type 
+
+Sign ::= "+" | "-" 
+
+Integer_constant ::= <nowiki>[Sign]</nowiki> [[#Integers|Integer]] 
+
+Character_constant ::= " ' " [[#Characters|Character]] " ' " 
+
+Boolean_constant ::= <code>True</code> | <code>False</code> 
+
+Real_constant ::= <nowiki>[Sign]</nowiki> [[#Reals|Real]]
+
+
+===Manifest strings ===
+Manifest_string ::= Basic_manifest_string | Verbatim_string 
+
+Basic_manifest_string ::= ' " '  String_content  ' " ' 
+
+String_content ::= {[[#Simple strings|Simple_string]] [[#Line wrapping parts|Line_wrapping_part]] ...}+
+
+Verbatim_string ::= Verbatim_string_opener Line_sequence Verbatim_string_closer 
+
+Verbatim_string_opener ::= ' " ' <nowiki>[</nowiki>[[#Simple strings|Simple_string]]<nowiki>]</nowiki> Open_bracket 
+
+Verbatim_string_closer ::= Close_bracket <nowiki>[</nowiki>[[#Simple strings|Simple_string]]<nowiki>]</nowiki> ' " ' 
+
+Open_bracket ::= <nowiki>"[" | "{"</nowiki> 
+
+Close_bracket ::= "]" | "}"
+
+Line_sequence ::=  {[[#Simple strings|Simple_string]] [[#New line|New_line]] ...}+
+
+{{Note|Exactly the same [[#Simple strings|Simple_string]] (including embedded white space, if any) should be used in ''Verbatim_string_opener'' and ''Verbatim_string_closer'' of the same verbatim string.}}
+
+===External routines ===
+External ::= <code>external</code> External_language <nowiki>[External_name]</nowiki>
+
+External_language ::= Unregistered_language | [[#Registered languages|Registered_language]] 
+
+Unregistered_language ::= [[#Manifest strings|Manifest_string]] 
+
+External_name ::= <code>alias</code> [[#Manifest strings|Manifest_string]]
+{{note|If the `inline` keyword is used in the Registered_language part, then External_name part is the inline code on the specified language.}}
+
+
+===Registered languages ===
+Registered_language ::= [[#C externals|C_external]] | [[#C++ externals|C++_external]] | [[#DLL externals|DLL_external]]
+
+
+===External signatures ===
+External_signature ::= <code>signature</code> <nowiki>[External_argument_types] [: External_type]</nowiki> 
+
+External_argument_types ::= "(" External_type_list ")" 
+
+External_type_list ::= {External_type "," ...}* 
+
+External_type ::= [[#Simple strings|Simple_string]]
+
+
+===External file use ===
+External_file_use ::= <code>use</code> External_file_list 
+
+External_file_list ::= {External_file "," <nowiki>... }+ </nowiki>
+
+External_file ::= External_user_file | External_system_file 
+
+External_user_file ::= ' " '  [[#Simple strings|Simple_string]]  ' " ' 
+
+External_system_file ::= <nowiki>"<"</nowiki> [[#Simple strings|Simple_string]] <nowiki>">"</nowiki>
+
+===C externals ===
+C_external ::= ' " ' <code>C</code> <nowiki>[</nowiki><code>inline</code>] <nowiki>[</nowiki> [[#External signatures |External_signature]] <nowiki>] [</nowiki> [[#External file use |External_file_use]] <nowiki>] ' " '</nowiki>
+
+
+===C++ externals ===
+C++_external ::= ' " '  <code>C++</code> <code>inline</code> <nowiki>[</nowiki> [[#External signatures |External_signature]] <nowiki>] [</nowiki> [[#External file use |External_file_use]] <nowiki>] ' " '</nowiki>
+
+
+===DLL externals ===
+DLL_external ::= ' " ' <code>dll</code> <nowiki>[</nowiki><code>windows</code><nowiki>] DLL_identifier [DLL_index] [[</nowiki> [[#External signatures |External_signature]] <nowiki>] [</nowiki> [[#External file use |External_file_use]] <nowiki>] ' " ' </nowiki>
+
+DLL_identifier ::= [[#Simple strings|Simple_string]] 
+
+DLL_index ::= [[#Integers|Integer]]
+
+
+===Comments ===
+Comment ::= "- -" <nowiki>{</nowiki>[[#Simple strings|Simple_string]] Comment_break ...}* 
+
+Comment_break ::= New_line <nowiki>[Blanks_or_tabs] "- -"</nowiki>
+
+===Integers ===
+Integer ::= <nowiki>[Integer_base]</nowiki> Digit_sequence 
+
+Integer_base ::= "0" Integer_base_letter 
+
+Integer_base_letter ::= "b"  |  "c"  |  "x" |  "B"  |  "C"  |  "X" 
+
+Digit_sequence ::= Digit+ 
+
+Digit ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"  | 
+"a" | "b" | "c" | "d" | "e" | "f" | 
+"A" | "B" | "C" | "D" | "E" | "F" | "_"
+

documentation/22.05/eiffel/Language_reference/quick-reference-eiffel-programming-language/index.wiki

@@ -0,0 +1,16 @@
+[[Property:title|Quick reference to the Eiffel programming language]]
+[[Property:link_title|Quick Reference]]
+[[Property:weight|4]]
+[[Property:uuid|4f61365d-59f6-a394-678b-144bad8ec12f]]
+The Quick Reference to the Eiffel programming language provides an informal guide to the syntax and reserved words of the language. The Eiffel programming language is described in detail in the '''ISO/ECMA''' standard document, available [http://www.ecma-international.org/publications/standards/Ecma-367.htm online].  
+
+Sometimes there are differences between the language as defined by the standard and that which is implemented by Eiffel Software. These differences are documented in the online documentation.
+
+So, the final authority on Eiffel as implemented by Eiffel Software is the content of the standard document, amended by those variances cited in the [[Differences between standard ECMA-367 and Eiffel Software implementation|"differences" chapter of the online documentation]]. 
+
+This reference is based on the June 2006 ISO/ECMA standard document.
+
+
+
+
+

documentation/22.05/eiffel/Language_reference/void-safe-programming-eiffel/converting-existing-software-void-safety/changes-eiffel-libraries-support-void-safety.wiki

@@ -0,0 +1,88 @@
+[[Property:title|Void-safe changes to Eiffel libraries]]
+[[Property:weight|0]]
+[[Property:uuid|dc993c0e-fbec-dc5a-82c8-fbfd9fa9bc3a]]
+==Overview==
+
+During the adoption of void-safety, the software libraries provided by Eiffel Software have been converted to be void-safe. The bulk of the changes made to these libraries will have little or no adverse effect on your existing software as you go through the process of void-safe conversion. However, there are a few changes to the library that we consider "breaking" changes, that is, important changes that might cause problems in existing systems that use certain library classes. 
+
+
+{{note|Many of these changes were in effect in the ''experimental'' mode of versions 6.4 and 6.5. With the release of version 6.6, the ''experimental'' mode of previous versions became the ''default'' mode and, consequently may have caused these changes to become more apparent to some users. A ''compatibility'' mode is available to ease transition. The ''compatibility'' mode is accessible using the <code>-compat</code> command line option or through the EiffelStudio choices provided through the Microsoft Windows ''Start'' button. }}
+
+
+==Important changes to library classes==
+
+
+===Class ARRAY===
+
+====New preconditions====
+
+Some additional preconditions are in force in <code>ARRAY</code> in void-safe mode. 
+
+In void-unsafe mode, the behavior is equivalent to that of previous versions.
+
+====Feature make_from_special====
+
+The signature of this routine has changed. 
+
+Current signature: <code>make_from_special (a: SPECIAL [G])</code> 
+
+Previous signature: <code>make_from_special (a: SPECIAL [G]; min_index, max_index: INTEGER)</code>
+
+Using the current version will create an array with a range from 1 to the number of elements in the argument `a`.
+
+====Feature auto_resize====
+
+This implementation (private) feature has been removed.
+
+
+===Class ARRAYED_LIST===
+
+====Relationship to ARRAY====
+
+Previously <code>ARRAYED_LIST</code> conformed to <code>ARRAY</code>. This is no longer the case. The feature <code>{ARRAYED_LIST}.to_array</code> can be used to produce an instance of <code>ARRAY</code> from an instance of <code>ARRAYED_LIST</code>.
+
+====Features count and area====
+
+Previously these two queries, <code>count</code> and <code>area</code>, were attributes. They are now functions.
+
+
+===Class HASH_TABLE===
+
+The internal implementation has changed in ways that cause the order of traversal to differ from previous versions.
+
+
+===Classes SPECIAL and TO_SPECIAL===
+
+====Feature {SPECIAL}.make====
+
+This void-unsafe feature has been removed.
+
+In its place, the creation procedures <code>{SPECIAL}.make_filled</code> and <code>{SPECIAL}.make_empty</code> can be used.
+
+<code>{SPECIAL}.make_filled</code> is available in both ''default'' and ''compatible'' modes. Use this creation procedure if you want code that is compatible with both modes.
+
+<code>{SPECIAL}.make_empty</code> is available in ''default'' mode only.
+
+====Feature {TO_SPECIAL}.make_area====
+
+In order to reflect the above change to class <code>SPECIAL</code>, the <code>make_area</code> feature of <code>TO_SPECIAL</code> has been removed in favor of <code>{TO_SPECIAL}.make_filled_area</code> and <code>{TO_SPECIAL}.make_empty_area</code>.
+
+The availability of <code>{TO_SPECIAL}.make_filled_area</code> and <code>{TO_SPECIAL}.make_empty_area</code> corresponds to that noted above for the creation features of <code>SPECIAL</code>:
+
+<code>{TO_SPECIAL}.make_filled_area</code> is available in both ''default'' and ''compatible'' modes. Use <code>make_filled_area</code> for code that needs to compile in both modes.
+
+<code>{TO_SPECIAL}.make_empty_area</code> is available only in ''default'' mode.
+
+====Relationship of feature {SPECIAL}.count to {SPECIAL}.capacity====
+
+In previous versions, for a particular instance of <code>SPECIAL</code> the queries <code>count</code> and <code>capacity</code> yielded the same value.
+
+This is no longer always true. If an instance of <code>SPECIAL</code> is created with, for example, <code>make_empty (10)</code>, although the <code>capacity</code> will be 10, the <code>count</code> will be zero.
+
+However creating a <code>SPECIAL</code> using <code>make_filled</code> will produce an instance in which <code>count</code> and <code>capacity</code> are equal upon creation. So the behavior is similar to that of previous versions. Also, <code>make_filled</code> is available in both ''default'' and ''compatible'' modes. 
+
+If your code depends upon <code>count</code> and <code>capacity</code> having the same value, then you can use <code>make_filled</code> for creation. And then if you need resizing, use the "_with_default" versions of the "resized" features, specifically <code>resized_area_with_default</code> and <code>aliased_resized_area_with_default</code>.
+
+
+
+

documentation/22.05/eiffel/Language_reference/void-safe-programming-eiffel/converting-existing-software-void-safety/index.wiki

@@ -0,0 +1,335 @@
+[[Property:title|Converting existing software to void-safety]]
+[[Property:weight|6]]
+[[Property:uuid|eb901272-d405-2277-005d-e37275b9baa4]]
+If you have been using Eiffel for a while, you may be maintaining systems which were developed before Eiffel became void-safe. If that's the case, then you will probably want to make those systems void-safe. 
+
+In this section we will use the experience of converting a set of simple (but not too simple) legacy Eiffel classes to show the types of issues that you may encounter, and how to deal with them. 
+
+So in the discussion below, you will see references to these classes:
+
+
+{| border="1"
+|-
+! Class name
+! Description
+|-
+| APPLICATION
+| Simple root class containing declarations of types NVP and NVP_LIST
+|-
+| NVP
+| Class modeling name/value pairs of type STRING
+|-
+| NVP_LIST
+| Class modeling a list of NVP's with specialized behavior; heir of TWO_WAY_LIST [NVP]
+|}
+
+
+It's not important that you know much about the details of these classes. We will, however, look at certain parts of the classes in enough detail to resolve the conversion issues.
+
+
+=Conversion considerations=
+
+==To redesign or not to redesign==
+
+During the process of conversion of classes to void-safety, the compiler will point out problems which you will have to fix. Some of these will be straightforward, while others may be tricky. It is natural, or sometimes mandatory, at times to consider changing elements of the design of your software. 
+
+Also, as you sift through your existing software during the void-safe conversion, you may not get very far before you see things that you wish had been done differently. This occurs often during reviews of existing systems, not just because of the introduction of void-safety. 
+
+In the discussions that follow you will see these redesign opportunities arise, and the decisions that were made for these cases.
+
+==Be aware of changes to Eiffel libraries==
+
+The libraries distributed with EiffelStudio have been converted to support void-safety. Mostly the changes made will cause no problems for existing software. However a few changes have been identified as "breaking" changes. You may or may not encounter the effects of these changes, but you should be aware of how they could effect your software and what options you have for adapting to them. Breaking changes are described in the [[EiffelStudio release notes]] and in the page dedicated to [[Void-safe changes to Eiffel libraries]].
+
+=Conversion process=
+
+==Enable full class checking==
+
+First make sure your project will compile correctly under the configuration of EiffelStudio that you intend to use to convert to void-safe.
+
+Then set the project setting '''Full Class Checking''' to '''True'''. Do a ''[[Clean compile|clean compile]]'' of your system. 
+
+Full class checking will analyze your classes to make sure that in cases of inheritance, features of the parent classes are rechecked for validity in the heirs.
+
+Here's an example of the kind of error you might expect when compiling with full class checking:
+
+
+[[Image:VGCC error]]
+
+
+The situation here is that the feature <code>split</code> has been inherited (from class <code>TWO_WAY_LIST [G]</code>) by our class <code>NVP_LIST</code>. Feature <code>split</code> includes code to create and attach feature <code>sublist</code> which is typed <code>attached like Current</code> which in this case means <code>attached NVP_LIST</code>. To do this creation, <code>split</code> uses a creation procedure <code>make_sublist</code>. 
+
+Now here's the rub: <code>NVP_LIST</code> has not named <code>make_sublist</code> as a creation procedure: 
+<code>
+create
+    make, make_from_string, make_from_file_named
+</code>
+If we go to the <code>create</code> part of <code>NVP_LIST</code> and add <code>make_sublist</code> to its list of creation procedures, this will fix the problem:
+<code>
+create
+    make, make_from_string, make_from_file_named, make_sublist
+</code>
+
+So, fix any problems that arise out of turning on full class checking.
+
+==Enable other project settings==
+
+The second step in conversion of existing software is to change the values of the other void-safe related project settings and use the void-safe configurations for any delivered libraries and precompilations.
+
+In the project settings for the target in which you are working, set '''Void safety''' to '''Complete''', '''Transitional''' , '''Initialization''' or '''Conformance'''. 
+
+{{note|Remember that during a transitional period starting with v6.4, there will be multiple versions of the configuration files for Eiffel libraries and precompiles. For example, base.ecf (void-unsafe) and base-safe.ecf (void-safe). Starting with v16.11 there is only one configuration file for libraries (e.g., base.ecf) that works with both void-safe and void-unsafe client software, but if you are using a precompile, there could be different versions for void-safe and void-unsafe precompiles.}}
+
+If necessary, remove Eiffel libraries and any precompiled library that your project uses and re-add them with their void-safe configuration files. Because you've set your target to void-safety, when you click '''Add Library''', you should see only void-safe configurations by default. 
+You will see a check box on the dialog that you can uncheck if you want to see all available library configurations:
+
+
+[[Image:VoidSafeAddLibraryDialog]]
+  
+
+Now do a [[Clean compile|clean compile]].
+
+If you've replaced a precompiled library that you have not already built, EiffelStudio will offer to build it for you on the fly:
+
+
+[[Image:VoidSafePrecompileOffer]]
+
+
+Now you should see error messages representing any situation in your project in which the compiler determines that it cannot guarantee void-safety.
+
+This is what our legacy system produced:
+
+
+[[Image:VoidSafeErrorList]]
+
+
+==Fix the issues==
+
+Next you fix the problems that the compiler discovered. The compiler errors concerning void-safety typically will be of three varieties. 
+
+# VEVI: violations of the '''Variable initialization rule'''. An attached variable is not '''properly set'''.
+# VUTA: violations of the '''Target rule'''. The target of a feature call is not attached.
+# VJAR (and other related codes): violations of attached status considered in conformance. The attachment status of the source of an assignment (or an argument to a feature call) is not compatible with that of the target of the assignment (or the formal argument).
+
+Let's look at some specific cases and how fixing them unfolds.
+
+===Variables not properly set===
+
+[[Image:VoidSafeVEVI1]]
+
+
+There are two VEVI errors like this in class <code>APPLICATION</code> of our legacy system. They are probably the most obvious and easiest cases to handle. 
+
+<code>
+feature {NONE} -- Initialization
+
+    make
+            -- Run application.
+        do
+                ...
+        end
+
+feature -- Access
+
+    my_nvp: NVP
+            -- NVP for testing
+
+    my_nvp_list: NVP_LIST
+            -- NVP_LIST for testing
+</code>
+
+Here attribute declarations for <code>my_nvp</code> and <code>my_nvp_list</code> are made. These are assumed to be attached because of the project setting. But the create routine <code>make</code> fails to create objects and attach them. So by adding those creations, as shown below, the compiler is satisfied.
+
+<code>
+    make
+            -- Run application.
+        do
+            create my_nvp.make ("SomeName", "SomeValue")
+            create my_nvp_list.make
+                ...
+        end
+</code>
+
+
+In a second case, there is also an Initialization rule violation (VEVI), this time on <code>Result</code>, in this routine:
+
+<code>
+    at_first (nm: STRING): NVP
+            -- The first found NVP with name matching nm.
+            -- 	Or Void if not found
+        require
+            nm_valid: nm /= Void and then not nm.is_empty
+        local
+            tc: CURSOR
+        do
+            tc := cursor
+            start
+            name_search (nm)
+            if not exhausted then
+                Result := item
+            end
+            go_to (tc)
+        ensure
+            index_unchanged: index = old index
+        end
+</code>
+
+Here we cannot just ensure that <code>Result</code> is always attached, because, as indicated by the header comment, <code>Result</code> is allowed to be void by design. 
+
+So the least impact to this routine will be to declare its type as <code>detachable</code>:
+
+<code>
+    at_first (nm: STRING): detachable NVP
+            -- The first found NVP with name matching nm.
+            -- 	Or Void if not found
+</code>
+
+
+The same change is made in other routines that can return void by design, particularly including a routine called <code>value_at_first</code>, which gets our attention next.
+
+The case of <code>at_first</code> offered us an opportunity to redesign (or not). We might have been able to leave <code>at_first</code> attached. After all, in void-safe software, the fewer <code>detachable</code>s, the better. Maybe we could devise a way, possibly through preconditions and other queries, that would guarantee that <code>at_first</code> attempts to execute only when it can return a value. 
+
+But <code>at_first</code> is an exported query, so a consequence of such a change in the class design is that it would affect the class interface in such a way that existing clients would have to be modified to comply. In other words, it would be a "breaking" change. 
+
+
+===Source of assignment does not conform to target===
+
+The change to <code>at_first</code> satisfies the VEVI issue in <code>at_first</code>, but it introduces a previously unseen conformance issue (VJAR) in the routine <code>value_at_first</code>:
+
+
+[[Image:VoidSafeVJAR1]]
+
+
+<code>value_at_first</code> looks like this:
+
+<code>
+    value_at_first (nm: STRING): detachable STRING
+            -- Value from first found NVP with name matching nm
+            -- 	Or Void of not found
+        require
+            nm_valid: nm /= Void and then not nm.is_empty
+        local
+            tn: NVP
+        do
+            tn := at_first (nm)
+            if tn /= Void then
+                Result := tn.value
+            end
+        end
+</code>
+
+The problem is that the local variable <code>tn</code> is declared as <code>attached</code>, but we know that now the result of <code>at_first</code> is detachable, making this assignment invalid:
+<code>
+            tn := at_first (nm)
+</code>
+
+Here the '''attached syntax''' can fix the problem and streamline the routine:
+
+<code>
+    value_at_first (nm: STRING): detachable STRING
+            -- Value from first found NVP with name matching nm
+            -- 	Or Void of not found
+        require
+            nm_valid: nm /= Void and then not nm.is_empty
+        do
+            if attached at_first (nm) as tn then
+                Result := tn.value
+            end
+        end
+</code>
+
+In this version <code>tn</code> need not be declared as a local variable. Remember that the attached syntax provides a fresh local variable, if the expression is not void. 
+
+===Both VEVI and VJAR errors===
+
+A design issue in class <code>NVP_LIST</code> causes both conformance and initialization compiler errors. In the original design, an instance of the class NVP_LIST could traverse its contents NVP-by-NVP with inherited functionality.  Additionally, <code>NVP_LIST</code> has immediate functionality allowing an instance to traverse its contents in two different ways returning "sublists" based on recurring patterns of the <code>name</code> attributes of a sequence of name/value pairs. 
+
+These two traversal methods are referred to as "sequencing" and "segmenting". It's not important that you understand the details of what these traversals do. But it is important to know that a valid instance of <code>NVP_LIST</code> can either be in the process of sequencing or in the process of segmenting, or neither. It is invalid to be both sequencing ''and'' segmenting. 
+
+Two class attributes are maintained to store the recurring patterns of values of <code>{NVP}.name</code> that guide traversal:
+
+<code>
+feature {NONE} -- Implementation
+
+    sequence_array: ARRAY [STRING]
+            -- The current array of names being used for
+            --  sequence traversal
+
+    segment_array: ARRAY [STRING]
+            -- The current array of names being used to determine
+            --  the termination of list segments
+</code>
+
+In the original class design, each of these attributes would be void unless their corresponding traversal was active. So the class contains the following clauses in its invariant:
+
+<code>
+	not_sequencing_and_segmenting: not (segment_readable and sequence_readable)
+	sequence_traversal_convention: (sequence_array = Void) = (not sequence_readable)
+	segment_traversal_convention: (segment_array = Void) = (not segment_readable)
+</code>
+
+Of course by default these attributes are considered to be attached. So, because they are not initialized during creation, we see initialization errors. Because elements of the class intentionally set them to <code>Void</code>, we see conformance errors. 
+
+Here we have another opportunity to redesign (or not). We could mark the two arrays as <code>detachable</code>, recompile and fix any problems this causes (in fact, it causes eight errors: six Target rule violations, and two conformance issues). 
+
+However, because these attributes are not exported, we may be able to leave them attached and make changes to the implementation design without making breaking changes to the interface. 
+
+Those exported features which take arguments of the type <code>ARRAY [STRING]</code> which will serve as sequencing or segmenting control also require that the array contain at least one element. For example, the contract for feature <code>segment_start</code> contains these preconditions:
+
+<code>
+    segment_start (nms: ARRAY [STRING_8])
+            -- Place segment cursor on the first occurrence of a seqment of list which
+            -- 	begins at the current cursor position and
+            -- 	terminates in a sequence with names equivalent to and ordered the same as `nms'.
+            -- If no such sequence exists, then ensure exhausted
+        require
+            nms_valid: nms /= Void and then (nms.count > 0)
+            not_sequencing: not sequence_readable
+</code>
+
+Because the restriction always exists that a valid <code>sequence_array</code> or <code>segment_array</code> must contain at least one element, it is possible to redesign the implementation of the class such that an empty <code>sequence_array</code> and <code>segment_array</code> could serve the same purpose as a <code>Void</code> one does in the original design.
+
+So the invariant clauses that we saw above would now become:
+
+<code>
+	not_sequencing_and_segmenting: not (segment_readable and sequence_readable)
+	sequence_traversal_convention: (sequence_array.is_empty) = (not sequence_readable)
+	segment_traversal_convention: (segment_array.is_empty) = (not segment_readable)
+</code>
+
+We already have compiler errors (VJAR's) that point us to those places in which we have code that sets either <code>sequence_array</code> or <code>segment_array</code> to <code>Void</code>. Like this:
+
+<code>
+            segment_array := Void
+</code>
+
+These instances need to be changed to attach an empty array, maybe like this:
+
+<code>
+            create segment_array.make (1, 0)
+</code>
+
+Additionally, some postconditions which reference the implementation features <code>sequence_array</code> and/or <code>segment_array</code> would have to be changed. Looking at the postcondition clauses for <code>segment_start</code> we see that <code>segment_array</code> is expected (or not) to be <code>Void</code>:
+
+<code>
+    ensure
+        started: (not exhausted) implies (segment_readable and (segment_array /= Void) and (last_segment_element_index > 0))
+        not_started: exhausted implies ((not segment_readable) and (segment_array = Void) and (last_segment_element_index = 0))
+</code>
+
+To support the "empty array" design, <code>segment_start</code>'s postcondition clauses would be:
+
+<code>
+    ensure
+        started: (not exhausted) implies (segment_readable and (not segment_array.is_empty) and (last_segment_element_index > 0))
+        not_started: exhausted implies ((not segment_readable) and (segment_array.is_empty) and (last_segment_element_index = 0))
+</code>
+
+
+
+{{SeeAlso|<br/>[[Converting EiffelVision 2 Systems to Void-Safety]]<br/>[[Void-safe changes to Eiffel libraries]]}}
+
+
+
+
+

documentation/22.05/eiffel/Language_reference/void-safe-programming-eiffel/converting-existing-software-void-safety/mixing-void-safe-and-void-unsafe-software.wiki

@@ -0,0 +1,28 @@
+[[Property:title|Mixing void-safe and void-unsafe software]]
+[[Property:weight|3]]
+[[Property:uuid|3446f214-3c77-ef41-98eb-92942298630c]]
+{{underconstruction}}
+
+
+=Introduction=
+
+Eiffel Software recommends that any new development efforts be implemented using Eiffel's void-safe approach, thus eliminating one more common type of runtime failure. It is also recommended that existing software be converted to void-safety at the earliest opportunity.
+
+Under some circumstances it is possible and even helpful to mix void-safe and void-unsafe libraries. During conversion to void-safety, for example, it can be helpful to compile and test a void-unsafe system with void-safe versions of the libraries it depends upon. 
+
+=Rule for mixing void-safety modes=
+
+The rule for using void-safe and void-unsafe software together is fairly simple. 
+
+
+{{Rule|name=Mixing void-safe and void-unsafe software|text=<br/>
+1) A class that is void-unsafe may depend upon other classes (as suppliers or ancestors) which are either void-safe or void-unsafe.<br/>
+2) A class that is void-safe may depend only upon other classes that are void-safe.}}
+
+
+This means that if the root class of a system is void-safe, then every other class in the system must also be void-safe.  
+
+However, if you are converting a system to void-safety, it's likely that your root class and the classes in the closely related clusters will be void-unsafe. The rule allows you to mix the void-safe versions of the Eiffel Software library classes from the EiffelStudio distribution with your void-unsafe system during conversion.
+
+
+

documentation/22.05/eiffel/Language_reference/void-safe-programming-eiffel/creating-new-void-safe-project.wiki

@@ -0,0 +1,390 @@
+[[Property:link_title|New void-safe project]]
+[[Property:title|Creating a new void-safe project]]
+[[Property:weight|2]]
+[[Property:uuid|92cea2e9-b094-6380-2c5d-1cd1eb3038b4]]
+
+{{TOC|limit=2}}
+
+Now that we've been introduced to the Eiffel void-safe facilities, let's look at what it takes to set up a new void-safe software project. Here we'll look at the void-safety related project settings and how the can be used. Then we'll look deeper into the use of some of the void-safe tools.
+
+==Project settings for void-safe projects==
+
+There are two project settings that are related to void-safety. These settings can be set with great granularity throughout your project to allow you maximum flexibility, particularly when including classes or libraries that are void-unsafe or that have been converted to void-safety, but must do double duty in the void-safe and void-unsafe worlds. 
+
+===The ''"Void-safe"'' setting===
+
+The '''Void-safe''' setting determines whether and how the Eiffel compiler checks your project against the void-safe related validity rules. 
+
+This is the essential void-safe project setting. It can assume one of the following values:
+# '''No''': No checking against any of the void-safety validity rules. Attachment marks '''attached''' and '''detachable''' are simply ignored.
+# '''Conformance''': The attachment marks are not ignored for type conformance checks (with respect to VJAR/VBAR and related validity rules).
+# '''Initialization''': Validity rules are selectively checked. The initialization rule (VEVI) and the target rule (VUTA) are checked only for attached entities and attached call targets -- i.e., detachable cases are not checked. 
+# '''Transitional''': It is an obsolete level which is for users who have already migrated their code to void-safety using an old version of the compiler which did not implement all the void-safety validity rules (especially with agent initialization).
+# '''Complete''': Complete checking against all void-safety validity rules.
+
+So, for a new void-safe project, you would want to set this option first to '''Conformance''', then '''Initialization''' and finally to '''Complete'''. This will let you migrate your code progressively without much changes at each steps.
+
+
+===The ''"Full class checking"'' setting===
+
+This setting instructs the compiler to recheck inherited features in descendant classes. This setting is True and cannot be changed for projects with some void-safety level enabled.
+
+
+==Void-safe libraries==
+
+As of EiffelStudio version 13.11, all libraries distributed with EiffelStudio are void-safe except the EiffelCOM library.
+
+{{note|During a period of transition, there are different Eiffel configuration files (.ecf's) for void-unsafe and void-safe projects (for example, base.ecf and base-safe.ecf). If you have set the '''Void-safe''' setting to check for void-safety, then when you add a library to your project in EiffelStudio, you will see only the void-safe configurations by default. Starting with version 16.11 there is only one version of each of the configuration files for each library. The single configuration files serve both void-unsafe and void-safe projects.}}
+
+===Using generic classes===
+
+Void-safety affects generic classes. Fortunately, from the viewpoint of those writing clients to the generic classes in the EiffelBase library, not much has changed. Still, you should understand the interplay between void-safety and [[ET: Genericity and Arrays|genericity]].
+
+Consider a generic class like <code>LIST [G]</code>. The formal generic parameter <code>G</code> represents an arbitrary type. In a generic derivation of <code>LIST [G]</code>, say <code>LIST [STRING]</code>, the formal generic type is replaced by an actual generic type, in this case <code>STRING</code>. 
+
+Remember that unconstrained genericity, <code>LIST [G]</code>, for example, is really a case of [[ET: Inheritance#Constrained genericity|constrained genericity]] in which the generic parameter is constrained to <code>ANY</code>, that is, it could be written <code>LIST [G -> ANY]</code>.
+
+With the advent of void-safe Eiffel, the unconstrained generic class name <code>LIST [G]</code> now equates to <code>LIST [G -> detachable ANY]</code>. Because any type, say <code>T</code>, (synonymous with <code>attached T</code> in void-safe Eiffel) conforms to <code>detachable T</code>, this change facilitates the production of generic classes, but has little effect on writers of clients to those classes.
+
+This change works for all the generic classes in EiffelBase ... except for one: <code>ARRAY</code>.  Arrays are a special case because we often create arrays with a pre-allocated number of elements. In the case of expanded types, there's not a problem. For example, in this code
+<code>
+    my_array: ARRAY [INTEGER]
+                ...
+            create my_array.make (1, 100)
+</code>
+we create <code>my_array</code> with one hundred <code>INTEGER</code> elements. <code>INTEGER</code> is an expanded type, and each element is initialized by applying the default initialization rule for <code>INTEGER</code>, i.e, the integer representation of zero.
+
+However, if <code>my_array</code> had been declared of a type with reference semantics, say <code>STRING</code> (meaning, of course, <code>attached STRING</code>, the default rule would not work well, because the default initialization for references types is <code>Void</code> which would not be allowed in an array of elements of any attached type.
+
+The solution to this challenge is fairly simple. For arrays of elements of detachable or expanded types, there is no different behavior. When dealing with arrays of elements of attached types, we must be careful. 
+
+Creating an array using <code>ARRAY</code>'s creation procedure <code>make</code> may still be safe in some cases. Specifically, <code>make</code> can be used with arrays of elements of attached types if the arguments have values such that an empty array will be created, that is, when
+<code>
+        min_index = max_index + 1
+</code>
+
+In all other situations involving arrays of elements of attached types, <code>make</code> may not be used to do the creation. Rather, you should use the creation procedure <code>make_filled</code> which takes three arguments. The first is an object of the type of the array, and the second and third are the minimum and maximum indexes, respectively. When the array is created, each of the elements will be initialized with a reference to the object of the first argument. 
+
+So, a call using <code>make_filled</code> would look like this:
+<code>
+    my_array: ARRAY [STRING]
+                ...
+            create my_array.make_filled (" ", 1, 100)
+</code>
+Upon creation, each element of the array will reference the same object; an object of type <code>STRING</code> composed of one space character.
+
+
+==Using the ''attribute'' keyword carefully==
+
+The keyword <code>attribute</code> should be used with some care. You might be tempted to think that it would be convenient or add an extra element of safety to use [[Void-safety: Background, definition, and tools#Self-initializing attributes|self-initializing attributes]] widely. And in a way, you would be correct. But you should also understand that there is a price to pay for using self-initializing attributes and stable attributes. It is that upon every access, an evaluation of the state of the attribute must be made. So, as a general rule, you should avoid using self-initializing attributes only for the purpose of lazy initialization.
+
+
+==More about the ''attached syntax''==
+
+The complete attached syntax is:
+<code>
+		attached {SOME_TYPE} exp as l_exp
+</code>
+In this section, we will see more ways in which to use this versatile language facility.
+
+===As a CAP-like construct which yields a local variable===
+
+In the introduction to the attached syntax, we used an example which showed how the attached syntax is directly relevant to void-safety. That is, the code: 
+<code>
+            if x /= Void then
+--              ... Any other instructions here that do not assign to x
+                x.f (a)
+            end
+</code>
+
+is a CAP for <code>x</code> ... but that's only true if <code>x</code> is a local variable or a formal argument to the routine that contains the code. 
+
+So to access a detachable attribute safely,  we could declare a local variable, make an assignment, and test for <code>Void</code> as above. Something like this:
+<code>
+    my_detachable_attribute: detachable MY_TYPE
+
+            ...
+    some_routine
+        local
+           x: like my_detachable_attribute
+        do
+            x := my_detachable_attribute
+            if x /= Void then
+--              ... Any other instructions here that do not assign to x
+                x.f (a)
+            end
+                ...
+</code>
+The attached syntax can both check the attached status of a detachable attribute and also provide a new local variable. So the routine becomes:
+<code>
+    some_routine
+        do
+            if attached my_detachable_attribute as x then
+--                  ... Any other instructions here that do not assign to x
+                x.f (a)
+            end
+                ...
+</code>
+
+===As a test for attachment===
+
+In its simplest form, the attached syntax can be used to test attached status only:
+<code>
+            if attached x then
+                do_something
+            else
+                do_something_different
+            end
+</code>
+
+So in this simple form, <code>attached x</code> can be used instead of <code>x /= Void</code>. The two are semantically equivalent, and which one you choose is a matter of personal preference. 
+
+
+===As a tool for "once per object"===
+
+There is a code pattern for functions that exists in some Eiffel software to effect "once-per-object / lazy evaluation". 
+
+{{note|As of EiffelStudio version 6.6, the use of this code pattern effecting "once per object" is no longer necessary. V6.6 includes explicit support for <code>once</code> routines which can be adjusted by a [[ET: Once routines and shared objects#Adjusting once semantics with "once keys"|once key]] to specify once per object.}}
+
+This "once-per-object" code pattern employs a cached value for some object which is not exported. When it is applied, the "once-per-object" function checks the attachment status of the cached value. If the cached value is void, then it is created and assigned to <code>Result</code>. If the cached value was found already to exist, then it is just assigned to <code>Result</code>. 
+
+Here's an example of this pattern used to produce some descriptive text of an instance of its class:
+
+<code>
+feature -- Access
+
+    descriptive_text: STRING
+        local
+            l_result: like descriptive_text_cache
+        do
+            l_result := descriptive_text_cache
+            if l_result = Void then
+                create Result.make_empty
+                    -- ... Build Result with appropriate
+                    -- descriptive text for Current.
+                descriptive_text_cache := Result
+            else
+                Result := l_result
+            end
+        ensure
+            result_attached: Result /= Void
+            result_not_empty: not Result.is_empty
+            result_consistent: Result = descriptive_text
+        end
+
+feature {NONE} -- Implementation
+
+    descriptive_text_cache: like descriptive_text
+
+</code>
+This example will not compile in a void-safe project (class types are attached by default). The problem is that the attribute <code>descriptive_text_cache</code> is of an attached type, therefore will be flagged by the compiler as not properly set (VEVI). Of course, it will be ... that's the whole idea here: not to initialize <code>descriptive_text_cache</code> until it's actually used. So it sounds like <code>descriptive_text_cache</code> should be declared detachable. That is:
+<code>
+    descriptive_text_cache: detachable like descriptive_text
+</code>
+This change will make this routine compile in a void-safe project. But you should notice that there is a ripple-down effect due to the change. Within the routine, <code>l_result</code> is typed <code>like descriptive_text_cache</code>, so it also will be detachable. Therefore we might expect trouble, because later in the routine we have:
+<code>
+                Result := l_result
+</code>
+Because we know Result is attached and l_result is detachable, we might expect a compiler error in which the source of an assignment does not conform to its target (VJAR). 
+
+But we don't get such an error. The reason is two-fold. First, <code>l_result</code> is a local variable whose use can be protected by a CAP. Second, the CAP in this case is the check to ensure that <code>l_result</code> is not void. We only make the assignment to <code>Result</code> if <code>l_result</code> is not void. So the compiler can prove that <code>l_result</code> cannot be void at the point at which the assignment occurs ... therefore, no error.
+
+Because the '''attached syntax''' can test attached status and provide a local variable, it can be used to remove some unnecessary code from this routine. The version of the routine that follows shows the attached syntax being used to test the attached status of <code>descriptive_text_cache</code> and yield the local variable <code>l_result</code> in the case that <code>descriptive_text_cache</code> is indeed attached. 
+<code>
+    descriptive_text: STRING
+        do
+            if attached descriptive_text_cache as l_result then
+                Result := l_result
+            else
+                create Result.make_empty
+                    -- ... Build Result with appropriate
+                    -- descriptive text for Current.
+                descriptive_text_cache := Result
+            end
+        ensure
+            result_attached: Result /= Void
+            result_not_empty: not Result.is_empty
+            result_consistent: Result = descriptive_text
+    end
+
+feature {NONE} -- Implementation
+
+    descriptive_text_cache: like descriptive_text
+
+</code>
+
+
+===As a replacement for assignment attempt===
+
+The assignment attempt ( <code>?=</code> ) has traditionally been used to deal with external objects (e.g., persistent objects from files and databases) and to narrow the type of an object in order to use more specific features. The latter is a process known by names such as "down casting" in some technological circles. A classic example is doing specific processing on some elements of a polymorphic data structure. Let's look at an example. Suppose we have a <code>LIST</code> of items of type <code>POLYGON</code>:
+<code>
+    my_polygons: LIST [POLYGON]
+</code>
+<code>POLYGON</code>s could be of many specific types, and one of those could be <code>RECTANGLE</code>. Suppose too that we want to print the measurements of the diagonals of all the <code>RECTANGLE</code>s in the list. Class <code>RECTANGLE</code> might have a query <code>diagonal</code> returning such a measurement, but <code>POLYGON</code> would not, for the reason that the concept of diagonal is not meaningful for all <code>POLYGON</code>s, e.g., <code>TRIANGLE</code>s.
+
+As we traverse the list we would use assignment attempt to try to attach each <code>POLYGON</code> to a variable typed as <code>RECTANGLE</code>. If successful, we can print the result of the application of <code>diagonal</code>. 
+<code>
+    l_my_rectangle: RECTANGLE
+
+                ...
+            from
+                my_polygons.start
+            until
+                my_polygons.exhausted
+            loop
+                l_my_rectangle ?= my_polygons.item
+                if l_my_rectangle /= Void then
+                    print (l_my_rectangle.diagonal)
+                    print ("%N")
+                end
+                my_polygons.forth
+            end
+</code>
+The '''attached syntax''' allows us to check both attached status and type, and provides us with a fresh local variable when appropriate:
+<code>
+            from
+                my_polygons.start
+            until
+                my_polygons.exhausted
+            loop
+                if attached {RECTANGLE} my_polygons.item as l_my_rectangle then
+                    print (l_my_rectangle.diagonal)
+                    print ("%N")
+                end
+                my_polygons.forth
+            end
+</code>
+As with the other examples of the '''attached syntax''', it is no longer necessary to make a declaration for the local variable, in this case <code>l_my_rectangle</code>.
+
+
+==More about CAPs==
+
+===Use of <code>check</code> instructions===
+
+In void-safe mode, the compiler will accept code that it can prove will only apply features to attached references at runtime ... and you help this process along by using the tools of void-safety, like attached types and CAPs. On the other hand, the compiler will reject code that it cannot guarantee is void-safe. Sometimes this may cause you a problem. There may be subtle situations in which you feel quite certain that a section of code will be free of void calls at runtime, but the compiler doesn't see it the same way, and rejects your code. In cases like this, you can usually satisfy the compiler by using <code>check</code> instructions.
+
+Technically speaking, <code>check</code> instructions are not CAPs. But they are useful in cases in which an entity is always expected to be attached at a certain point in the code. In the following example, the attribute <code>my_detachable_any</code> is detachable. But at the particular point at which it is the source of the assignment to <code>l_result</code>, it is expected always to be attached. If it is not attached at the time of the assignment, and therefore <code>l_result</code> becomes void, then an exception should occur. The <code>check</code> instruction provides this behavior.
+
+The following sample shows the <code>check</code> instruction at work. There are reasons why this is not the best use use of <code>check</code> in this case, and we will discuss that next.
+
+<code>
+                -- A not-so-good example of using check.
+
+    my_detachable_any: detachable ANY
+            ...
+    my_attached_any: ANY
+        local
+            l_result: like my_detachable_any
+        do
+            l_result := my_detachable_any
+            check
+                attached l_result 
+            end
+            Result := l_result
+        end
+</code>
+
+Here the assertion in the <code>check</code> guarantees that <code>l_result</code> is attached at the time of its assignment to <code>Result</code>. If <code>my_detachable_any</code> is ever not attached to an object, then an exception will be raised. 
+
+So what's wrong with the sample above? It would be fine in ''workbench'' code, but what happens if the code is in ''finalized'' mode, in which assertions are typically discarded?
+
+The answer is that the <code>check</code> in the sample above would no longer be effective, and the resulting executable would no longer be void-safe.
+
+The solution to this problem is found in a different form of the <code>check</code> instruction. Consider the same example, but this time using <code>check ... then ... end</code>:
+
+<code>
+                -- A better way of using check.
+
+    my_detachable_any: detachable ANY
+            ...
+    my_attached_any: ANY
+        do
+            check attached my_detachable_any as l_result then
+                Result := l_result
+            end
+        end
+</code>
+
+Here, in the improved version of the example, the <code>check ... then ... end</code> is used along with the <code>attached</code> syntax. This streamlines the code a bit by eliminating the need to declare a separate local entity, while achieving the same effect as the previous example. If <code>my_detachable_any</code> is attached at runtime, then the temporary variable <code>l_result</code> is created and attached to the same object. Then the body of the <code>check ... then ... end</code> is executed. If <code>my_detachable_any</code> is not attached, an exception occurs.
+
+Another important benefit, one that solves the problem with the original example, comes from the way in which <code>check ... then ... end</code> is handled by the compiler. The <code>check ... then ... end</code> form '''is always monitored, even if assertion checking is turned off at all levels''', as is usually done in finalized code.
+
+===Choosing CAPs versus the Attached Syntax===
+
+The attached syntax is convenient because it can check attached status and deliver a new local variable at the same time. But there are cases in which you might choose instead to define a local variable and use a CAP. Suppose you had code acting on several similar and detachable expressions, and you use the attached syntax in each case:
+<code>
+    foobar
+        do
+            if attached dictionary_entry ("abc") as l_abc then
+                l_abc.do_something
+            end
+            if attached dictionary_entry ("def") as l_def then
+                l_def.do_something
+            end
+            if attached dictionary_entry ("ghi") as l_ghi then
+                l_ghi.do_something
+            end
+        end
+</code>
+This routine causes three local variables to be allocated for the duration of routine <code>foobar</code>, one each for <code>l_abc</code>, <code>l_def</code>, and <code>l_ghi</code>. And it is no better to do this:
+<code>
+    foobar
+        do
+            if attached dictionary_entry ("abc") as l_entry then
+                l_entry.do_something
+            end
+            if attached dictionary_entry ("def") as l_entry then
+                l_entry.do_something
+            end
+            if attached dictionary_entry ("ghi") as l_entry then
+                l_entry.do_something
+            end
+        end
+</code>
+Even though the names are the same, still three separate local variables are allocated for <code>foobar</code>.
+
+In cases like this, you could effect a minor performance improvement by declaring one local variable and reusing it. In the following code, only one local variable is used and access to it is protected by the CAP <code>if l_entry /= Void then</code>. 
+<code>
+    foobar
+       local
+          l_entry: like dictionary_entry
+       do
+          l_entry := dictionary_entry ("abc")
+          if l_entry /= Void then
+                l_entry.do_something
+          end
+          l_entry := dictionary_entry ("def")
+          if l_entry /= Void then
+                l_entry.do_something
+          end
+          l_entry := dictionary_entry ("ghi")
+          if l_entry /= Void then
+                l_entry.do_something
+          end
+    end
+</code>
+
+==Stable attributes==
+
+Remember that stable attributes are actually detachable attributes, with the difference that they can never be the target of an assignment in which the source is <code>Void</code> or anything that could have a value of <code>Void</code>.
+
+Stable attributes are useful in situations in which there are valid object life scenarios in which some particular attribute will never need an object attached, or will only need an object attached late in the scenario. So in this case, the attribute is used only under certain runtime conditions. Declaring these attributes as stable eliminates the need to make attachments during object creation. Yet once needed, that is, once the attribute is attached, it will always be attached.
+
+Also, you should remember that unlike other attributes, you can access stable attributes directly in a CAP:
+<code>
+    my_stable_attribute: detachable SOME_TYPE
+        note
+            option: stable
+        attribute
+        end
+
+            ...
+
+            if my_stable_attribute /= Void then
+                my_stable_attribute.do_something
+            end
+
+            ...
+</code>
+
+{{SeeAlso| [[Void-safety: Background, definition, and tools#Types as "attached" or "detachable"|Types as "attached" or "detachable"]].}}

documentation/22.05/eiffel/Language_reference/void-safe-programming-eiffel/index.wiki

@@ -0,0 +1,23 @@
+[[Property:link_title|Void-safe programming]]
+[[Property:title|Void-safe programming in Eiffel]]
+[[Property:weight|10]]
+[[Property:uuid|a03568e8-eb79-70d7-04a3-6fd3ed7ac2b3]]
+=Void-safe software development using Eiffel: introduction=
+
+When you develop software in Eiffel, you can be assured (at compile time) that your system will not attempt (at run time) to apply a feature to a void reference -- or, in the terminology of other languages such as C, "dereference a null pointer".
+
+Throughout the history of Eiffel, new capabilities -- agents, the SCOOP concurrency mechanism and many others -- have added considerable expressive power to the languag,e while causing minimum impact on existing software. Void-safe Eiffel is such an innovation, which instead of adding new mechanisms ''removes'' a major source of instability in programs, present in all other major languages: null-pointer dereferencing. To say that Eiffel is void-safe means that such catastrophic yet common errors simply will not occur.
+
+There is in fact no need to speak of "void-safe Eiffel". The language is just Eiffel... and it is void-safe, just as it is statically typed.  We still occasionally refer to "Void-safe Eiffel" simply because until 2005 or so Eiffel was not void-safe (it had to start somewhere), and you may still encounter older documentation that talks about "calls on void targets" (null-pointer dereferences). But in today's Eiffel such an event is impossible. 
+
+The rest of this chapter explains void safety:
+
+# How is void-safety defined?
+# What are the specific elements of the mechanism?
+# How do these relate to Eiffel before void-safety?
+# What do I need to know to produce standard Eiffel software?
+# What do I need to know to convert my existing systems to be standard?
+
+
+
+

documentation/22.05/eiffel/Language_reference/void-safe-programming-eiffel/void-safety-background-definition-and-tools.wiki

@@ -0,0 +1,289 @@
+[[Property:modification_date|Mon, 20 Dec 2021 10:16:27 GMT]]
+[[Property:publication_date|Mon, 20 Dec 2021 10:13:53 GMT]]
+[[Property:link_title|Background and tools]]
+[[Property:title|Void-safety: Background, definition, and tools]]
+[[Property:weight|0]]
+[[Property:uuid|689f62b2-5675-5ab6-cd47-d891cf3d484d]]
+=Background=
+
+The primary focus of Eiffel is on software quality. Void-safety, like static typing, is another facility for improving software quality. Void-safe software is protected from run time errors caused by calls to void references, and therefore will be more reliable than software in which calls to void targets can occur. The analogy to static typing is a useful one. In fact, void-safe capability could be seen as an extension to the type system, or a step beyond static typing, because the mechanism for ensuring void-safety is integrated into the type system.
+
+==Static typing==
+
+You know that static typing eliminates a whole class of software failures. This is done by making an assurance at compile time about a feature call of the form:
+<code>
+            x.f (a)
+</code>
+Such a feature call is judged acceptable at compile time only if the type of <code>x</code> has a feature <code>f</code> and that any arguments, represented here by <code>a</code>, number the same as the formal arguments of <code>f</code>, and are compatible with the types of those formal arguments.
+
+
+In statically typed languages like Eiffel, the compiler guarantees that you cannot, at run time, have a situation in which feature <code>f</code> is not applicable to the object attached to <code>x</code>. If you've ever been a Smalltalk programmer, you are certainly familiar with this most common of errors that manifests itself as "Message not understood." It happens because Smalltalk is not statically typed. 
+
+==Void-unsafe software==
+
+Static typing will ensure that there is some feature <code>f</code> that can be applied at run time to <code>x</code> in the example above. But it does not assure us that, in the case in which <code>x</code> is a reference, that there will always be an object attached to <code>x</code> at any time <code>x.f (a)</code> is executed. 
+
+This problem is not unique to Eiffel. Other environments that allow or mandate reference semantics also allow the possibility of void-unsafe run time errors. If you've worked in Java or .NET you may have seen the NullReferenceException. Sometimes you might have experienced this rather poetic sounding message: "Object reference not set to an instance of an object". In Eiffel you would see "Feature call on void target". All these are the hallmarks of run time errors resulting from void-unsafe software.
+
+{{note|If you need a review of difference between reference types and expanded types in Eiffel, see [[ET: The Dynamic Structure: Execution Model|the chapter of the Eiffel Tutorial dedicated to the Eiffel execution model]]. }}
+
+Of course this is not an issue with instances of expanded types, because these instances are indeed "expanded" within their parent objects. But we could not imagine a world with expanded types only. References are important for performance reasons and for modeling purposes. For example, consider that a car has an engine and a manufacturer. When we model cars in software, it might be appropriate for engines to be expanded types, as each car has one engine. But certainly the same is not true for manufacturer. Many cars can share, through a reference, a single manufacturer.
+
+So, references are necessary, but we want them to be trouble free. 
+
+==Void-safe software==
+
+Void-safe software, then, is software in which the compiler can give assurance, through a static analysis of the code, that at run time whenever a feature is applied to a reference, that the reference in question will have an object attached. This means that the feature call
+<code>
+            x.f (a)
+</code>
+is valid only if we are assured that <code>x</code> will be attached to an object when the call executes.
+
+
+{{info|This validity rule is called the '''Target rule''', validity code VUTA, and is the primary rule for void-safety. In the following discussion, you will see that other validity rules are involved, too. You can see the formal definition of all validity rules in the [http://www.ecma-international.org/publications/standards/Ecma-367.htm ISO/ECMA standard document] available online. }}
+
+
+Once we have committed ourselves to this validity rule, we must have a strategy for complying with the rule.
+
+=Elements of the void-safe strategy=
+
+Here are the tools of void-safe trade. They will each be addressed in more detail throughout the documentation that follows. As you look at these elements it helps to try to think about things from the compiler's viewpoint ... after all, it is the compiler that we expect to give us the guarantee that our code is indeed void-safe. 
+
+First let's look at a couple of approaches that won't work.
+
+It might occur to us that we could enforce compliance with the target rule by simply eliminating the concept of void references. But this would not be practical. Void is a valuable abstraction that is useful in many situations, such as providing void links in structures. So, we must keep void ... but we want to keep it under control.
+
+Another thought might be that we could just have the compiler do all the work for us. But would be impossibly time consuming for the compiler to investigate every conceivable execution path available to a system to make certain that every possible feature call was made on an attached reference. 
+
+So, all of this boils down to the fact that we have to take some actions that help the compiler along. That's what the following are about.
+
+==Certified Attachment Patterns (CAPs)==
+
+We know that in the context of certain code patterns, it is clear that it would be impossible for a reference to be void. These patterns are identified and we call them CAPs, short for Certified Attachment Patterns. Here is a very straightforward example expressed in a syntax that should be familiar to all Eiffel developers:
+<code>
+            if x /= Void then
+--              ... Any other instructions here that do not assign to x
+                x.f (a)
+            end
+</code>
+Here a check is made to ensure <code>x</code> is not void. Then as long as no assignments to <code>x</code> are made in the interim, a feature <code>f</code> can be applied to <code>x</code> with the certainty that <code>x</code> will be attached at the time ... and importantly, this can be determined at compile time. So, we say that this code pattern is a CAP for <code>x</code>.
+
+
+It is important to understand that in this example (and with other CAPs), <code>x</code> is allowed to be a local variable or formal argument only. That is, <code>x</code> may not be an attribute or general expression (with one exception which we will see [[#Stable attributes|below]]). Direct access to class attribute references cannot be allowed via a CAP due to the fact that they could be set to void by a routine call in some execution path invoked by the intervening instructions or possibly even different process thread. In a later [[Void-safety: Background, definition, and tools#Types as "attached" or "detachable"|section]], we will see that this is not quite such a limitation as it may appear at this point.
+
+
+{{note|You will find more useful information about CAPs in [[Creating a new void-safe project#More about CAPs|More about CAPs]]. Learn how certain code patterns are determined to be CAPs in [[What makes a Certified Attachment Pattern]]. }}
+
+
+==The ''attached syntax'' (object test)==
+
+For the purposes of void-safety, the '''attached syntax''' does double duty for us. It allows us to make certain that a reference is attached, and it provides us a safe way to access objects that are attached to class attributes. 
+
+We noted earlier that this code
+<code>
+            if x /= Void then
+--              ... Any other instructions here that do not assign to x
+                x.f (a)
+            end
+</code>
+creates a CAP for feature calls on <code>x</code>, but only if <code>x</code> is a local variable or a formal argument. 
+
+By using the '''attached syntax''', we can perform an '''object test''' on a variable. That is, the attached syntax is a <code>BOOLEAN</code> expression which provides an answer to the question "Is <code>x</code> attached to an object?" At the same time, if indeed <code>x</code> is attached to an object, the attached syntax will deliver to us a fresh local variable, also attached to <code>x</code>'s object, on which we can make feature calls.
+<code>
+            if attached x as l_x then
+                l_x.f (a)
+            end
+</code>
+In the example above, <code>x</code> is tested to make certain that it is attached. If so, the new local <code>l_x</code> becomes attached to the same object as <code>x</code>. And so the object can be used safely even if <code>x</code> is a class attribute. So, the attached syntax, is really another CAP, because it provides a clearly verifiable place for the application of features to targets that are guaranteed not to be void.
+
+
+{{note|The attached syntax has other syntax variations as well as other uses. These will be discussed [[Creating a new void-safe project#More about the attached syntax|later]]. }}
+
+
+One way to make sure we comply with the target rule would be always use a CAP or the attached syntax every time we want to apply a feature to a referenced object. That might work, but it falls among the impractical approaches to the problem ... it would break a very high percentage of existing Eiffel code, not to mention cluttering things up quite a bit.
+
+==Types as "attached" or "detachable"==
+
+Rather than trying to protect every feature call, Eiffel allows us to declare any variable as being of an '''attached type'''. This is an important extension to the Eiffel type system. 
+
+In Eiffel prior to the introduction of void-safe facilities, any reference variable could be set to <code>Void</code>. So, all variables were considered '"detachable"'. 
+
+The current standard Eiffel supports a mixture of '''attached''' and '''detachable''' types. When a variable is declared of an attached type, as in the following example, then the compiler will prevent it from being set to <code>Void</code> or set to anything that can be set to <code>Void</code>.
+ 
+<code>
+    my_attached_string: attached STRING
+</code>
+
+It is easy to imagine that the more declarations are of attached types, the easier it will be to guarantee that a call to a void target cannot take place at run time. In fact, if every declaration was guaranteed to be of an attached type, then that would be all that was needed to satisfy the Target rule. 
+
+However, it wouldn't be workable to have only attached types, because sometimes it's important to allow references to have a value of <code>Void</code>.  
+
+When it is necessary to allow <code>Void</code> as a value, a declaration can use the ''detachable mark'' as in the following.
+<code>
+    my_detachable_string: detachable STRING
+</code> 
+
+
+This doesn't mean that on every declaration you must put either an ''attached mark'' or a ''detachable mark''. Declarations that are unmarked are allowed. If a declaration contains neither '''attached''' nor '''detachable''', then it is assumed to be '''attached'''.
+
+In Eiffel then, all declarations will have types that are either '''attached''' or '''detachable'''. As a result, we need only use CAPs and the attached syntax with detachable types. So the important thing to remember is that ''direct access to class attributes of detachable types is never void-safe.''
+
+===Attachment and conformance===
+
+The distinction between attached and detachable types results in a small but important addition to the rules of conformance. Because variables declared as attached types can never be void, then it is important not to allow any assignment of a detachable source to an attached target. However, assigning an attached source to a detachable target is permissible. The following code shows both cases (as described earlier, class types are attached by default).
+<code>
+    my_attached_string: STRING
+    my_detachable_string: detachable STRING
+
+                ...
+
+            my_attached_string := my_detachable_string    -- Invalid
+            my_detachable_string := my_attached_string    -- Valid
+</code>
+
+
+==Initialization rule==
+
+If we have attached types, then we can assume variables declared of these types, once attached, will always be attached. But how do they get attached in the first place? That's what the initialization rule is all about. 
+
+The rule says that at any place in which a variable is accessed, it must be '''properly set'''. A variable's being properly set has a precise, but not particularly simple definition in the Eiffel standard. 
+
+
+{{info|You can find the formal definition of the '''Variable initialization rule''', validity code VEVI, and its related concepts such as '''properly set''' variables in the [http://www.ecma-international.org/publications/standards/Ecma-367.htm ISO/ECMA standard document]. }}
+
+
+Still, it's not too hard to understand the basics of initializing variables of attached types:
+
+* For the initialization of attributes of a class, we can apply a rule similar to that of the initial evaluation of class invariants ... that is, everything must be in order upon completion of a creation procedure. If a class attribute is of an attached type, then each of the class's creation procedures is responsible for making sure that the attribute is attached to an object upon its completion. 
+
+* A local variable is considered properly set if it is initialized at some point '''preceding''' its use in any execution path in which it is used. So immediately after its <code>create</code> instruction, the local variable would be considered properly set. But if the <code>create</code> occurred in the <code>then</code> part of an <code>if</code> instruction, the local variable would not be properly set in the <code>else</code> part of that same <code>if</code> instruction:
+
+<code>
+    my_routine
+                -- Illustrate properly set local variable
+        local
+            l_my_string: STRING
+        do
+            if my_condition then
+                create l_my_string.make_empty
+--              ... l_my_string is properly set here
+            else
+--              ... l_my_string is not properly set here
+            end
+        end
+</code>
+
+* A variable is considered properly set if it is '''self-initializing'''. What it means to be self-initializing is explained below.
+
+==Self-initializing attributes==
+
+A self-initializing attribute is guaranteed to have a value when accessed at run time. Declarations of self-initializing attributes are characterized by the use of the code that follows the <code>attribute</code> keyword. The code is executed to initialize the attribute in the case that the attribute is accessed prior to being initialized in any other way. 
+
+So, self-initializing attributes are ordinary attributes, with the restriction that they are of both ''attached'' types and ''reference'' types (i.e., not expanded types or constants).  Self-initializing attributes still can be, and typically will be initialized in the traditional ways. The difference is that the code in the attribute part serves as a kind of safety net guaranteeing that a self-initializing attribute will never be void, even if it is accessed prior to being initialized by one of the traditional means.
+
+<code>
+    value: STRING
+        attribute
+            create Result.make_empty
+        end
+</code>
+
+In the example above, the attribute <code>value</code> will be attached to an object of type <code>STRING</code>, in fact, the empty string, if no other initialization occurs before the first access of <code>value</code>.
+
+==Rule for conformance==
+
+You will remember that the Eiffel type system dictates that an assignment instruction:
+<code>
+            x := y
+</code>
+is valid only if the type of <code>y</code> is '''compatible''' with the type of <code>x</code>. Compatibility, in turn, means either '''conversion''' or '''conformance'''. 
+
+The fact that all types are either '''attached''' or '''detachable''' adds another dimension to rule for conformance:
+*If x is of an attached type, then y must be of an attached type.
+This prevents us from circumventing attached status at run time. If <code>x</code> is of a detachable type, then <code>y</code> could be either a detachable or attached type.
+
+The same goes for routine calls. In a call:
+<code>
+            z.r (y)
+</code>
+where <code>x</code> is the formal argument for <code>r</code>, then if x is of an attached type, then y must be of an attached type.
+
+==Stable attributes==
+
+Stable attributes are really stable ''detachable'' attributes, as adding the concept of stability is meaningful only for detachable attributes. Declaring a detachable attribute as stable, means that it behaves like a detachable attribute except that its assignment rules mimic those of attached attributes. In other words, a stable attribute does not need to be attached during object creation the way that attributes declared as attached must. But like attached type attributes, stable attributes can never be the target of an assignment in which the source is <code>Void</code> or a detachable type.
+<code>
+    my_test: detachable TEST
+        note
+            option: stable
+        attribute
+        end
+</code>
+
+This means that even though stable attributes do not need to be initialized like attributes of attached types, once they are attached to an object, they can never be void again.
+
+Stable attributes are also interesting in that they are the only exception to the rule given above in the [[Void-safety: Background, definition, and tools#Certified Attachment Patterns (CAPs)|CAPs section]] that stated that direct access to attributes cannot be protected by a CAP. A stable attribute can be used under the protection of a CAP. This is because once a stable attribute has an object attached, it can never again be set to <code>Void</code>. So there's no worry about having the attribute's state going unexpectedly from attached to non-attached because of the actions of other routines or threads.
+
+==Rule for generic parameters==
+
+Generic classes provide another question. A generic class like
+<code>
+class
+    C [G]
+        ...
+</code>
+allows us to create a type by providing a specific actual generic parameter for the formal parameter <code>G</code>.
+
+So, two valid derivations are:
+<code>
+    my_integer_derivation: C [INTEGER]
+</code>
+and
+<code>
+    my_employee_derivation: C [EMPLOYEE]
+</code>
+
+If class C contains a declaration:
+<code>
+    x: G
+</code>
+What do we know about the void-safety of <code>x</code> ? 
+
+In the case of the <code>INTEGER</code> derivation above, we know <code>x</code> is safe because <code>INTEGER</code> is an expanded type. But often types like <code>EMPLOYEE</code> will be reference types which could be void at run time.
+
+'''For a class like <code>C [G]</code>, <code>G</code> is considered detachable'''. As a result, because of the [[Void-safety: Background, definition, and tools#Rule for conformance|rule for conformance]], any class will work for an actual generic parameter. That means that both of the following are valid generic derivations:
+
+<code>
+    my_detachable_string_derivation: C [detachable STRING]
+
+    my_attached_string_derivation: C [attached STRING]
+</code>
+
+If <code>C</code> contains a declaration <code>x: G</code>, the application of features to <code>x</code> must include verification of attachment (CAPs, attached syntax, etc).
+
+Constrained genericity can be used to create generic classes in which the generic parameter represents an attached type. If class <code>C</code> had been defined as: 
+<code>
+class C [G -> attached ANY]
+            ...
+</code>
+then <code>x</code> in this class has attached type <code>G</code>. Consequently, the actual generic type in any derivation must be attached ... and feature calls on <code>x</code> are safe.
+
+==Rule for ARRAYs==
+
+The rule for generic parameters applies to all generic types ... except <code>ARRAYs</code>. In the typical creation of an <code>ARRAY</code>, we would provide a minimum and maximum index. 
+<code>
+    my_array: ARRAY [STRING]
+
+                ...
+
+            create my_array.make (1, 100)
+</code>
+During creation, an area to store the appropriate number of entries is also created. And depending upon the actual generic parameter, these entries are either objects for expanded types or references for reference types. 
+
+In the case of an actual generic parameter of an attached reference type, all the elements must be attached to instances of type during the creation of the ARRAY. The <code>make</code> procedure would not do this. Creation of an <code>ARRAY</code> in which the actual generic parameter is attached must be done using the <code>make_filled</code> creation procedure. 
+<code>
+            create my_array.make_filled ("", 1, 100)
+</code>
+The first argument is an object of the actual generic type, in this case an empty <code>STRING</code>. Every entry in the newly created <code>ARRAY</code> will be initialized to reference this object.
+
+
+For more detail on void-safe use of arrays and other generic classes, see the section: [[Creating a new void-safe project#Using generic classes|Using generic classes]].

documentation/22.05/eiffel/Language_reference/void-safe-programming-eiffel/what-makes-certified-attachment-pattern.wiki

@@ -0,0 +1,182 @@
+[[Property:title|What makes a Certified Attachment Pattern]]
+[[Property:weight|8]]
+[[Property:uuid|1a20197d-5a88-59c3-9a04-512399125661]]
+
+==A little background on CAPs==
+
+Certified Attachment Patterns (CAPs) were described in the section on [[Void-safety: Background, definition, and tools#Certified attachment patterns (CAPs)|void-safety tools]]. To review, a CAP is a code pattern for a certain expression, say <code>exp</code> of a detachable type that ensures that <code>exp</code> will never have a void run-time value within the covered scope. 
+
+A simple example is the familiar test for void reference:
+<code>
+            if l_x /= Void then
+                l_x.do_something    -- Valid for formal arguments, local variables, and stable attributes
+            end
+</code>
+We know that after the explicit check to make sure <code>l_x</code> is not <code>Void</code>, that the feature application <code>l_x.do_something</code> is void-safe.
+Of course, you should remember from previous discussions that <code>l_x</code> must be a local variable, a formal argument, or a  [[Void-safety: Background, definition, and tools#Stable attributes|stable attribute]].
+
+When void-safety was first envisioned for Eiffel, it was intended that individual CAPs would be proven or certified and documented. This would produce a "catalog" of CAPs. 
+
+What happened instead is that the members of the Eiffel standard committee have been able to produce and publish as part of the [http://www.ecma-international.org/publications/standards/Ecma-367.htm standard] a definition of the nature of a CAP from which a determination can be made as to whether a particular code pattern is or is not a CAP. 
+
+The definition in the standard document is not easily readable by most developers. So, in this documentation, you will see various examples of CAPs and the rationale behind them.
+
+
+==The standard CAP definition==
+
+The Eiffel standard (2nd edition, June 2006) defines a CAP as follows:
+----
+'''''A Certified Attachment Pattern (or CAP) for an expression <code>exp</code> whose type is detachable is an occurrence of <code>exp</code> in one of the following contexts: '''''
+
+
+'''''1. <code>exp</code> is an Object-Test Local and the occurrence is in its scope. '''''
+
+'''''2. <code>exp</code> is a read-only entity and the occurrence is in the scope of a void test involving <code>exp</code>.'''''
+----
+
+The terminology used in the definition is precise. For example, terms like "read-only entity" and "scope of a void test" have specific meanings that are supported by their own definitions in the standard. 
+
+Still, the standard does contain informative text that gives us a guideline that a CAP is a scheme to ensure that a particular expression of a detachable type will never have void run-time value in the scope covered by the CAP.
+
+The discussion here will follow that guideline, and, as such, will be less formal (and consequently less precise) than that in the standard, and is intended to be a practical guide. Of course, the [http://www.ecma-international.org/publications/standards/Ecma-367.htm standard document] is available for download if you wish to investigate the specifics.
+
+
+==CAP-able expressions==
+
+In the first context in the definition above, the expression <code>exp</code> can be an '''Object-Test Local'''. An Object-Test Local is the identifier specified for a fresh local entity in an '''object test'''. Remember, object tests are coded using the [[Void-safety: Background, definition, and tools#The attached syntax (object test)|attached syntax]]. 
+<code>
+            attached x as l_x 
+</code>
+In the object test expression above, the identifier '''<code>l_x</code>''' is an Object-Test Local.
+
+In the second context, the expression can be a '''read-only entity'''. Read-only entities are:
+# Constant attributes
+# Formal arguments
+# Object-Test Locals
+# <code>Current</code>
+
+Additionally, the Eiffel Software compiler allows for [[Void-safety: Background, definition, and tools#Stable attributes|stable attributes]] and local variables to be protected by a CAP. 
+
+===Stable attributes===
+
+Stable attributes are the only class attributes which are CAP-able. This is because stable attributes, once attached at run-time, can never have a void value again. So, you use stable attributes safely by using them under the protection of a CAP. Consider this stable attribute:
+<code>
+    my_stable_string: detachable STRING
+        note
+            option: stable
+        attribute
+        end
+</code>
+The detachable attribute <code>my_stable_string</code>, because it is stable, is not required to be initialized during the creation of instances of the class in which it is a feature. That means that for each instance, <code>my_stable_string</code> can be initialized later during the instance's life-cycle or not at all. But because it is detachable, <code>my_stable_string</code> cannot be accessed in any context in which it cannot be determined that it is currently attached. For ordinary attributes, this means either using an object test and accessing the object through an object test local, or using using a local variable under the protection of a CAP. 
+
+Stable attributes however, can be used directly in a CAP, as shown below: 
+
+<code>
+            if my_stable_string /= Void then
+                my_stable_string.append ("abc")        -- Valid
+                    ...
+</code>
+
+So using stable attributes can reduce the need to initialize rarely used attributes, and the need to code object tests.
+
+===Local variables===
+
+Local variables can be used in a CAP as long as they are not the target of an assignment whose source is <code>Void</code> or some expression which could possibly be void.
+
+So, for a local variable <code>l_string</code>, the following is valid:
+<code>
+        local
+            l_string: detachable STRING
+        do
+            if l_string /= Void then
+                l_string.append ("abc")        -- Valid
+                    ...
+</code>
+
+But, if <code>l_string</code> had been a target of an assignment in which the source could possibly have been void, then it could no longer be guaranteed that <code>l_string</code> is not void. So, assuming that <code>my_detachable_string</code> is an attribute declared as type <code>detachable STRING</code>, the second application of <code>append</code> in this example would be invalid:
+
+<code>
+        local
+            l_string: detachable STRING
+        do
+            if l_string /= Void then
+                l_string.append ("abc")        -- Valid
+                l_string := my_detachable_string
+                l_string.append ("xyz")        -- Invalid: my_detachable_string might have been void
+                    ...
+</code>
+
+==Common CAPs==
+
+We've already seen the simple test for void as a CAP:
+<code>
+    local
+        l_str: detachable STRING
+
+                ...
+
+            if l_str /= Void then
+                l_str.append ("xyz")        -- Valid
+            end
+</code>
+
+Additionally, a creation instruction can serve as a CAP. After the execution of a creation instruction, the target of the creation instruction will be attached:
+<code>
+        local
+            l_str: detachable STRING
+        do
+            create l_str.make_empty
+            l_str.append ("xyz")        -- Valid
+                ...
+</code>
+
+
+==Less obvious cases==
+
+There are some situations that constitute CAPs that we might not think of immediately. 
+
+For example, the case of the non-strict boolean operator <code>and then</code>: 
+<code>
+            if x /= Void and not x.is_empty then        -- Invalid
+                ...
+
+            if x /= Void and then not x.is_empty then        -- Valid
+                ...
+</code>
+Assuming that <code>x</code> is CAP-able, the first line of code is invalid because the expression <code>x.is_empty</code> could always be evaluated even in the case in which <code>x</code> is void. 
+
+In the second line of code, the non-strict boolean is used, guaranteeing that <code>x.is_empty</code> will not be evaluated in cases in which <code>x</code> is void. Therefore, <code>x.is_empty</code> falls within the scope of the void test on <code>x</code>.
+
+In contracts, multiple assertion clauses are treated as if they were separated by <code>and then</code>. This allows preconditions like the one in the following example:
+<code>
+my_routine (l_str: detachable STRING)
+        require
+            l_str /= Void
+            not l_str.is_empty        -- Valid
+                ...
+</code>
+
+Another not-so-obvious CAP is related to the use of the logical implication:
+<code>
+        local
+            l_str: detachable STRING
+        do
+            if l_str /= Void implies some_expression then
+                ...
+            else
+                l_str.append ("xyz")        -- Valid
+            end
+</code>
+
+
+==The bottom line on CAPs==
+
+In summary, CAPs provide void-safe protection for certain types of detachable expressions. 
+
+Possibly the characteristic of CAPs which is most important to developers is whether or not a particular CAP is supported by the compiler. In other words, from the developers viewpoint, the only opinion that matters in the argument of whether a particular pattern constitutes a CAP is that of the compiler. 
+
+If the compiler can provide assurance that a certain code pattern guarantees void-safe protection, then the developer will have that pattern available as a CAP. Likewise, even if a pattern can be shown logically to be a CAP, but for some reason it is not supported by the compiler, then that pattern will not available as a CAP and the compiler will not allow its use. 
+
+
+
+