Contract Editor tool

Overview

As a rule, in EiffelStudio, class text can only be edited in the Editing tool, and then only when the Basic Text view is selected. The Contract Editing tool is an exception to this.

The Contract Editor tool gives you the ability to examine and edit class contracts in a context that is isolated from the full class text. In other words, when you use the Contract Editor tool, you see and edit the contracts without having to work around other elements of the software text such as implementation. For routines, you can edit pre- and postconditions, and for classes, you can edit class invariants. The tool provides views of inherited contracts as well as immediate ones.

Also included is a set of templates for creating common assertion patterns. By using these templates whenever possible, you add consistency to your class text.

You can target the Contract Editor tool by picking a routine name or class name and dropping it into the tool. Within the Contract Editor tool window, a single contract element is shown. A contract element here means either a precondition or a postcondition for a routine, or a class invariant for a class. Each assertion clause for a particular contract element is editable individually.

The Contract Editor tool can be helpful during analysis and design phases of development, when class specification is a primary concern.

Invoking the Contract Editor tool

If the Contract Editor tool is not currently visible, it can be made visible by following the menu path:

View --> Tools --> Contract Editor

Once visible, the tool can be docked to an appropriate location, if desired.

Toolbar

The Contract Editor toolbar contains the following items:

 Save modifications to the associated class. Becomes enabled when changes have been made to a contract. Clicking will cause changes to be saved.

 Add a new contract. Allows you to add a new contract assertion clause to the currently selected contract element (precondition, postcondition, or invariant). Clicking will provide a choice of creating from a template or creating a custom assertion clause. 

 Remove selected contract. Will delete the currently selected assertion clause from the contract element being edited.

 Edit selected contract. Will place the currently selected assertion clause in edit mode. Clauses can also be edited by double-clicking the clause itself, or right-clicking on a selected clause and choosing "Edit".

 and  Move selected contract up (or down). Use to move the selected assertion clause up or down in relation to the other clauses for this contract element.

 Refresh the current contracts to include any unsaved, undetected editor changes. EiffelStudio updates the Contract Editor tool display whenever class text is saved. However, if you edit a class in the Editing tool and have not saved it, there will be a difference between the Editing tool's display and the Contract Editor tool's display for the edited code. Clicking this icon will update the Contract Editor tool to include unsaved changes from the Editing tool.

 Select the type of contracts to edit. Use to select the contract element to edit. The name of the element (precondition, postcondition, or invariant) is listed to the right of the icon. If the Contract Editor tool is targeted to a routine, you can choose between Precondition and Postcondition by clicking this icon. If the tool is targeted to a class, then Invariant is selected and this icon is disabled in the toolbar.

 Show/hide the hidden contract place holders for inherited contracts. In addition to the assertion clauses that are coded immediately on the target routine or class, the Contract Editor tool also shows any assertion clauses inherited from a class's proper ancestor classes. These clauses are labeled with the name of the class from which they are inherited. By default, any classes in the inheritance graph which do not contribute clauses to a contract element are not shown. Toggling this icon down will show placeholders for these classes that are in the graph but do not contribute assertion clauses. Toggling the icon up will re-hide the placeholders.

 or  Show the callers of the currently edited feature. The icon shown here is dependent upon whether the tool is targeted to a routine or class. If the tool is targeted to a routine, then the icon shown will be the feature callers icon (). If the tool is targeted to a class, then the icon shown will be the class descendants icon (). In either case, clicking the icon does not effect the display in the Contract Editor tool. Rather, the action is shown in either the Feature tool (in the case of routines) or the Class tool (in the case of classes). 

Editing contracts

You edit contracts one assertion clause at a time. When you make a selection in the Contracts column of the Contract Editor tool, an entire assertion clause will be selected. In the depiction below, the clause minute_valid is selected from the class invariant of class TIME_OF_DAY.

This applies to multi-line assertion clauses, too, as shown below.

The selected clause can be moved up or down relative to the other clauses by using the up and down arrows in the toolbar.

To make changes to the text of the currently selected assertion clause, click the Edit button () on the toolbar, or just double-click the selected clause. The clause appears in the Edit Contract dialog box.

You can edit the tag for your assertion clause and the assertion itself.

Assertion clause tags must be valid identifiers. The Contract Editor tool will check your input as you type and alert you if entered a character string that would not be a valid identifier. The tag is optional, so you can leave it empty if you wish.

After editing the assertion clause itself, you can click OK. At this point the Contract Editor tool will perform a syntactical analysis on your assertion clause in order to help you avoid some types of errors. If your assertion clause appears syntactically sound, the Edit Contract dialog box will be dismissed and your changes will be visible in the Contract Editor tool display.

At this point, the changes have not been saved to the class text. To save the changes click the Save icon () in the toolbar.

Adding assertion clauses

You can add a new clause to any contract assertion by clicking the "Add" button () on the toolbar. The button provides two methods of creation "Custom" and "From Template".

Choosing "Add Custom..." produces a freeform dialog, much like the editing dialog show earlier in which you can edit an assertion clause from scratch:

"Add from Template" provides a list of code templates for commonly used assertion types. Adding assertion clauses from templates when possible speeds up class specification and helps to avoid errors. Consider a newly coded routine:

my_routine (a_string: STRING) -- Do something with `a_string`. do end

Part of the specification of this routine might be a precondition that states that the argument must be attached (i.e., not Void), and not the empty string. This precondition can be added to the feature by adding two assertion clauses from templates. To specify that a_string must be attached, you would first choose the template "Attached Contract" which provides this dialog:

This template focuses on the fact that some entity (expressed as var in the template) must be the object of an assertion clause that guarantees that the entity is attached. To have the template create such a clause for the argument a_string shown in the routine above, just replace var with a_string in the top text box of the dialog. The resulting code is updated automatically:

Adding a clause to specify that a_string must not be empty is done similarly, by selecting the "Not is empty" template. After adding these two precondition clauses, the routine now looks like this:

my_routine (a_string: STRING) -- My routine require a_string_attached: a_string /= Void not_a_string_is_empty: not a_string.is_empty do end