A third ACM webinar this year (after two on agile methods): I will be providing a general introduction to Design by Contract. The date is this coming Thursday, September 17, and the time is noon New York (18 Paris/Zurich, 17 London, 9 Los Angeles, see here for hours elsewhere). Please tune in! The event is free but requires registration here.
Archive for the ‘Publication announcement’ Category.
Programming, wrote Dijkstra many years ago, is a branch of applied mathematics. That is only half of the picture: the other half is engineering, and this dual nature of programming is part of its attraction.
Descriptions of the mathematical side are generally, in my view, too complicated. This article  presents a mathematical theory of programs and programming based on concepts taught in high school: elementary set theory. The concepts covered include:
- Programming languages.
- Kinds of programs: imperative, functional, object-oriented.
- Concurrency (small-step and large-step)
- Control structures (compound, if-then-else and Dijkstra-style conditional, loop).
- State, store and environment.
- Notational conventions for building specifications and programs incrementally.
- Loop invariants and variants.
One of the principal ideas is that a program is simply the description of a mathematical relation. The program text is a rendering of that relation. As a consequence, one may construct programming languages simply as notations to express certain kinds of mathematics. This approach is the reverse of the usual one, where the program text and its programming languages are the starting point and the center of attention: theoreticians develop techniques to relate them to mathematical concepts. It is more effective to start from the mathematics (“unparsing” rather than parsing).
All the results (74 properties expressed formally, a number of others in the text) are derived as theorems from rules of elementary set theory; there are no new axioms whatsoever.
The paper also has a short version , omitting proofs and many details.
ACM is offering this coming Wednesday a one-hour webinar entitled Agile Methods: The Good, the Hype and the Ugly. It will air on February 18 at 1 PM New York time (10 AM West Coast, 18 London, 19 Paris, see here for more cities). The event is free and the registration link is here.
The presentation is based on my recent book with an almost identical title . It will be a general discussion of agile methods, analyzing both their impressive contributions to software engineering and their excesses, some of them truly damaging. It is often hard to separate the beneficial from the indifferent and the plain harmful, because most of the existing presentations are of the hagiographical kind, gushing in admiration of the sacred word. A bit of critical distance does not hurt.
As you can see from the Amazon page, the first readers (apart from a few dissenters, not a surprise for such a charged topic) have relished this unprejudiced, no-nonsense approach to the presentation of agile methods.
Another characteristic of the standard agile literature is that it exaggerates the contrast with classic software engineering. This slightly adolescent attitude is not helpful; in reality, many of the best agile ideas are the direct continuation of the best classic ideas, even when they correct or adapt them, a normal phenomenon in technology evolution. In the book I tried to re-place agile ideas in this long-term context, and the same spirit will also guide the webinar. Ideological debates are of little interest to software practitioners; what they need to know is what works and what does not.
Actually not that new: this paper  was published in August of last year. It is part of Christian Estler’s work for this PhD thesis, defended a few weeks ago, and was pursued in collaboration with Martin Nordio and Carlo Furia. It received the best paper award at the International Conference on Global Software Engineering; in fact this was the third time in a row that this group received the ICGSE award, so it must have learned a few things about collaborative development.
The topic is an issue that affects almost all software teams: how to make sure that people are aware of each other’s changes to a shared software base, in particular to avoid the dreaded case of a merge conflict: you and I are working on the same piece of code, but we find out too late, and we have to undergo the painful process of reconciling our conflicting changes.
The paper builds once again on the experience of our long-running “Distributed and Outsourced Software Engineering” course project, where students from geographically spread universities collaborate on a software development . It relies on data from 105 student developers making up twelve development teams located in different countries.
The usual reservations about using data from students apply, but the project is substantial and the conditions not entirely different from those of an industrial development.
The study measured the frequency and impact of merge conflicts, the effect of insufficient awareness (no one told me that you are working on the same module that I am currently modifying) and the consequences for the project: timeliness, developer morale, productivity.
Among the results: distribution does not matter that much (people are not necessarily better informed about their local co-workers’ developments than about remote collaborators); lack of awareness occurs more often than merge conflicts, and causes more damage.
 H-Christian Estler, Martin Nordio, Carlo A. Furia and Bertrand Meyer: Awareness and Merge Conflicts in Distributed Software Development, in proceedings of ICGSE 2014, 9th International Conference on Global Software Engineering, Shanghai, 18-21 August 2014, IEEE Computer Society Press (best paper award), see here.
 Distributed and Outsourced Software Engineering course and project, see here. (The text mentions “DOSE 2013” but the concepts remains applicable and it will be updated.)
