22 ;;Quote: extend Hoare's assertions to concurrent programs by pre-conditions holding until termination of unit; equivalent for atomic actions

23 ;;Quote: want to prove safety properties (e.g., no incorrect output) and liveness properties (e.g., termination of program)

23 ;;Quote: to prove liveness properties such as termination need to prove safety properties such as monotonic decreases

24 ;;Quote: specify atomic operations for concurrent programs by angle brackets, e.g., ' := '

25 ;;Quote: in proofs of concurrent programs need to introduce value variables for intermediate results