Lambda the Ultimate

(seen via G. Meredith on the Scala list.)

a paper on new DbC thoughts.

Abstract. The approach known as Design by Contract (DbC) promotes reliable
software development through elaboration of type signatures for sequential programs
with logical formulae. This paper presents an assertion method which generalises the
notion of DbC to multiparty distributed interactions, enabling the specification and ver-
ification of distributed multiparty protocols, based on the π-calculus with full recursion.
Centring on the notion of global assertions and their projections onto endpoint asser-
tions, our method allows fully general specifications for typed sessions with session
channel passing, constraining the content of the exchanged messages, the choice of sub-
conversations to follow, and invariants on recursions. The paper presents key theoretical
foundations of this framework, including a validation algorithm for consistency of global
assertions and a sound and relatively complete compositional proof system for verifying
a large class of processes against assertions.

as if i'm going to grok 10% of it... but maybe it is good exercise for my grey matter.