section \<open>UNITY: Examples Involving Single Programs\<close>
text\<open>
The directory presents verification examples that do not involve program
composition. They are mostly taken from Misra's 1994 papers on ``New
UNITY'':
\<^item> common meeting time (\<^file>\<open>Common.thy\<close>) \<^item> the token ring (\<^file>\<open>Token.thy\<close>) \<^item> the communication network (\<^file>\<open>Network.thy\<close>) \<^item> the lift controller (a standard benchmark) (\<^file>\<open>Lift.thy\<close>) \<^item> a mutual exclusion algorithm (\<^file>\<open>Mutex.thy\<close>) \<^item> \<open>n\<close>-process deadlock (\<^file>\<open>Deadlock.thy\<close>) \<^item> unordered channel (\<^file>\<open>Channel.thy\<close>) \<^item> reachability in directed graphs (section 6.4 of the book)
(\<^file>\<open>Reach.thy\<close> and \<^file>\<open>Reachability.thy\<close>> \<close>
end
¤ Dauer der Verarbeitung: 0.0 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.
