Author:halw

Date:2009-09-15T21:20:11.000000Z


git-svn-id: https://svn.eiffel.com/eiffel-org/trunk@300 abb3cda0-5349-4a8f-a601-0c33ac3a8c38
This commit is contained in:
halw
2009-09-15 21:20:11 +00:00
parent aa1c9e0833
commit 0634355ebc
2 changed files with 18 additions and 7 deletions

View File

@@ -72,7 +72,7 @@ It is important to understand that in this example (and with other CAPs), <code>
{{note|You will find more useful information about CAPs in [[Void-safe programming in Eiffel#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''===
===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.

View File

@@ -11,21 +11,32 @@ Certified Attachment Patterns (CAPs) were described in the section on [[Void-saf
A simple example is the familiar test for void reference:
<code>
if x /= Void then
x.do_something
if l_x /= Void then
l_x.do_something
end
</code>
We know that after the explicit check to make sure <code>x</code> is not <code>Void</code>, that the feature application <code>x.do_something</code> is void-safe.
Of course, you should remember from previous discussions that <code>x</code> must be a local variable, a formal argument, or a [[Void-safety: Background, definition, and tools#Stable attributes|stable attribute]].
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 standard committee was able to produce 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.
What happened instead is that the members of the Eiffel standards 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: ''
#'' <code>exp</code> is an Object-Test Local and the occurrence is in its scope. ''
#'' <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.
Here we will consider the CAP definition only, but our discussion will be supported by the ancillary definitions. Of course, the [http://www.ecma-international.org/publications/standards/Ecma-367.htm standard document] is available for download if you need to review the specific details.