Among the open problems of verification, particularly the verification of object-oriented programs, one of the most vexing is framing: how to specify and verify what programs element do not change. Continuing previous work, this article presents a “double frame inference” method, automatic on both sides the specification and verification sides. There is no need to write frame specifications: they will be inferred from routine postconditions. For verification, the method computes the set of actually changed properties through a “change calculus”, itself based on the previously developed alias calculus.
Some verification techniques, such as Hoare-style proofs, require significant annotation effort and potentially yield full functional verification; others, such as model checking and abstract interpretation, have more limited goals but seek full automation. Framing, in my opinion, should be automatic, freeing the programmer-verifier to devote the annotation effort to truly interesting properties.
 Bertrand Meyer: Framing the Frame Problem, in Dependable Software Systems, Proceedings of August 2014 Marktoberdorf summer school, eds. Alexander Pretschner, Manfred Broy and Maximilian Irlbeck, NATO Science for Peace and Security, Series D: Information and Communication Security, Springer, 2015 (to appear), pages 174-185; preprint available here.
To verify sequential programs, we have to prove that they do the right thing, but also that they do it within our lifetime — that they terminate. The termination problem is considerably harder with concurrent programs, since they add a new form of non-termination: deadlock. A set of concurrent processes or threads will deadlock if they end up each holding a resource that another wants and wanting a resource that another holds.
There is no general solution to the deadlock problem, even a good enough general solution. (“Good enough” is the best we can hope for, since like many important problems deadlock is undecidable.) It is already hard enough to provide run-time deadlock detection, to be able at least to cancel execution when deadlock happens. The research reported in this new paper  pursues the harder goal of static detection. It applies to an object-oriented context (specifically the SCOOP model of concurrent OO computation) and relies fundamentally on the alias calculus, a static alias analysis technique developed in previous publications.
The approach is at its inception and considerable work remains to be done. Still, the example handled by the paper is encouraging: analyzing two versions of the dining philosophers problem and proving — manually — that one can deadlock and the other cannot.
 Bertrand Meyer: An automatic technique for static deadlock prevention, in PSI 2014 (Ershov Informatics Conference), eds. Irina Virbitskaite and Andrei Voronkov, Lecture Notes in Computer Science, Springer, 2015, to appear.; draft available here.
The Paris computer science bookstore Le Monde en Tique is organizing, this coming Friday, Oct. 3, starting at 5 PM, a signing session for my book Agile! The Good, the Hype and the Ugly .
About the book (for readers new to this site): it provides a cold-blooded analysis of agile methods and examines their claims, their value and their limitations.
Le Monde en Tique is well known to technology aficionados in Paris and far beyond. Jean Demétreaux and his team established it at a time when it was hard, slow and expensive to order technical books from international publishers. While other legendary bookstores such a Stacey’s in San Francisco had to close in response to competition from chain stores and Internet offerings, le Monde en Tique (a pun on “tique” words such as informatics and bureautics, and also on ICT, in French TIC) has found new markets and lives on. It is set in a historic building in the medieval heart of Paris . They already organized such book signings for the publication of the French translation of Object-Oriented Software Construction  and of Touch of Class, the latter reported in this blog . If you are nearby, please come on Friday!
 Book signing announcement with access instructions: here.
 Bertrand Meyer: Conception et Programmation Orientées Objet (translation of Object-Oriented Software Construction, 2nd edition, Prentice Hall), Eyrolles, Paris 2008, book page here.
 Knuth and Company, article on this blog, 19 October 2009, see here.
