EECS4090

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== EiffelCode Simple Mode Quick Demo (DbC) ======

====== EiffelCode Simple Mode Demo (Design by Contract) ======

  * [[https://youtu.be/eCVraeBKgiQ|Simple Mode Video]]
  * [[http://code.eecs.yorku.ca|Access the IDE in a browwser]] (EECS or Passport York Login required)

Below is a Demo of a Capstone Project by two students: Webapp for compiling/executing Eiffel programs with a selection of coding challenges illustrating Design by Contract.

<HTML>
<iframe width="560" height="315" src="https://www.youtube.com/embed/eCVraeBKgiQ" frameborder="0" allow="accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture" allowfullscreen></iframe>
</HTML>

The above video demos the simple mode, but there is also a project and tutorial mode. It is more challenging to develop a robust web-app of this kind than a desktop application. 

See [[:student:demo|More details of the student capstone features and design]]. 

===== Design by Contract =====

In Design by Contract (developed by Bertrand Meyer), a software component has a mathematical **specification** that describes **what** the the component must do (free of implementation detail) and an **implementation** (one of possibly many) that describes **how** the specification is implemented. 

For example, the specification of a  a square root function is described by a precondition (keyword **require**) and a postcondition (keyword **ensure**) as shown below. 

{{:demo:sqrt.png?600|}}

There are of course many different implementations that might satisfy this specification. 

A **contract** imposes obligations and benefits on the **client** (a component that uses the square root function) and the **supplier** (who must provide a body for the square root function).

{{:demo:contract.png?600|}}

A precondition failure is the fault of the client of the component. A postcondition failure is the fault of the supplier of the failure. 

Runtime assertion checking (in Eiffel) is used to check that the given implementation satisfies the specification.