Design by Contract

P. Nienaltowski, B. Meyer, J. Ostroff: Contracts for concurrency, DOI 10.1007/s00165-007-0063-2, January 2008
The traditional correctness semantics of preconditions and postconditions is not suitable for concurrent programming. This article outlines a new semantics for preconditions and postconditions which applies equally well in concurrent and sequential contexts and permits a flexible use of contracts for specifying the mutual rights and obligations of clients and suppliers while preserving the potential for parallelism. We argue that the new semantics is a generalisation of the traditional correctness semantics. We also propose a proof technique for concurrent programs which supports proofs - similar to those for traditional non-concurrent programs - of partial correctness and loop termination in the presence of asynchrony.
Download the PDF

P. Nienaltowski: Flexible access control policy for SCOOP, DOI 10.1007/s00165-008-0072-9, February 2008
The contract-based SCOOP model enables the construction of object-oriented concurrent applications with little more effort than sequential ones. The model provides strong safety guarantees: mutual exclusion and atomicity at the routine level, and FIFO scheduling of clients' calls. Unfortunately, in the original proposal of the model these guarantees come at a high price: they entail locking all the arguments of a feature call; in most cases, the amount of locking is higher than necessary. We propose two refinements of the access control policy for SCOOP: a type-based mechanism to optimise locking, and a lock passing mechanism for safe handling of complex synchronisation scenarios with mutual locking of several separate objects. These refinements increase the expressive power of the model, give programmers more control over the computation, and enable more potential parallelism, thus reducing the risk of deadlock.
Download the PDF

Please note the above PDFs are pre-print versions. For more information please visit FACJ at or email info@praxis-his.com