NameDateSize

..25-Jul-201927

Alloc.thyH A D25-Jul-201939 KiB

AllocBase.thyH A D25-Jul-20192.7 KiB

AllocImpl.thyH A D25-Jul-201914.3 KiB

Client.thyH A D25-Jul-20198.3 KiB

Counter.thyH A D25-Jul-20193.4 KiB

Counterc.thyH A D25-Jul-20193.7 KiB

Handshake.thyH A D25-Jul-20192.3 KiB

Priority.thyH A D25-Jul-20199.3 KiB

PriorityAux.thyH A D25-Jul-20194.9 KiB

Progress.thyH A D25-Jul-20193.4 KiB

README.htmlH A D25-Jul-20191.4 KiB

TimerArray.thyH A D25-Jul-20192.2 KiB

README.html

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>
15The directory presents verification examples involving program composition.
16They are mostly taken from the works of Chandy, Charpentier and Chandy.
17
18<UL>
19<LI>examples of <em>universal properties</em>:
20the counter (<A HREF="Counter.thy"><CODE>Counter.thy</CODE></A>)
21and 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
37proofs involving ENSURES can sometimes be proved automatically.  The
38level of automation appears to be about the same as in HOL-UNITY by Flemming
39Andersen 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>
46