equal
deleted
inserted
replaced
1 (* Title: HOL/BCV/DFA_Framework.thy |
1 (* Title: HOL/BCV/DFA_Framework.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 2000 TUM |
4 Copyright 2000 TUM |
5 |
|
6 The relationship between dataflow analysis and a welltyped-insruction predicate. |
|
7 *) |
5 *) |
8 |
6 |
9 header "Dataflow Analysis Framework" |
7 header "Dataflow Analysis Framework" |
10 |
8 |
11 theory DFA_Framework = Listn: |
9 theory DFA_Framework = Listn: |
|
10 |
|
11 text {* |
|
12 The relationship between dataflow analysis and a welltyped-insruction predicate. |
|
13 *} |
12 |
14 |
13 constdefs |
15 constdefs |
14 bounded :: "(nat => nat list) => nat => bool" |
16 bounded :: "(nat => nat list) => nat => bool" |
15 "bounded succs n == !p<n. !q:set(succs p). q<n" |
17 "bounded succs n == !p<n. !q:set(succs p). q<n" |
16 |
18 |