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/Comp/README.html
author huffman
Tue, 11 May 2010 19:01:35 -0700
changeset 36841 02df88789641
parent 15582 7219facb3fd0
child 51404 90a598019aeb
permissions -rw-r--r--
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 11194
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: 11194
diff changeset 
     2
 







11194






ea13ff5a26d1
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>








11194






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



paulson


parents: 

diff
changeset




    13














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



paulson


parents: 

diff
changeset




    14


<H2>UNITY: Examples Involving Program Composition</H2>













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



paulson


parents: 

diff
changeset




    15














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



paulson


parents: 

diff
changeset




    16


<P>













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



paulson


parents: 

diff
changeset




    17


The directory presents verification examples involving program composition.













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



paulson


parents: 

diff
changeset




    18


They are mostly taken from the works of Chandy, Charpentier and Chandy.













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



paulson


parents: 

diff
changeset




    19














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



paulson


parents: 

diff
changeset




    20


<UL>













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



paulson


parents: 

diff
changeset




    21


<LI>examples of <em>universal properties</em>:













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



paulson


parents: 

diff
changeset




    22


the counter (<A HREF="Counter.thy"><CODE>Counter.thy</CODE></A>)













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



paulson


parents: 

diff
changeset




    23


and priority system (<A HREF="Priority.thy"><CODE>Priority.thy</CODE></A>)













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



paulson


parents: 

diff
changeset




    24














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



paulson


parents: 

diff
changeset




    25


<LI>the allocation system (<A HREF="Alloc.thy"><CODE>Alloc.thy</CODE></A>)













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



paulson


parents: 

diff
changeset




    26














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



paulson


parents: 

diff
changeset




    27


<LI>client implementation (<A HREF="Client.thy"><CODE>Client.thy</CODE></A>)













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



paulson


parents: 

diff
changeset




    28














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



paulson


parents: 

diff
changeset




    29


<LI>allocator implementation (<A HREF="AllocImpl.thy"><CODE>AllocImpl.thy</CODE></A>)













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



paulson


parents: 

diff
changeset




    30














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



paulson


parents: 

diff
changeset




    31


<LI>the handshake protocol













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



paulson


parents: 

diff
changeset




    32


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













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



paulson


parents: 

diff
changeset




    33














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



paulson


parents: 

diff
changeset




    34


<LI>the timer array (demonstrates arrays of processes)













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



paulson


parents: 

diff
changeset




    35


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













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



paulson


parents: 

diff
changeset




    36


</UL>













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



paulson


parents: 

diff
changeset




    37














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



paulson


parents: 

diff
changeset




    38


<P> Safety proofs (invariants) are often proved automatically.  Progress













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



paulson


parents: 

diff
changeset




    39


proofs involving ENSURES can sometimes be proved automatically.  The













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



paulson


parents: 

diff
changeset




    40


level of automation appears to be about the same as in HOL-UNITY by Flemming













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



paulson


parents: 

diff
changeset




    41


Andersen et al.













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



paulson


parents: 

diff
changeset




    42














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



paulson


parents: 

diff
changeset




    43


<HR>













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



paulson


parents: 

diff
changeset




    44


<P>Last modified on $Date$













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



paulson


parents: 

diff
changeset




    45














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



paulson


parents: 

diff
changeset




    46


<ADDRESS>













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



paulson


parents: 

diff
changeset




    47


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













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



paulson


parents: 

diff
changeset




    48


</ADDRESS>








15582






7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




    49


</BODY>













7219facb3fd0
HTML 4.01 Transitional conformity



webertj


parents: 
15283

diff
changeset




    50


</HTML>















isabelle