A few years ago I became fascinated with agile methods: with the unique insights they include; with the obvious exaggerations and plainly wrong advice they also promote; and perhaps most of all with the constant intermingling of these two extremes.
I decided to play the game seriously: I read a good part of the agile literature, including all the important books; I sang the song, became a proud certified Scrum Master; I applied many agile techniques in my own work.
The book mentioned above is the result of that study and experience. It is both a tutorial and a critique.
The tutorial component was, I felt, badly needed. Most of the agile presentations I have seen are partisan texts, exhorting you to genuflect and adopt some agile method as the secret to a better life. Such preaching has a role but professionals know there is no magic in software development. Agile! describes the key agile ideas objectively, concretely, and as clearly as I could present them. It does not introduce them in a vacuum, like the many agile books that pretend software engineering did not exist before (except for a repulsive idea, the dreaded “waterfall”). Instead, it relates them to many other concepts and results of software engineering, to which they bring their own additions and improvements.
Unfortunately, not all the additions are improvements. Up to now, the field has largely been left (with the exception of Boehm’s and Turner’s 2005 “Guide for the Perplexed“) to propaganda pieces and adoring endorsements. I felt that software developers would benefit more from a reasoned critical analysis. All the more so that agile methods are a remarkable mix of the best and the worst; the book carefully weeds out — in the terminology of the title — the ugly from the hype and the truly good.
Software developers and managers need to know about the “ugly”: awful agile advice that is guaranteed to harm your project. The “hype” covers ideas that have been widely advertised as shining agile contributions but have little relevance to the core goals of software development. The reason it was so critical to identify agile ideas belonging to these two categories is that they detract from the “good”, some of it remarkably good. I would not have devoted a good part of the last five years to studying agile methods if I did not feel they included major contributions to software engineering. I also found that some of these contributions do not get, in the agile literature itself, the explanations and exposure they deserve; I made sure they got their due in the book. An example is the “closed-window rule”, a simple but truly brilliant idea, of immediate benefit to any project.
Software methodology is a difficult topic, on which we still have a lot to learn. I expect some healthy discussions, but I hope readers will appreciate the opportunity to discuss agile ideas in depth for the greater benefit of quality software development.
I also made a point of writing a book that (unlike my last two) is short: 190 pages, including preface, index and everything else.
The table of contents follows; more details and sample chapters can be found on the book page listed above.
1.6 A FIRST ASSESSMENT
Not new and not good
New and not good
Not new but good
New and good!
2 DECONSTRUCTING AGILE TEXTS
2.1 THE PLIGHT OF THE TRAVELING SEMINARIST
Proof by anecdote
When writing beats speaking
Discovering the gems
Agile texts: reader beware!
2.2 THE TOP SEVEN RHETORICAL TRAPS
Proof by anecdote
Slander by association
Postscript: you have been ill-served by the software industry!
&3 THE ENEMY: BIG UPFRONT ANYTHING
3.1 PREDICTIVE IS NOT WATERFALL
3.2 REQUIREMENTS ENGINEERING
Requirements engineering techniques
Agile criticism of upfront requirements
The waste criticism
The change criticism
The domain and the machine
3.3 ARCHITECTURE AND DESIGN
Is design separate from implementation?
Agile methods and design
3.4 LIFECYCLE MODELS
3.5 RATIONAL UNIFIED PROCESS
3.6 MATURITY MODELS
CMMI in plain English
The Personal Software Process
CMMI/PSP and agile methods
An agile maturity scale
4 AGILE PRINCIPLES
4.1 WHAT IS A PRINCIPLE?
4.2 THE OFFICIAL PRINCIPLES
4.3 A USABLE LIST
4.4 ORGANIZATIONAL PRINCIPLES
Put the customer at the center
Let the team self-organize
Maintain a sustainable pace
Develop minimal software
4.5 TECHNICAL PRINCIPLES
Treat tests as a key resource
Do not start any new development until all tests pass
Express requirements through scenarios
5 AGILE ROLES
5.2 PRODUCT OWNER
5.4 MEMBERS AND OBSERVERS
5.6 COACH, SCRUM MASTER
5.7 SEPARATING ROLES
6 AGILE PRACTICES: MANAGERIAL
The closed-window rule
Sprint: an assessment
6.2 DAILY MEETING
6.3 PLANNING GAME
6.4 PLANNING POKER
6.5 ONSITE CUSTOMER
6.6 OPEN SPACE
6.7 PROCESS MINIATURE
6.8 ITERATION PLANNING
6.9 REVIEW MEETING
6.11 SCRUM OF SCRUMS
6.12 COLLECTIVE CODE OWNERSHIP
The code ownership debate
Collective ownership and cross-functionality
7 AGILE PRACTICES: TECHNICAL
7.1 DAILY BUILD AND CONTINUOUS INTEGRATION
7.2 PAIR PROGRAMMING
Pair programming concepts
Pair programming versus mentoring
Pair programming: an assessment
7.3 CODING STANDARDS
The refactoring concept
Benefits and limits of refactoring
Incidental and essential changes
Combining a priori and a posteriori approaches
7.5 TEST-FIRST AND TEST-DRIVEN DEVELOPMENT
The TDD method of software development
An assessment of TFD and TDD
8 AGILE ARTIFACTS
8.3 USER STORIES
8.4 STORY POINTS
8.6 DEFINITION OF DONE
8.7 WORKING SPACE
8.8 PRODUCT BACKLOG, ITERATION BACKLOG
8.9 STORY CARD, TASK CARD
8.10 TASK AND STORY BOARDS
8.11 BURNDOWN AND BURNUP CHARTS
8.13 WASTE, TECHNICAL DEBT, DEPENDENCY, DEPENDENCY CHARTS
9 AGILE METHODS
9.1 METHODS AND METHODOLOGY
The fox and the hedgehog
9.2 LEAN SOFTWARE AND KANBAN
Lean Software’s Big Idea
Lean Software’s principles
Lean Software: an assessment
9.3 EXTREME PROGRAMMING
XP’s Big Idea
XP: the unadulterated source
Key XP techniques
Extreme Programming: an assessment
Scrum’s Big Idea
Key Scrum practices
Scrum: an assessment
Crystal’s Big Idea
Crystal: an assessment
10 DEALING WITH AGILE TEAMS
10.1 GRAVITY STILL HOLDS
10.2 THE EITHER-WHAT-OR-WHEN FALLACY
11 THE UGLY, THE HYPE AND THE GOOD: AN ASSESSMENT OF THE AGILE APPROACH
11.1 THE BAD AND THE UGLY
Deprecation of upfront tasks
User stories as a basis for requirements
Feature-based development and ignorance of dependencies
Rejection of dependency tracking tools
Rejection of traditional manager tasks
Rejection of upfront generalization
Coach as a separate role
Deprecation of documents
11.2 THE HYPED
11.3 THE GOOD
11.4 THE BRILLIANT
For almost anyone programming in Eiffel, contracts are just a standard part of daily life; Patrice Chalin’s pioneering study of a few years ago  confirmed this impression. A larger empirical study is now available to understand how developers actually use contracts when available. The study, to published at FM 2014  covers 21 programs, not just in Eiffel but also in JML and in Code Contracts for C#, totaling 830,000 lines of code, and following the program’s revision history for a grand total of 260 million lines of code over 7700 revisions. It analyzes in detail whether programmers use contracts, how they use them (in particular, which kinds, among preconditions, postconditions and invariants), how contracts evolve over time, and how inheritance interacts with contracts.
The paper is easy to read so I will refer you to it for the detailed conclusions, but one thing is clear: anyone who thinks contracts are for special development or special developers is completely off-track. In an environment supporting contracts, especially as a native part of the language, programmers understand their benefits and apply them as a matter of course.
 Patrice Chalin: Are practitioners writing contracts?, in Fault-Tolerant System, eds. Butler, Jones, Romanovsky, Troubitsyna, Springer LNCS, vol. 4157, pp. 100–113, 2006.
 H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni and Bertrand Meyer: Contracts in Practice, to appear in proceedings of 19th International Symposium on Formal Methods (FM 2014), Singapore, May 2014, draft available here.
