This is an old revision of the document!

Lectures, Readings, and Exercises

General Notes

Touch of Class is available with online access via Steacie Library (you need your library account for this).
- You will be required to read extracts from the book (which you can get access to using your library login) on specific topics, but you may also want to read other relevant sections to understand the context better.
Under the heading of each week there is a Topics section. Use that for you to reflect on the materials and as a guidance to prepare for the tests and exam.

Section 4.6 of Touch of Class has a short introduction to contracts.
Sections 13.1 & 13.2 of Touch of Class has a short introduction to genericity.
Many video tutorials on the official Eiffel website
Two video introductions to Design by Contract part 1 part 2
A short video introduction to Eiffel Studio (link)

Requirements vs. Design vs. Implementation
What is design?
- Architecture
- Specification of behaviour
What are the criteria of good design?
- correct
- efficient
- maintainable
  - modular
  - stable interface
  - information hiding
Design by Contract
- precondition, postcondition, and class invariant
- the precondition of a feature is the obligation of its client but benefits of its supplier
- the postcondition of a feature is the benefits of its client but obligation of its supplier
Logic
- the notion that a predicate is weaker or stronger than another
- a precondition can be strengthened to disallow input values that will cause a class invariant violation upon executing the command (e.g., withdraw)
- a satisfactory precondition is derived from the class invariant
- a wrong implementation may pass through a postcondition that is too weak
- a postcondition can be strengthened to disallow improper updates on the state
Testing
- not to prove correctness, but to reveal bugs
- partition input domain into equivalence classes
Eiffel Studio
- create an empty project
- add the espec (Eiffel Specification) testing library
- at runtime,
  - before a feature's implementation body is executed, its precondition and the class invariant are checked;
  - then the implementation body is executed;
  - upon its termination, the postcondition and the class invariants are checked.

Void Safety
- My forum response on type checking, void checks at compile time and runtime, and how void safety is supported in EStudio
- A short introduction