Why do we use Eiffel in EECS3311, software design?

• Because Eiffel the language, Eiffel the method and Eiffel the tool encourage thinking above the code level at the design level.
• The Eiffel IDE in particular is not just a tool that is used for large scale software development ¹⁾, it is also a tool for model driven engineering with good support for seamless round trip engineering between models (“blueprints”) and code. See https://ieeexplore.ieee.org/document/8501488.

• Specifications vs. Implementations: Design by Contract
  • Preconditions, postconditions, class invariants for specifying classes as abstract data types,
  • Subcontracting for the correct use of inheritance via the Liskov substitutability principle
  • Loop variants and invariants for checking the correctness of implemented features
  • Ordinary Unit Testing and Specification Tests
• Design level constructs such as true multiple inheritance (as supported by UML)
• Seamless round trip engineering between BON/UML models and code.

The Eiffel method is used throughout the design principles taught (and evaluated via labs, network secure labtests and a project) in EEC3311.

Fig 1: Design Principles

OO Basics is assumed. The course covers the topics in the orange box labelled “Design”, interleaved with a variety of Design Patterns that illustrate those principles. Specifications are implicated in every principle in the orange “Design” box. The design principles are needed for a solid understanding of the design patterns. For example, a core information hiding idea (stressed in the course) used in many patterns is:

Remove the part of the software that changes and encapsulate it elsewhere so that changes to it do not overflow and pollute the part that does not change. [Now when you encapsulate a component, that component will need a good API, and a good API must be properly specified.]

The course has weekly labs, and a project (with two phases) with an open-ended design problem. All designs must be shown to be feasible and correct via unit and acceptance testing, and students must produce software design documents (see below) for the project and some of the labs.

• A key design skill is the ability to decomposes a complex system into simpler components (or modules), and the organization of those components into a cohesive, robust and maintainable product.
• This requires a good architecture (how the components interact with each other) as well as a specification of the component API that describes how the component must behave, free of implementation detail.
• A good specification allows developers to choose different implementations and for a check of the correctness of the chosen implementation against the specification. Obviously, a design that is not correct is not a good design.

Fig. 2: An example of the use of contracts

class MATH feature
       max_precision: REAL_64 = 1.0e-14
			-- 14 significant digits
 
       min_precision: REAL_64 = 0.01
			-- 2 significant digits
 
       epsilon: REAL_64
 
	sqrt(x: REAL_64): REAL_64
                  -- return the square root of `x`
                  -- with precision epsilon
		require
			non_negative: x >= 0
		do
			-- some implementation goes here
                        -- e.g try Bisection, Secant and Newton-Rhapson
                        -- evaluate w.r.t correctness and efficiency
		ensure
			result_accurate:
				(Result * Result - x).abs <= Result*epsilon
			epsilon_unchanged:
				epsilon = old epsilon
		end
 
          ...
invariant
	max_constraint: Max_precision <= epsilon
	min_precision: epsilon <= Min_precision
end

In the above example we see program text (the class MATH) that includes specifications of its features and their implementations. For example, the query sqrt has a precondition (require clause) and a postcondition (ensure clause). The implementation is the body of the routine between the do and ensure keywords. There is also a class invariant that must be preserved by all routines (queries and commands) of the class. These contracts impose obligations between a client using the class and the supplier of the class.

Suppose a client module calls sqrt(-200.42), i.e. with a negative number. Then the client has violated their obligation, and the IDE will flag this as a precondition violation. Thus every client must first demonstrate that the precondition is satisfied before calling the function. The benefit to the client is that the supplier (the designer of modulo MATH) must demonstrate the correctness of the postcondition. This is called design by contract. All modules must interact with each other in accordance with the contracts, for the design to be correct. In the contract view of the program text we see only the contracts not the implementations.

Seamless model driven engineering: The worldview underlying the Eiffel method is treating the whole process of software development as a continuum; unifying the concepts behind activities such as requirements, specification, design, implementation, verification, maintenance and evolution; and working to resolve the remaining differences, rather than magnifying them. Anyone who has worked in both specification and programming knows how similar the issues are. Formal specification languages look remarkably like programming languages; to be usable for significant applications they must meet the same challenges: defining a coherent type system, supporting abstraction, providing good syntax (clear to human readers and parsable by tools), specifying the semantics, offering modular structures, allowing evolution while ensuring compatibility. The same kinds of ideas, such as an object-oriented structure, help on both sides. Eiffel as a language is the notation that attempts to support this seamless, continuous process, providing tools to express both abstract specifications and detailed implementations. Lampsort, Bertrand Meyer, 2014.

Design in EEC3311 is open-ended, i.e. there are an unbounded number of solutions. Many of these solutions might be bad, and only some might be good. A student earns a grade by providing evidence in their SDD that justifies the grade. The rubric for design documents is as follows:

The project encourages students to synthesize the various principles including the feasibility and correctness of design and the architecture of design. The correctness assessment is performed via a number of automated regression tests(unit and acceptance). The software design document describes the organization of the classes. An outline of the sections in the SDD are as follows:

• Software product requirements
• Top level Architecture of the product (e.g. class diagrams and sequence diagrams)
• Information hiding: Table of modules with a description of the responsibility and secret of each module (class) .
• Expanded description justifying the main design decisions
• Correctness: description of the significant contracts
• Summary of testing procedures (unit testing and acceptance testing)

The IDE can generate BON or UML class diagrams. Below is a BON class diagram showing multiple inheritance in the composite design pattern.

The double green arrows represent client-supplier relations (associations) between classes, and the single red arrows represent inheritance.

The “capstone” of the course is a project (usually with a team of 2 students) in two phases (in the second phase, more features are added). Below is one of the BON class diagrams produced by a team (taken from their software design document). This 3rd-year course is usually the first time most students design software with many classes (typically 15-20 classes are needed for a modular design).

Ada and Eiffel provide native language support for Design by Contract, but the principle that specifications are integral to design carries over to designing in any language. The Unified Modeling Language (UML) is the de facto modelling language in software engineering thus supports Design by Contract in the form of OCL (Object Constraint Language). For other methods of specification, see Video: Thinking Above the Code and the video below for Specifications in Industry at Amazon, Google and Facebook.