UNITY: Examples Involving Program Composition

The directory presents verification examples involving program composition. They are mostly taken from the works of Chandy, Charpentier and Chandy.

• examples of universal properties: the counter (Counter.thy) and priority system (Priority.thy)
• the allocation system (Alloc.thy)
• client implementation (Client.thy)
• allocator implementation (AllocImpl.thy)
• the handshake protocol (Handshake.thy)
• the timer array (demonstrates arrays of processes) (TimerArray.thy)

Safety proofs (invariants) are often proved automatically. Progress proofs involving ENSURES can sometimes be proved automatically. The level of automation appears to be about the same as in HOL-UNITY by Flemming Andersen et al.