Assertional and Behavioral approaches to concurrency
Uri Abraham, he Concurrency Column by Luca Aceto · Bulletin of the European Association for Theoretical Computer Science · 2011
We compare two proofs of the mutual-exclusion property of the well known critical section algorithm of Peterson: an assertional proof and a behavioral one. The accepted view is that behavioral proofs are informal and are, for some intrinsic reason, error prone. We try to present a different view and to outline a framework within which the behavioral approach can be formalized in a way that keeps the intuitive content of the behavioral reasoning.