New LASER proceedings






Springer has just published in the tutorial sub-series of Lecture Notes in Computer Science a new proceedings volume for the LASER summer school [1]. The five chapters are notes from the 2008, 2009 and 2010 schools (a previous volume [2] covered earlier schools). The themes range over search-based software engineering (Mark Harman and colleagues), replication … Read more




Ado About The Resource That Was (Not)






The resources we have at our disposal on a computing system may be huge, but they are always finite, and our programs’ appetite for resources will eventually exhaust them. At that stage, we have to deal with the SBYBAW rule, which sounds like a tautology but is an encouragement to look for clever algorithms: techniques for freeing resources when no resources remain may not request new resources.







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







Agile methods: the good, the bad and the ugly






Agile methods are wonderful. They’ll give you software in no time at all, turn your customers and users into friends, catch bugs before they catch you, change the world, and boost your love life.







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?







Publish no loop without its invariant






There may be no more blatant example of the disconnect between the software engineering community and the practice of programming than the lack of widespread recognition for the fundamental role of loop invariants.