Software correctness

blog Why Type-safety?

schoelle's picture

The search for a type-safe version of Eiffel is a never-ending story in the development of the Eiffel language. Recently, Helmuth Brandl has created a series of blog entries with a nice description of is needed to make Eiffel type-safe. There have been others posting blog entries (including me) and it also had been a constant topic during the ECMA process of Eiffel standardization.

Interestingly, a question that was seldom raised was: why do we need type-safety? As absurd as it seems for all the mathematicians to raise this question, the Eiffel community has understood for a long time that mathematical soundness is not a reason in itself. Instead, it serves a purpose in the enterprise of language design: giving software developers means to express themselves in ways that reduce the number of defects in his/her programs and enable him/her to master complex problems he/she would not be able to master without.

blog Correctness conditions (2) for calling an agent

colin-adams's picture

Following on from correctness_conditions_for_calling_an_agent, I have thought about the following scheme (it would require ECMA to be amended to require a tag on assertions, but this should be done anyway.

blog Correctness conditions for calling an agent

colin-adams's picture

I was recently reading the paper "From Design Patterns to Reusable Components: The Factory Library by Karine Arnout and Bertrand Meyer" and I noticed that although they had succeeded in turning the pattern "Abstract Factory" into a component, the resulting class (ABSTRACT_FACTORY) did not have a sound contract.

Syndicate content