What makes a Certified Attachment Pattern

A little background on CAPs

Certified Attachment Patterns (CAPs) were described in the section on void-safety tools. To review, a CAP is a code pattern for a certain expression, say exp of a detachable type that ensures that exp will never have a void run-time value within the covered scope.

A simple example is the familiar test for void reference: if l_x /= Void then l_x.do_something -- Valid for formal arguments, local variables, and stable attributes end We know that after the explicit check to make sure l_x is not Void, that the feature application l_x.do_something is void-safe. Of course, you should remember from previous discussions that l_x must be a local variable, a formal argument, or a 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 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 exp whose type is detachable is an occurrence of exp in one of the following contexts:

1. exp is an Object-Test Local and the occurrence is in its scope.

2. exp is a read-only entity and the occurrence is in the scope of a void test involving exp.

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 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 exp 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 attached syntax. attached x as l_x In the object test expression above, the identifier l_x is an Object-Test Local.

In the second context, the expression can be a read-only entity. Read-only entities are:

1. Constant attributes
2. Formal arguments
3. Object-Test Locals
4. Current

Additionally, the Eiffel Software compiler allows for 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: my_stable_string: detachable STRING note option: stable attribute endThe detachable attribute my_stable_string, 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, my_stable_string can be initialized later during the instance's life-cycle or not at all. But because it is detachable, my_stable_string 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:

if my_stable_string /= Void then my_stable_string.append ("abc") -- Valid ...

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 Void or some expression which could possibly be void.

So, for a local variable l_string, the following is valid: local l_string: detachable STRING do if l_string /= Void then l_string.append ("abc") -- Valid ...

But, if l_string had been a target of an assignment in which the source could possibly have been void, then it could no longer be guaranteed that l_string is not void. So, assuming that my_detachable_string is an attribute declared as type detachable STRING, the second application of append in this example would be invalid:

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 ...

Common CAPs

We've already seen the simple test for void as a CAP: local l_str: detachable STRING ... if l_str /= Void then l_str.append ("xyz") -- Valid end

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: local l_str: detachable STRING do create l_str.make_empty l_str.append ("xyz") -- Valid ...

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 and then: if x /= Void and not x.is_empty then -- Invalid ... if x /= Void and then not x.is_empty then -- Valid ...Assuming that x is CAP-able, the first line of code is invalid because the expression x.is_empty could always be evaluated even in the case in which x is void.

In the second line of code, the non-strict boolean is used, guaranteeing that x.is_empty will not be evaluated in cases in which x is void. Therefore, x.is_empty falls within the scope of the void test on x.

In contracts, multiple assertion clauses are treated as if they were separated by and then. This allows preconditions like the one in the following example:my_routine (l_str: detachable STRING) require l_str /= Void not l_str.is_empty -- Valid ...

Another not-so-obvious CAP is related to the use of the logical implication: local l_str: detachable STRING do if l_str /= Void implies some_expression then ... else l_str.append ("xyz") -- Valid end

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.