theory IMP_2 imports"HOL-Library.Predicate_Compile_Quickcheck" begin
subsection \<open>IMP\<close>
text\<open> In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IFand While. \<close>
type_synonym var = unit type_synonym state = bool
datatype com =
Skip |
Ass bool |
Seq com com | IF com com |
While com
inductive exec :: "com => state => state => bool"where "exec Skip s s" | "exec (Ass e) s e" | "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" | "s ==> exec c1 s t ==> exec (IF c1 c2) s t" | "\ s ==> exec c2 s t ==> exec (IF c1 c2) s t" | "\ s ==> exec (While c) s s" | "s ==> exec c s s' ==> exec (While c) s' s'' ==> exec (While c) s s''"
lemma "exec c s s' ==> exec (Seq c c) s s'" quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample] oops
end
¤ 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.0.2Bemerkung:
(vorverarbeitet)
¤
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.
