text\<open>The \<open>VAR {_}\<close> syntax supports two variants: \<^item> \<open>VAR {x = t}\<close> where \<open>t::nat\<close> is the decreasing expression,
the variant, and\<open>x\<close> a variable that can be referred to from inner annotations.
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>. \<^item> \<open>VAR {t}\<close> where the variable is omitted because it is not needed. \<close>
syntax "_While0" :: "'bexp \ 'assn \ 'com \ 'com"
(\<open>(\<open>indent=1 notation=\<open>mixfix Hoare while expression\<close>\<close>WHILE _/ INV (\<open>open_block notation=\<open>mixfix Hoare invariant\<close>\<close>{_}) //DO _ /OD)\<close> [0, 0, 0] 61) text\<open>The \<open>_While0\<close> syntax is translated into the \<open>_While\<close> syntax with the trivial variant 0.
This is ok because partial correctness proofs do not make use of the variant.\<close>
text\<open>Completeness requires(?) the ability to refer to an outer variant in an inner invariant. Thus we need to abstract over a variable equated with the variant, the \<open>x\<close> in \<open>VAR {x = t}\<close>.
But the \<open>x\<close> should only occur in invariants. To enforce this, syntax translations in \<^file>\<open>hoare_syntax.ML\<close>
separate the program from its annotations and only the latter are abstracted over over \<open>x\<close>.
(Thus\<open>x\<close> can also occur in inner variants, but that neither helps nor hurts.)\<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
