isabelle: src/HOL/UNITY/Comp/README.html@49d7818e6161 (annotated)

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>

author	narboux
	Fri, 20 Apr 2007 14:30:35 +0200
changeset 22753	49d7818e6161
parent 15582	7219facb3fd0
child 51404	90a598019aeb
permissions	-rw-r--r--