| author | wenzelm |
| Sat, 08 Apr 2023 16:59:20 +0200 | |
| changeset 77786 | 3badbb7bc7ed |
| parent 75916 | b6589c8ccadd |
| permissions | -rw-r--r-- |
|
75916
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
1 |
theory README_Simple imports Main |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
2 |
begin |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
3 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
4 |
section \<open>UNITY: Examples Involving Single Programs\<close> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
5 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
6 |
text \<open> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
7 |
The directory presents verification examples that do not involve program |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
8 |
composition. They are mostly taken from Misra's 1994 papers on ``New |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
9 |
UNITY'': |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
10 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
11 |
\<^item> common meeting time (\<^file>\<open>Common.thy\<close>) |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
12 |
\<^item> the token ring (\<^file>\<open>Token.thy\<close>) |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
13 |
\<^item> the communication network (\<^file>\<open>Network.thy\<close>) |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
14 |
\<^item> the lift controller (a standard benchmark) (\<^file>\<open>Lift.thy\<close>) |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
15 |
\<^item> a mutual exclusion algorithm (\<^file>\<open>Mutex.thy\<close>) |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
16 |
\<^item> \<open>n\<close>-process deadlock (\<^file>\<open>Deadlock.thy\<close>) |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
17 |
\<^item> unordered channel (\<^file>\<open>Channel.thy\<close>) |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
18 |
\<^item> reachability in directed graphs (section 6.4 of the book) |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
19 |
(\<^file>\<open>Reach.thy\<close> and \<^file>\<open>Reachability.thy\<close>> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
20 |
\<close> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
21 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
22 |
end |