User Tools
eiffel:why:start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
eiffel:why:start [2021/02/09 16:19] jonathan [Why Eiffel?] |
eiffel:why:start [2021/02/09 21:20] (current) jonathan [Why Eiffel?] |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| * [[eiffel:why:petition:|Petition and Answers]] | * [[eiffel:why:petition:|Petition and Answers]] | ||
| - | * 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.)) | + | * **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 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. | + | * **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. |
| - | * **Seamlesness**: 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 | + | * **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 |
| ---- | ---- | ||
| Line 37: | Line 37: | ||
| 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. | 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. | * 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 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. | + | * 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. | * 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/start.1612887599.txt.gz · Last modified: 2021/02/09 16:19 by jonathan
Page Tools
