21 Basic "'a \<Rightarrow> 'a" |
21 Basic "'a \<Rightarrow> 'a" |
22 | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) |
22 | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) |
23 | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) |
23 | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) |
24 | While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) |
24 | While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) |
25 |
25 |
26 syntax (xsymbols) |
26 syntax |
27 "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) |
27 "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) |
28 |
|
29 translations |
28 translations |
30 "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD" |
29 "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD" |
31 |
30 |
32 abbreviation annskip ("SKIP") where "SKIP == Basic id" |
31 abbreviation annskip ("SKIP") where "SKIP == Basic id" |
33 |
32 |
34 type_synonym 'a sem = "'a => 'a => bool" |
33 type_synonym 'a sem = "'a => 'a => bool" |
35 |
34 |
76 "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) |
75 "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) |
77 |
76 |
78 syntax |
77 syntax |
79 "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" |
78 "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" |
80 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
79 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
81 syntax ("" output) |
80 syntax (output) |
82 "_hoare" :: "['a assn,'a com,'a assn] => bool" |
81 "_hoare" :: "['a assn,'a com,'a assn] => bool" |
83 ("{_} // _ // {_}" [0,55,0] 50) |
82 ("{_} // _ // {_}" [0,55,0] 50) |
84 |
83 |
85 ML_file \<open>hoare_syntax.ML\<close> |
84 ML_file \<open>hoare_syntax.ML\<close> |
86 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close> |
85 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close> |
87 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close> |
86 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close> |
88 |
87 |
89 syntax |
88 syntax |
90 "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" |
89 "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" |
91 ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) |
90 ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) |
92 syntax ("" output) |
91 syntax (output) |
93 "_hoare_tc" :: "['a assn,'a com,'a assn] => bool" |
92 "_hoare_tc" :: "['a assn,'a com,'a assn] => bool" |
94 ("[_] // _ // [_]" [0,55,0] 50) |
93 ("[_] // _ // [_]" [0,55,0] 50) |
95 |
94 |
96 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close> |
95 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close> |
97 print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>))]\<close> |
96 print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>))]\<close> |