equal
deleted
inserted
replaced
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
2 |
3 <!-- $Id$ --> |
3 <!-- $Id$ --> |
4 <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY> |
4 |
|
5 <HTML> |
|
6 |
|
7 <HEAD> |
|
8 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
9 <TITLE>HOL/UNITY/README</TITLE> |
|
10 </HEAD> |
|
11 |
|
12 <BODY> |
5 |
13 |
6 <H2>UNITY: Examples Involving Single Programs</H2> |
14 <H2>UNITY: Examples Involving Single Programs</H2> |
7 |
15 |
8 <P> The directory presents verification examples that do not involve program |
16 <P> The directory presents verification examples that do not involve program |
9 composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'': |
17 composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'': |
33 <P>Last modified on $Date$ |
41 <P>Last modified on $Date$ |
34 |
42 |
35 <ADDRESS> |
43 <ADDRESS> |
36 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
44 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
37 </ADDRESS> |
45 </ADDRESS> |
38 </BODY></HTML> |
46 </BODY> |
|
47 </HTML> |