Software Engineering Documentation

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Why Eiffel? ======

  * [[:eiffel:why|Why Eiffel?]]
  * [[eiffel:why:petition:|Petition and Answers]]

  * **Specifications**: In design, the skill we wish to develop is the ability to distill a complex problem into its simplest components, and to organize the components into a cohesive and maintainable product. To do this well, we will need to construct abstractions (**specifications**) of data and computation above the code level to develop software products that are safe and fit for purpose. This is especially so in safety critical and mission critical systems. We will require (not just a good coding language) but a language and tool that also facilitates the expression of design above the code level.((See the video [[https://youtu.be/-4Yp3j_jk8Q|Leslie Lamport: Thinking Above the Code]] for the importance of specifications. Leslie Lamport is the winner of the Turing Award in 2013. He writes: Engineers and Architects draw detailed blueprints before a brick is laid or a nail is hammered. Programmers and software engineers seldom do. A blueprint for software is called a **specification**. The need for extremely rigorous specifications before coding complex or critical systems should be obvious—especially for concurrent and distributed systems. This talk explains why some sort of specification should be written for any software.)) 

  * **A Design Language/Tool**: This is where Eiffel the language, method and tool plays a role. It must not only be compared to programming languages such as Java, Golang and Rust. Like these languages, one may use Eiffel to code implementations. But it is also a tool that expresses design above the code level to produce products that can be demonstrated to be safe and fit for purpose. What tools are used in industry to express such designs? There are many (e.g. there is a proliferation of tools for expressing design via UML, statecharts and OCL). If comparisons are to be made -- then it must be to those tools that are used to express designs that are feasible and correct, having a cohesive and thus maintainable architecture.   

  * **Seamlessness**: Bertand Meyer developed the ideas of **Design** by Contract (DbC). He writes as follows. 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

----

====== Specifications and Design by Contract (DbC) ====

The following two videos discuss the importance of **Specifications** (and thus DbC) for rigorous **Engineering Design**. Recall that licensed engineers must demonstrate((It is not possible to formally prove correctness in real products using real compilers on real hardware; what we are looking for is evidence beyond that of testing.)) that their products are safe and fit for use.(([[https://en.wikipedia.org/wiki/Design_by_contract|Design by Contract]] was developed by Bertrand Meyer.)) See [[https://youtu.be/GMQMzk3DZug|here]] for the role of specifications in industry for mission critical systems. 

In the following two short introductory videos, our examples need to be very simple to grasp the underlying theory. We need to start with the simplest component before we start with the design and construction of more complex components. Although our examples must perforce be very simple for the purpose of illustration, Eiffel the language, the method and the tool -- scale up to the design of very large industrial strength systems. 



----

===== 01 What is Design?=====

Video is about 25 minutes. 

{{ :eiffel:why:01-what-is-design.pdf |01-What-Is-Design.pdf}}. And why DbC?

{{ :eiffel:why:01-what-is-design.mp4 |01 What is Design?}}. 


----
===== 02 Specification Mystery=====
Video is about 25 minutes. 

This video is a **very basic** introduction to Design By Contract (DbC). We present some simple "mystery code" and then show how a Specification (via DbC) is essential to unravel the mystery. 
  * With a Specification, we can document our understanding of the goal of the code. In this first step, we need to learn the skill of writing precise specifications (contracts). This is the main skill needed to use Eiffel the method and tool. The run-time will apply the necessary **theory** automatically to check the correctness of the design. 
  * In this video we also use this simple mystery example to discuss the underlying **mathematical theory** of program verification that Eiffel applies automatically, i.e. we can prove that a given implementation satisfies the specification (assuming the correctness of the compiler etc.). This theory was developed by Hoare and Dijkstra over 50 years ago at the foundations of software engineering. As in other engineering disciplines where we develop mathematical models to predict by calculation the behaviour of systems, Hoare logic is a theory that can be used to predict the behaviour of software systems. Is the system safe (e.g. by all its methods satisfying a class invariant)? Do its components terminate with the correct result where so required? In a reactive system are its safety and liveness properties satisfied in all executions?
  * After this video, you may want to try one more simple example to check your understanding. The Euclidean GCD algorithm is a relatively efficient method for computing the greatest common divisor of two integers, the largest number that divides them both without a remainder. See {{:eiffel:why:simple-dbc-gcd.pdf |here}} for the problem and a complete solution using Eiffel's DbC. Of course, it is understood that this function is provided in the base libraries of modern programming languages, so that there is no need for programmers to design this function. However, modern languages also provide canned search and sort functions; nevertheless, we study the design of such algorithms so as to understand the theory -- which can then be applied to new cases and applications where canned solutions are not available. 

{{ :eiffel:why:02-specification-mystery.pdf |02-Specification-Mystery.pdf}}.Slides. 


{{:eiffel:why:02-specification-mystery.mp4 |02 Specification Mystery}}

----
----

===== Out of Service Software Errors encountered during the 2020-21 Coronavirus Pandemic =====

Even non-mission critical software might be improved with more rigorous techniques beyond testing. 


{{:eiffel:why:td-out-of-service.jpeg?300|}}
{{:eiffel:why:bmo-out-of-service.jpg?300|}}
Software Engineering Documentation

User Tools

Site Tools

Page Tools
