Quelle  README_Comp.thy   Sprache: Isabelle

theory README_Comp imports Main
begin

section ‹UNITY: Examples Involving Program Composition›

text ‹
  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.
›

end