Proof-Outline Logic (Concurrent Programming Edition)
Theodore S. Norvell · 2014
An introduction to proof outlines, compiled as background reading for Engi 8893 Concurrent Programming and Engi 9869 Advanced Concurrent Programming. Note on editions: This is the Concurrent Programming edition, designed to support MUN courses Engi-7893 and Engi-9869. The first part of this note –the part up to the section entitled Concurrent Programming– also appears in an edition for MUN course Engi-6892 Algorithms: Correctness and Complexity. The content is the same, but the notation is a bit different. The notation used in this edition better matches the notation used in Andrews’ text book [Andrews, 2000]. [For students who took Engi6892 in 2013 or earlier: since earlier editions of this note and the edition for Engi-6892 I’ve made the following changes in terminology. I formerly said that a condition was “valid” where I now say it is “universally true”. And I formally said that a Hoare triple or a proof outline was “valid” where I now say it is “partially correct”.]