author | nipkow |
Sat, 28 Apr 2012 07:38:22 +0200 | |
changeset 47818 | 151d137f1095 |
parent 46233 | f23dc7d16c0b |
permissions | -rw-r--r-- |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
1 |
theory Collecting_list |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
2 |
imports ACom |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
3 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
4 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
5 |
subsection "Executable Collecting Semantics on lists" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
6 |
|
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
7 |
fun step :: "state list \<Rightarrow> state list acom \<Rightarrow> state list acom" where |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
8 |
"step S (SKIP {P}) = (SKIP {S})" | |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
9 |
"step S (x ::= e {P}) = |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
10 |
(x ::= e {[s(x := aval e s). s \<leftarrow> S]})" | |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
11 |
"step S (c1; c2) = step S c1; step (post c1) c2" | |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
12 |
"step S (IF b THEN c1 ELSE c2 {P}) = |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
13 |
IF b THEN step [s \<leftarrow> S. bval b s] c1 ELSE step [s\<leftarrow>S. \<not> bval b s] c2 |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
14 |
{post c1 @ post c2}" | |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
15 |
"step S ({Inv} WHILE b DO c {P}) = |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
16 |
{S @ post c} WHILE b DO (step [s\<leftarrow>Inv. bval b s] c) {[s\<leftarrow>Inv. \<not> bval b s]}" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
17 |
|
46233 | 18 |
|
19 |
text{* Examples: *} |
|
20 |
||
21 |
definition "c = WHILE Less (V ''x'') (N 3) |
|
22 |
DO ''x'' ::= Plus (V ''x'') (N 2)" |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
23 |
definition "c0 = anno [] c" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
24 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
25 |
definition "show_acom xs = map_acom (map (show_state xs))" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
26 |
|
46233 | 27 |
|
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
28 |
text{* Collecting semantics: *} |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
29 |
|
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
30 |
value "show_acom [''x''] (((step [<>]) ^^ 6) c0)" |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
31 |
|
46233 | 32 |
|
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
33 |
text{* Small step semantics: *} |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
34 |
|
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
35 |
value "show_acom [''x''] (((step []) ^^ 5) (step [<>] c0))" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
36 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
37 |
end |