Attached types
Contents
Introduction
Attached types are introduced in the language by the ECMA/ISO standard to get rid of a common program error caused by a call of a feature on a Void target. The existing code base cannot be changed overnight to follow the new safety standards. Therefore there is a task to perform the smooth transition from non-void-safe code to void-safe code. This can be done by systematic application of the following steps:
- Identification. The code is analyzed to find some common patterns that assume that the target of the feature call is not void. They can be explicit, such as
require a /= Void
as well as implicit, such as
a.f
- Selection. Usually there is more than one way to change the existing code to make it void-safe. The correct replacement depends on the semantics of the piece of code and may rely on expert knowledge of a user. But there are still many "common" cases that require the same kind of modification which allows for automation of the process.
- Modification. After selection among the possible variants is completed, the actual code modification is performed. In order to avoid breaking all the code, the backup of the original as well as a journal of the changes can be kept.
The steps above can be performed manually, semi-automatically or automatically. The sections below discuss the variants that involve the tools to automate the transition to void-safe code.
Suggested Attachment Pattern (SAP)
Suggested Attachment Pattern (SAP) in non-void-safe code is similar to Certified Attachment Pattern (CAP) in void-safe code. Moreover, SAP is a superset of CAP, i.e. it includes all CAP code snippets as well as some other variants. SAP stands for the code patterns that expect that there is no feature calls on void target if they themselves do not trigger any exception. The most simple SAP includes the condition x /= Void
. In this case the type of x
can be declared to be attached, so that the condition can be optimized by substituting the value True
, or non-attached, so that the condition is not affected.
SAP |
---|
require x /= Void
|
ensure x /= Void
|
invariant x /= Void
|
Suggested Replacement Pattern (SRP)
Consider the following code snippet:
f (a: A) require a /= Void do ... a.g ... end
The precondition that states that the argument a
should not be Void
can be revised in the void-safe context in different ways. From the first sight it looks like the type of a
should be A (attached). However the source code can be modified in different ways depending on the required behavior of the feature f
:
- (default) Remove the precondition subclause
a /= Void
altogether, leaving typeA
attached (an explicit syntax!A
was proposed for transitional period). - Use type
?A
instead ofA
and leave the precondition subclause. - Don't change anything.
In other words every SAP is associated with one or more Suggested Replacement Patterns (SRP). The number and the kind of SRPs depends on the SAP. For example, a test for voidness in the precondition does not automatically mean that the argument should be of an attached type, because it can be relaxed in a descendant by the feature redeclaration. On the other hand, for the test that the function Result
is not void, specified in a postcondition, it is usually safe to assume that the returning type is attached, because the postcondition cannot be made weaker in a descendant.
Automation
The process of applying SRP for SAP can be automated. It can be integrated into EiffelStudio or run as a separate tool. The following actions can be provided:
- List all suggested replacements. The variants of this facility include:
- display the list on the screen
- log it to a file
- prepare a check list for further analysis by a user
- Make suggested replacements asking each time
- interactively
- by using a check list mentioned in the previous point
- Make suggested replacements automatically without human intervention
- perform all possible replacements
- perform replacements only for the selected SAPs
Void-safety levels
The compiler can be instructed to apply void safety rules on different scopes:
- system/library
- cluster
- class
This is achieved by the appropriate configuration options. In practice, a single system might use clusters with different settings for void safety. Then additional care should be taken on the boundaries to avoid compromizing void-safe classes by non-void-safe ones.
The compiler options also allow to control the level of the void safety checks:
Level | Are attachment properties checked at | |
compile-time? | run-time? | |
Compatibility mode | no | yes (workbench) / no (finalized) |
---|---|---|
Dynamic safety | yes, if possible | yes, unless proven at compile-time |
Static safety | yes (error unless proven) | no |