section \<open>UNITY: Examples Involving Program Composition\<close>
text\<open>
The directory presents verification examples involving program composition.
They are mostly taken from the works of Chandy, Charpentier and Chandy.
\<^item> examples of \<^emph>\<open>universal properties\<close>: the counter (\<^file>\<open>Counter.thy\<close>) and
priority system (\<^file>\<open>Priority.thy\<close>) \<^item> the allocation system (\<^file>\<open>Alloc.thy\<close>) \<^item> client implementation (\<^file>\<open>Client.thy\<close>) \<^item> allocator implementation (\<^file>\<open>AllocImpl.thy\<close>) \<^item> the handshake protocol (\<^file>\<open>Handshake.thy\<close>) \<^item> the timer array (demonstrates arrays of processes) (\<^file>\<open>TimerArray.thy\<close>)
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. \<close>
end
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
