Abstract: “Increasing effort in development of high quality distributed systems requires ground methodological base. Design by Contract approach looks very promising as a candidate since it helps to obtain component-wise specification and design, to separate concerns between developers, and makes development of high quality complex systems a manageable process. Unfortunately, in its classic form it can hardly be applied to distributed network applications because of lack of adequate means to describe asynchronous events. We extend Design by Contract with capabilities to describe callbacks and asynchronous communication between components and apply it to specify distributed software and to develop conformance test suites in automated manner. Specifications are developed in extensions of programming languages that makes them clear for industrial developers and decreases test construction effort. Practical results of numerous successful applications of the method are described.”
Since we’re on distributed systems (esp FoundationDB), I figured it was a good time to submit a low-cost verification technique for them. Design-by-Contract is flexible enough that many methods you might use in a custom language can be mapped onto the contracts. Previously, I’ve seen things like Rust borrow-checker and covert-channel analysis mapped onto SPARK Contracts. They do get more verbose but it at least works. This work uses events, callbacks, and asynchronous programming. Anyone wanting to experiment might try to pick a model in another concurrent or distributed language to see if they can map it to contracts.