src/HOL/UNITY/Comp/README.html
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 51404 90a598019aeb
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <HTML>
     4 
     5 <HEAD>
     6   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     7   <TITLE>HOL/UNITY/README</TITLE>
     8 </HEAD>
     9 
    10 <BODY>
    11 
    12 <H2>UNITY: Examples Involving Program Composition</H2>
    13 
    14 <P>
    15 The directory presents verification examples involving program composition.
    16 They are mostly taken from the works of Chandy, Charpentier and Chandy.
    17 
    18 <UL>
    19 <LI>examples of <em>universal properties</em>:
    20 the counter (<A HREF="Counter.thy"><CODE>Counter.thy</CODE></A>)
    21 and priority system (<A HREF="Priority.thy"><CODE>Priority.thy</CODE></A>)
    22 
    23 <LI>the allocation system (<A HREF="Alloc.thy"><CODE>Alloc.thy</CODE></A>)
    24 
    25 <LI>client implementation (<A HREF="Client.thy"><CODE>Client.thy</CODE></A>)
    26 
    27 <LI>allocator implementation (<A HREF="AllocImpl.thy"><CODE>AllocImpl.thy</CODE></A>)
    28 
    29 <LI>the handshake protocol
    30 (<A HREF="Handshake.thy"><CODE>Handshake.thy</CODE></A>)
    31 
    32 <LI>the timer array (demonstrates arrays of processes)
    33 (<A HREF="TimerArray.thy"><CODE>TimerArray.thy</CODE></A>)
    34 </UL>
    35 
    36 <P> Safety proofs (invariants) are often proved automatically.  Progress
    37 proofs involving ENSURES can sometimes be proved automatically.  The
    38 level of automation appears to be about the same as in HOL-UNITY by Flemming
    39 Andersen et al.
    40 
    41 <ADDRESS>
    42 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    43 </ADDRESS>
    44 </BODY>
    45 </HTML>