Quelle IMP_1.thy Sprache: Isabelle

theory IMP_1
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, and IF.
\<close>

type_synonym var = unit
type_synonym state = bool

datatype com =
  Skip |
  Ass bool |
  Seq com com |
  IF com 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"

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

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.