Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/Simple/README.html
author paulson
Wed, 04 Jul 2007 13:56:26 +0200
changeset 23563 42f2f90b51a6
parent 15582 7219facb3fd0
child 51404 90a598019aeb
permissions -rw-r--r--
simplified a proof
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 11195
diff changeset 
     1
 
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added
webertj
parents: 11195
diff changeset 
     2
 







11195






65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




     3


<!-- $Id$ -->








15582






7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




     4














7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




     5


<HTML>













7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




     6














7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




     7


<HEAD>













7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




     8


  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">













7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




     9


  <TITLE>HOL/UNITY/README</TITLE>













7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




    10


</HEAD>













7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




    11














7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




    12


<BODY>








11195






65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    13














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    14


<H2>UNITY: Examples Involving Single Programs</H2>













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    15














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    16


<P> The directory presents verification examples that do not involve program













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    17


composition.  They are mostly taken from Misra's 1994 papers on ``New UNITY'':













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    18


<UL>













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    19


<LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>)













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    20














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    21


<LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>)













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    22














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    23


<LI>the communication network













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    24


(<A HREF="Network.thy"><CODE>Network.thy</CODE></A>)













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    25














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    26


<LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>)













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    27














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    28


<LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>)













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    29














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    30


<LI><EM>n</EM>-process deadlock













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    31


(<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>)













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    32














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    33


<LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>)













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    34














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    35


<LI>reachability in directed graphs (section 6.4 of the book) (<A













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    36


HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    37


<A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>)













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    38


</UL>













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    39














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    40


<HR>













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    41


<P>Last modified on $Date$













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    42














65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    43


<ADDRESS>













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    44


<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>













65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp



paulson


parents: 

diff
changeset




    45


</ADDRESS>








15582






7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




    46


</BODY>













7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




    47


</HTML>















isabelle