Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: IMP_2.thy Sprache: Isabelle

Original von: Isabelle^©

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, IF and 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

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.