The SCOOP concurrency model has a clear division of objects into “regions”, improving the clarity and reliability of concurrent programs by establishing a close correspondence between the object structure and the process structure. Each region has an associated “processor”, which executes operations on the region’s objects. A literal application of this rule implies, however, a severe performance penalty. As part of the work for his PhD thesis (defended two weeks ago), Benjamin Morandi found out that a mechanism for specifying certain processors as “passive” yields a considerable performance improvement. The paper, to be published at COORDINATION, describes the technique and its applications.
Benjamin Morandi, Sebastian Nanz and Bertrand Meyer: Safe and Efficient Data Sharing for Message-Passing Concurrency, to appear in proceedings of COORDINATION 2014, 16th International Conference on Coordination Models and Languages, Berlin, 3-6 June 2014, draft available here.
My book “Agile! The Good, the Hype and the Ugly” will be published in a few weeks by Springer. The announced date is April 30 and there is a preview Amazon page: here.
I have mentioned this paper before (see the earlier blog entry here) but it is now going to be published  and has been significantly revised, both to take referee comments into account and because we found better ways to present the concepts.
We have endeavored to explain better than in the draft why the concept of negative variable is necessary and why the usual techniques for modeling object-oriented programs do not work properly for the fundamental OO operation, qualified call x.r (…). These techniques are based on substitution and are simply unable to express certain properties (let alone verify them). The affected properties are those involving properties of the calling context or the global project structure.
The basic idea (repeated in part from the earlier post) is as follows. In modeling OO programs, we have to take into account the unique “general relativity” property of OO programming: all the operations you write are expressed relative to a “current object” which changes repeatedly during execution. More precisely at the start of a call x.r (…) and for the duration of that call the current object changes to whatever x denotes — but to determine that object we must again interpret x in the context of the previous current object. This raises a challenge for reasoning about programs; for example in a routine the notation f.some_reference, if f is a formal argument, refers to objects in the context of the calling object, and we cannot apply standard rules of substitution as in the non-OO style of handling calls.
We introduced a notion of negative variable to deal with this issue. During the execution of a call x.r (…) the negation of x , written x’, represents a back pointer to the calling object; negative variables are characterized by axiomatic properties such as x.x’= Current and x’.(old x)= Current.
The paper explains why this concept is necessary, describes the associated formal rules, and presents applications.
 Bertrand Meyer and Alexander Kogtenkov: Negative Variables and the Essence of Object-Oriented Programming, to appear in Specification, Algebra, and Software, eds. Shusaku Iida, Jose Meseguer and Kazuhiro Ogata, Springer Lecture Notes in Computer Science, 2014, to appear. See text here.
