13 "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com" ("(2_ :=/ _)" [70, 65] 61) |
13 "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com" ("(2_ :=/ _)" [70, 65] 61) |
14 "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(_;/ _)" [61,60] 60) |
14 "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(_;/ _)" [61,60] 60) |
15 "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) |
15 "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) |
16 "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) |
16 "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) |
17 |
17 |
|
18 text \<open>The \<open>VAR {_}\<close> syntax supports two variants: |
|
19 \<^item> \<open>VAR {x = t}\<close> where \<open>t::nat\<close> is the decreasing expression, |
|
20 the variant, and \<open>x\<close> a variable that can be referred to from inner annotations. |
|
21 The \<open>x\<close> can be necessary for nested loops, e.g. to prove that the inner loops do not mess with \<open>t\<close>. |
|
22 \<^item> \<open>VAR {t}\<close> where the variable is omitted because it is not needed. |
|
23 \<close> |
|
24 |
18 syntax |
25 syntax |
19 "_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) |
26 "_While0" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'com \<Rightarrow> 'com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) |
20 translations |
27 |
21 "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD" |
28 text \<open>The \<open>_While0\<close> syntax is translated into the \<open>_While\<close> syntax with the trivial variant 0. |
|
29 This is ok because partial correctness proofs do not make use of the variant.\<close> |
22 |
30 |
23 syntax |
31 syntax |
24 "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
32 "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
25 "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool" ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) |
33 "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool" ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) |
26 syntax (output) |
34 syntax (output) |
27 "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("{_} // _ // {_}" [0,55,0] 50) |
35 "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("{_} // _ // {_}" [0,55,0] 50) |
28 "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("[_] // _ // [_]" [0,55,0] 50) |
36 "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool" ("[_] // _ // [_]" [0,55,0] 50) |
29 |
37 |
|
38 text \<open>Completeness requires(?) the ability to refer to an outer variant in an inner invariant. |
|
39 Thus we need to abstract over a variable equated with the variant, the \<open>x\<close> in \<open>VAR {x = t}\<close>. |
|
40 But the \<open>x\<close> should only occur in invariants. To enforce this, syntax translations in \<open>hoare_syntax.ML\<close> |
|
41 separate the program from its annotations and only the latter are abstracted over over \<open>x\<close>. |
|
42 (Thus \<open>x\<close> can also occur in inner variants, but that neither helps nor hurts.)\<close> |
|
43 |
|
44 datatype 'a anno = |
|
45 Abasic | |
|
46 Aseq "'a anno" "'a anno" | |
|
47 Acond "'a anno" "'a anno" | |
|
48 Awhile "'a set" "'a \<Rightarrow> nat" "nat \<Rightarrow> 'a anno" |
|
49 |
30 ML_file \<open>hoare_syntax.ML\<close> |
50 ML_file \<open>hoare_syntax.ML\<close> |
31 |
51 |
32 end |
52 end |