| products/sources/formale sprachen/Isabelle/HOL/UNITY/Simple/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: README.html Sprache: HTMLOriginal von: Isabelle© |
|
||||||||
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/
<HTML> <HEAD> <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> <TITLE>HOL/UNITY/README</TITLE> </HEAD> <BODY> <H2>UNITY: Examples Involving Single Programs</H2> <P> The directory presents verification examples that do not involve program composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'': <UL> <LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>) <LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>) <LI>the communication network (<A HREF="Network.thy"><CODE>Network.thy</CODE></A>) <LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>) <LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>) <LI><EM>n</EM>-process deadlock (<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>) <LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>) <LI>reachability in directed graphs (section 6.4 of the book) (<A HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and <A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>) </UL> <ADDRESS> <A NAME="[email protected]" HREF="mailto:[email protected]">[email protected]</A> </ADDRESS> </BODY> </HTML> ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.Bot Zugriff |