The following presentations from our ETH group in the ICSE week (International Conference on Software Engineering, San Francisco) address important issues of software specification and verification, describing new techniques that we have recently developed as part of our work building EVE, the Eiffel Verification Environment. One is at ICSE proper and the other at VSTTE (Verified Software: Tools, Theories, Experiments). If you are around please attend them.
Julian Tschannen will present Program Checking With Less Hassle, written with Carlo A. Furia, Martin Nordio and me, at VSTTE on May 17 in the 15:30-16:30 session (see here in the VSTTE program. The draft is available here. I will write a blog article about this work in the coming days.
Nadia Polikarpova will present What Good Are Strong Specifications?, written with , Carlo A. Furia, Yu Pei, Yi Wei and me at ICSE on May 22 in the 13:30-15:30 session (see here in the ICSE program). The draft is available here. I wrote about this paper in an earlier post: see here. It describes the systematic application of theory-based modeling to the full specification and verification of advanced software.
A core aspect of our verification work is the use of “strong” contracts, which express sophisticated specification properties without requiring a separate specification language: even for advanced properties, there is no need for a separate specification language, with special notations such as those of first-order logic; instead, one can continue to rely, in the tradition of Design by Contract, on the built-in notations of the programming language, Eiffel.
This is the idea of domain theory, as discussed in earlier posts on this blog, in particular . An early description of the approach, part of Bernd Schoeller’s PhD thesis work, was ; the next step was , presented at VSTTE in 2010.
A new paper to be presented at ICSE in May , part of an effort led by Nadia Polikarpova for her own thesis in progress, shows new advances in using strong specifications, demonstrating their expressive power and submitting them to empirical evaluation. The results show in particular that strong specifications justify the extra effort; in particular they enable automatic tests to find significantly more bugs.
A byproduct of this work is to show again the complementarity between various forms of verification, including not only proofs but (particularly in the contribution of two of the co-authors, Yi Wei and Yu Pei, as well as Carlo Furia) tests.
 Bertrand Meyer: Domain Theory: the forgotten step in program verification, article on this blog, see here.
 Bernd Schoeller, Tobias Widmer and Bertrand Meyer: Making Specifications Complete Through Models, in Architecting Systems with Trustworthy Components, eds. Ralf Reussner, Judith Stafford and Clemens Szyperski, Lecture Notes in Computer Science, Springer-Verlag, 2006, available here.
 Nadia Polikarpova, Carlo Furia and Bertrand Meyer: Specifying Reusable Components, in Verified Software: Theories, Tools, Experiments (VSTTE ‘ 10), Edinburgh, UK, 16-19 August 2010, Lecture Notes in Computer Science, Springer Verlag, 2010, available here.
 Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei and Bertrand Meyer: What Good Are Strong Specifications?, to appear in ICSE 2013 (Proceedings of 35th International Conference on Software Engineering), San Francisco, May 2013, draft available here.
As part of a Festschrift volume for Martin Glinz of the university of Zurich I wrote a paper  describing a general approach to requirements that I have been practicing and developing for a while, and presented in a couple of talks. The basic idea is to rely on object-oriented techniques, including contracts for the semantics, and to weave several levels of discourse: natural-language, formal and graphical.
 Bertrand Meyer: Multirequirements, to appear in Martin Glinz Festschrift, eds. Anne Koziolek and Norbert Scheyff, 2013, available here.
In modeling object-oriented programs, for purposes of verification (proofs) or merely for a better understanding, we are faced with the unique “general relativity” property of OO programming: all the operations you write (excluding non-OO mechanisms such as static functions) are expressed relative to a “current object” which changes repeatedly during execution. More precisely at the start of a call x.r (…) and for the duration of that call the current object changes to whatever x denotes — but to determine that object we must again interpret x in the context of the previous current object. This raises a challenge for reasoning about programs; for example in a routine the notation f.some_reference, if f is a formal argument, refers to objects in the context of the calling object, and we cannot apply standard rules of substitution as in the non-OO style of handling calls.
In earlier work [1, 2] initially motivated by the development of the Alias Calculus, I introduced a notion of negative variable to deal with this issue. During the execution of a call x.r (…) the negation of x , written x’, represents a back pointer to the calling object; negative variables are characterized by axiomatic properties such as x.x’= Current and x’.(old x)= Current. Alexander Kogtenkov has implemented these ideas and refined them.
In a recent paper under submission , we review the concepts and applications of negative variables.
 Bertrand Meyer: Steps Towards a Theory and Calculus of Aliasing, in International Journal of Software and Informatics, 2011, available here.
 Bertrand Meyer: Towards a Calculus of Object Programs, in Patterns, Programming and Everything, Judith Bishop Festschrift, eds. Karin Breitman and Nigel Horspool, Springer-Verlag, 2012, pages 91-128, available here.
 Bertrand Meyer and Alexander Kogtenkov: Negative Variables and the Essence of Object-Oriented Programming, submitted for publication, 2012. [Updated 13 January 2014: I have removed the link to the draft mentioned in this post since it is now superseded by the new version, soon to be published, and available here.]
Actually it is not a musical but an extensive survey. I have long been fascinated by the notion of loop invariant, which describes the essence of a loop. Considering a loop without its invariant is like conducting an orchestra without a score.
In this submitted survey paper written with Sergey Velder and Carlo Furia , we study loop invariants in depth and describe many algorithms from diverse areas of computer science through their invariants. For simplicity and clarity, the specification technique uses the Domain Theory technique described in an earlier article on this blog  (see also ). The invariants were verified mechanically using Boogie, a sign of how much more realistic verification technology has become in recent years.
The survey was a major effort (we worked on it for a year and a half); it is not perfect but we hope it will prove useful in the understanding, teaching and verification of important algorithms.
Here is the article’s abstract:
At the heart of every loop, and hence of all significant algorithms, lies a loop invariant: a property ensured by the initialization and maintained by every iteration so that, when combined with the exit condition, it yields the loop’s final effect. Identifying the invariant of every loop is not only a required step for software verification, but also a key requirement for understanding the loop and the program to which it belongs. The systematic study of loop invariants of important algorithms can, as a consequence, yield insights into the nature of software.
We performed this study over a wide range of fundamental algorithms from diverse areas of computer science. We analyze the patterns according to which invariants are derived from postconditions, propose a classification of invariants according to these patterns, and present its application to the algorithms reviewed. The discussion also shows the need for high-level specification and invariants based on “domain theory”. The included invariants and the corresponding algorithms have been mechanically verified using an automatic program prover. Along with the classification and applications, the conclusions include suggestions for automatic invariant inference and general techniques for model-based specification.
 Carlo Furia, Bertrand Meyer and Sergey Velder: Loop invariants: analysis, classification, and examples, submitted for publication, December 2012, draft available here.
 Domain Theory: the Forgotten Step in Program Verification, article from this blog, 11 April 2012, available here.
 Domain Theory: Precedents, article from this blog, 11 April 2012, available here