|
5111
|
1 |
(* Title: HOL/UNITY/Traces
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1998 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Inductive definitions of
|
|
|
7 |
* traces: the possible execution traces
|
|
|
8 |
* reachable: the set of reachable states
|
|
|
9 |
*)
|
|
|
10 |
|
|
4776
|
11 |
Traces = UNITY +
|
|
|
12 |
|
|
5111
|
13 |
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
|
|
4776
|
14 |
|
|
5111
|
15 |
(*Initial states and program => (final state, reversed trace to it)...
|
|
|
16 |
Arguments MUST be curried in an inductive definition*)
|
|
|
17 |
|
|
|
18 |
inductive "traces Init Acts"
|
|
4776
|
19 |
intrs
|
|
|
20 |
(*Initial trace is empty*)
|
|
5111
|
21 |
Init "s: Init ==> (s,[]) : traces Init Acts"
|
|
4776
|
22 |
|
|
5111
|
23 |
Acts "[| act: Acts; (s,evs) : traces Init Acts; (s,s'): act |]
|
|
|
24 |
==> (s', s#evs) : traces Init Acts"
|
|
4776
|
25 |
|
|
|
26 |
|
|
5111
|
27 |
constdefs reachable :: "'a set * ('a * 'a)set set => 'a set"
|
|
|
28 |
"reachable == %(Init,Acts). {s. EX evs. (s,evs): traces Init Acts}"
|
|
4776
|
29 |
|
|
|
30 |
end
|