Software engineering
A safe and stable solution
Reading about the latest hullabaloo around Android’s usage of Java, and more generally following the incessant flow of news about X suing Y in the software industry (with many combinations of X and Y) over Java and other object-oriented technologies, someone with an Eiffel perspective can only smile. Throughout its history, suggestions to use Eiffel … Read more
Specification explosion
To verify software, we must specify it; otherwise there is nothing to verify against. People often cite the burden of specification as the major obstacle toward making verification practical. At issue are not only the effort required to express the goals of software elements (their contracts) but also intermediate assertions, or “verification conditions”, including loop … Read more
Towards a Calculus of Object Programs
I posted here a draft of a new article, Towards a Calculus of Object Programs. Here is the abstract: Verifying properties of object-oriented software requires a method for handling references in a simple and intuitive way, closely related to how O-O programmers reason about their programs. The method presented here, a Calculus of Object Programs, … Read more
If I’m not pure, at least my functions are
It is often suggested that the programming language should support specifying that a routine is pure; many people have indeed proposed the addition of a keyword such as pure to Eiffel. One of the reasons this is not — in my opinion — such a great idea is that purity is just a special case of the more general problem of framing: specifying and verifying what a routine does not change. If we can specify an arbitrary frame property, then we can, as a special case covered by the general mechanism, specify that a routine changes nothing. The language solution is simple: no routine may change the value of a query other than those specified in its postcondition
Assessing concurrency models
In a recent experiment with students we wanted to know how the SCOOP concurrency model compares to Java Threads in terms of ease of learning, program readability and correctness. Our group, however, is heavily involved with SCOOP. How did we address the risk of bias, and other parts of the “Professor Smith Syndrome”? What are our results, and can you believe them?