Quelle Compiler2.thy Sprache: Isabelle

(* Author: Gerwin Klein *)

section \<open>Compiler Correctness, Reverse Direction\<close>

theory Compiler2
imports Compiler
begin

text \<open>
The preservation of the source code semantics is already shown in the
parent theory \<open>Compiler\<close>. This here shows the second direction.
\<close>

subsection \<open>Definitions\<close>

text \<open>Execution in \<^term>\<open>n\<close> steps for simpler induction\<close>
primrec
  exec_n :: "instr list \ config \ nat \ config \ bool"
  (\<open>_/ \<turnstile> (_ \<rightarrow>^_/ _)\<close> [65,0,1000,55] 55)
where
  "P \ c \^0 c' = (c'=c)" |
  "P \ c \^(Suc n) c'' = (\c'. (P \ c \ c') \ P \ c' \^n c'')"

text \<open>The possible successor PCs of an instruction at position \<^term>\<open>n\<close>\<close>
text_raw\<open>\snip{isuccsdef}{0}{1}{%\<close>
definition isuccs :: "instr \ int \ int set" where
"isuccs i n = (case i of
  JMP j \<Rightarrow> {n + 1 + j} |
  JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} |
  JMPGE j \<Rightarrow> {n + 1 + j, n + 1} |
  _ \<Rightarrow> {n +1})"
text_raw\<open>}%endsnip\<close>

text \<open>The possible successors PCs of an instruction list\<close>
definition succs :: "instr list \ int \ int set" where
"succs P n = {s. \i::int. 0 \ i \ i < size P \ s \ isuccs (P!!i) (n+i)}"

text \<open>Possible exit PCs of a program\<close>
definition exits :: "instr list \ int set" where
"exits P = succs P 0 - {0..< size P}"


subsection \<open>Basic properties of \<^term>\<open>exec_n\<close>\<close>

lemma exec_n_exec:
  "P \ c \^n c' \ P \ c \* c'"
  by (induct n arbitrary: c) (auto intro: star.step)

lemma exec_0 [intro!]: "P \ c \^0 c" by simp

lemma exec_Suc:
  "\ P \ c \ c'; P \ c' \^n c'' \ \ P \ c \^(Suc n) c''"
  by (fastforce simp del: split_paired_Ex)

lemma exec_exec_n:
  "P \ c \* c' \ \n. P \ c \^n c'"
  by (induct rule: star.induct) (auto intro: exec_Suc)

lemma exec_eq_exec_n:
  "(P \ c \* c') = (\n. P \ c \^n c')"
  by (blast intro: exec_exec_n exec_n_exec)

lemma exec_n_Nil [simp]:
  "[] \ c \^k c' = (c' = c \ k = 0)"
  by (induct k) (auto simp: exec1_def)

lemma exec1_exec_n [intro!]:
  "P \ c \ c' \ P \ c \^1 c'"
  by (cases c') simp

subsection \<open>Concrete symbolic execution steps\<close>

lemma exec_n_step:
  "n \ n' \
  P \<turnstile> (n,stk,s) \<rightarrow>^k (n',stk',s') =
  (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)"
  by (cases k) auto

lemma exec1_end:
  "size P <= fst c \ \ P \ c \ c'"
  by (auto simp: exec1_def)

lemma exec_n_end:
  "size P <= (n::int) \
  P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)"
  by (cases k) (auto simp: exec1_end)

lemmas exec_n_simps = exec_n_step exec_n_end

subsection \<open>Basic properties of \<^term>\<open>succs\<close>\<close>

lemma succs_simps [simp]:
  "succs [ADD] n = {n + 1}"
  "succs [LOADI v] n = {n + 1}"
  "succs [LOAD x] n = {n + 1}"
  "succs [STORE x] n = {n + 1}"
  "succs [JMP i] n = {n + 1 + i}"
  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
  by (auto simp: succs_def isuccs_def)

lemma succs_empty [iff]: "succs [] n = {}"
  by (simp add: succs_def)

lemma succs_Cons:
  "succs (x#xs) n = isuccs x n \ succs xs (1+n)" (is "_ = ?x \ ?xs")
proof
  let ?isuccs = "\p P n i::int. 0 \ i \ i < size P \ p \ isuccs (P!!i) (n+i)"
  have "p \ ?x \ ?xs" if assm: "p \ succs (x#xs) n" for p
  proof -
    from assm obtain i::int where isuccs: "?isuccs p (x#xs) n i"
      unfolding succs_def by auto
    show ?thesis
    proof cases
      assume "i = 0" with isuccs show ?thesis by simp
    next
      assume "i \ 0"
      with isuccs
      have "?isuccs p xs (1+n) (i - 1)" by auto
      hence "p \ ?xs" unfolding succs_def by blast
      thus ?thesis ..
    qed
  qed
  thus "succs (x#xs) n \ ?x \ ?xs" ..

  have "p \ succs (x#xs) n" if assm: "p \ ?x \ p \ ?xs" for p
  proof -
    from assm show ?thesis
    proof
      assume "p \ ?x" thus ?thesis by (fastforce simp: succs_def)
    next
      assume "p \ ?xs"
      then obtain i where "?isuccs p xs (1+n) i"
        unfolding succs_def by auto
      hence "?isuccs p (x#xs) n (1+i)"
        by (simp add: algebra_simps)
      thus ?thesis unfolding succs_def by blast
    qed
  qed
  thus "?x \ ?xs \ succs (x#xs) n" by blast
qed

lemma succs_iexec1:
  assumes "c' = iexec (P!!i) (i,s,stk)" "0 \ i" "i < size P"
  shows "fst c' \ succs P 0"
  using assms by (auto simp: succs_def isuccs_def split: instr.split)

lemma succs_shift:
  "(p - n \ succs P 0) = (p \ succs P n)"
  by (fastforce simp: succs_def isuccs_def split: instr.split)

lemma inj_op_plus [simp]:
  "inj ((+) (i::int))"
  by (metis add_minus_cancel inj_on_inverseI)

lemma succs_set_shift [simp]:
  "(+) i ` succs xs 0 = succs xs i"
  by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)

lemma succs_append [simp]:
  "succs (xs @ ys) n = succs xs n \ succs ys (n + size xs)"
  by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps)

lemma exits_append [simp]:
  "exits (xs @ ys) = exits xs \ ((+) (size xs)) ` exits ys -
                     {0..<size xs + size ys}"
  by (auto simp: exits_def image_set_diff)

lemma exits_single:
  "exits [x] = isuccs x 0 - {0}"
  by (auto simp: exits_def succs_def)

lemma exits_Cons:
  "exits (x # xs) = (isuccs x 0 - {0}) \ ((+) 1) ` exits xs -
                     {0..<1 + size xs}"
  using exits_append [of "[x]" xs]
  by (simp add: exits_single)

lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def)

lemma exits_simps [simp]:
  "exits [ADD] = {1}"
  "exits [LOADI v] = {1}"
  "exits [LOAD x] = {1}"
  "exits [STORE x] = {1}"
  "i \ -1 \ exits [JMP i] = {1 + i}"
  "i \ -1 \ exits [JMPGE i] = {1 + i, 1}"
  "i \ -1 \ exits [JMPLESS i] = {1 + i, 1}"
  by (auto simp: exits_def)

lemma acomp_succs [simp]:
  "succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
  by (induct a arbitrary: n) auto

lemma acomp_exits [simp]:
  "exits (acomp a) = {size (acomp a)}"
proof -
  have "Suc 0 \ length (acomp a)"
    by (induct a) auto
  then show ?thesis
    by (auto simp add: exits_def)
qed

lemma bcomp_succs:
  "0 \ i \
  succs (bcomp b f i) n \<subseteq> {n .. n + size (bcomp b f i)}
                           \<union> {n + i + size (bcomp b f i)}"
proof (induction b arbitrary: f i n)
  case (And b1 b2)
  from And.prems
  show ?case
    by (cases f)
       (auto dest: And.IH(1) [THEN subsetD, rotated]
                   And.IH(2) [THEN subsetD, rotated])
qed auto

lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]

lemma bcomp_exits:
  fixes i :: int
  shows
  "0 \ i \
  exits (bcomp b f i) \<subseteq> {size (bcomp b f i), i + size (bcomp b f i)}"
  by (auto simp: exits_def)

lemma bcomp_exitsD [dest!]:
  "p \ exits (bcomp b f i) \ 0 \ i \
  p = size (bcomp b f i) \<or> p = i + size (bcomp b f i)"
  using bcomp_exits by auto

lemma ccomp_succs:
  "succs (ccomp c) n \ {n..n + size (ccomp c)}"
proof (induction c arbitrary: n)
  case SKIP thus ?case by simp
next
  case Assign thus ?case by simp
next
  case (Seq c1 c2)
  from Seq.prems
  show ?case
    by (fastforce dest: Seq.IH [THEN subsetD])
next
  case (If b c1 c2)
  from If.prems
  show ?case
    by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
next
  case (While b c)
  from While.prems
  show ?case by (auto dest!: While.IH [THEN subsetD])
qed

lemma ccomp_exits:
  "exits (ccomp c) \ {size (ccomp c)}"
  using ccomp_succs [of c 0] by (auto simp: exits_def)

lemma ccomp_exitsD [dest!]:
  "p \ exits (ccomp c) \ p = size (ccomp c)"
  using ccomp_exits by auto

subsection \<open>Splitting up machine executions\<close>

lemma exec1_split:
  fixes i j :: int
  shows
  "P @ c @ P' \ (size P + i, s) \ (j,s') \ 0 \ i \ i < size c \
  c \<turnstile> (i,s) \<rightarrow> (j - size P, s')"
  by (auto split: instr.splits simp: exec1_def)

lemma exec_n_split:
  fixes i j :: int
  assumes "P @ c @ P' \ (size P + i, s) \^n (j, s')"
          "0 \ i" "i < size c"
          "j \ {size P ..< size P + size c}"
  shows "\s'' (i'::int) k m.
                   c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
                   i' \ exits c \
                   P @ c @ P' \ (size P + i', s'') \^m (j, s') \
                   n = k + m"
using assms proof (induction n arbitrary: i j s)
  case 0
  thus ?case by simp
next
  case (Suc n)
  have i: "0 \ i" "i < size c" by fact+
  from Suc.prems
  have j: "\ (size P \ j \ j < size P + size c)" by simp
  from Suc.prems
  obtain i0 s0 where
    step: "P @ c @ P' \ (size P + i, s) \ (i0,s0)" and
    rest: "P @ c @ P' \ (i0,s0) \^n (j, s')"
    by clarsimp

  from step i
  have c: "c \ (i,s) \ (i0 - size P, s0)" by (rule exec1_split)

  have "i0 = size P + (i0 - size P) " by simp
  then obtain j0::int where j0: "i0 = size P + j0"  ..

  note split_paired_Ex [simp del]

  have ?case if assm: "j0 \ {0 ..< size c}"
  proof -
    from assm j0 j rest c show ?case
      by (fastforce dest!: Suc.IH intro!: exec_Suc)
  qed
  moreover
  have ?case if assm: "j0 \ {0 ..< size c}"
  proof -
    from c j0 have "j0 \ succs c 0"
      by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
    with assm have "j0 \ exits c" by (simp add: exits_def)
    with c j0 rest show ?case by fastforce
  qed
  ultimately
  show ?case by cases
qed

lemma exec_n_drop_right:
  fixes j :: int
  assumes "c @ P' \ (0, s) \^n (j, s')" "j \ {0..
  shows "\s'' i' k m.
          (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
           else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
           i' \ exits c) \
           c @ P' \ (i', s'') \^m (j, s') \
           n = k + m"
  using assms
  by (cases "c = []")
     (auto dest: exec_n_split [where P="[]", simplified])


text \<open>
  Dropping the left context of a potentially incomplete execution of \<^term>\<open>c\<close>.
\<close>

lemma exec1_drop_left:
  fixes i n :: int
  assumes "P1 @ P2 \ (i, s, stk) \ (n, s', stk')" and "size P1 \ i"
  shows "P2 \ (i - size P1, s, stk) \ (n - size P1, s', stk')"
proof -
  have "i = size P1 + (i - size P1)" by simp
  then obtain i' :: int where "i = size P1 + i'" ..
  moreover
  have "n = size P1 + (n - size P1)" by simp
  then obtain n' :: int where "n = size P1 + n'" ..
  ultimately
  show ?thesis using assms
    by (clarsimp simp: exec1_def simp del: iexec.simps)
qed

lemma exec_n_drop_left:
  fixes i n :: int
  assumes "P @ P' \ (i, s, stk) \^k (n, s', stk')"
          "size P \ i" "exits P' \ {0..}"
  shows "P' \ (i - size P, s, stk) \^k (n - size P, s', stk')"
using assms proof (induction k arbitrary: i s stk)
  case 0 thus ?case by simp
next
  case (Suc k)
  from Suc.prems
  obtain i' s'' stk'' where
    step: "P @ P' \ (i, s, stk) \ (i', s'', stk'')" and
    rest: "P @ P' \ (i', s'', stk'') \^k (n, s', stk')"
    by auto
  from step \<open>size P \<le> i\<close>
  have *: "P' \ (i - size P, s, stk) \ (i' - size P, s'', stk'')"
    by (rule exec1_drop_left)
  then have "i' - size P \ succs P' 0"
    by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
  with \<open>exits P' \<subseteq> {0..}\<close>
  have "size P \ i'" by (auto simp: exits_def)
  from rest this \<open>exits P' \<subseteq> {0..}\<close>
  have "P' \ (i' - size P, s'', stk'') \^k (n - size P, s', stk')"
    by (rule Suc.IH)
  with * show ?case by auto
qed

lemmas exec_n_drop_Cons =
  exec_n_drop_left [where P="[instr]", simplified] for instr

definition
  "closed P \ exits P \ {size P}"

lemma ccomp_closed [simp, intro!]: "closed (ccomp c)"
  using ccomp_exits by (auto simp: closed_def)

lemma acomp_closed [simp, intro!]: "closed (acomp c)"
  by (simp add: closed_def)

lemma exec_n_split_full:
  fixes j :: int
  assumes exec: "P @ P' \ (0,s,stk) \^k (j, s', stk')"
  assumes P: "size P \ j"
  assumes closed: "closed P"
  assumes exits: "exits P' \ {0..}"
  shows "\k1 k2 s'' stk''. P \ (0,s,stk) \^k1 (size P, s'', stk'') \
                           P' \ (0,s'',stk'') \^k2 (j - size P, s', stk')"
proof (cases "P")
  case Nil with exec
  show ?thesis by fastforce
next
  case Cons
  hence "0 < size P" by simp
  with exec P closed
  obtain k1 k2 s'' stk'' where
    1: "P \ (0,s,stk) \^k1 (size P, s'', stk'')" and
    2: "P @ P' \ (size P,s'',stk'') \^k2 (j, s', stk')"
    by (auto dest!: exec_n_split [where P="[]" and i=0, simplified]
             simp: closed_def)
  moreover
  have "j = size P + (j - size P)" by simp
  then obtain j0 :: int where "j = size P + j0" ..
  ultimately
  show ?thesis using exits
    by (fastforce dest: exec_n_drop_left)
qed

subsection \<open>Correctness theorem\<close>

lemma acomp_neq_Nil [simp]:
  "acomp a \ []"
  by (induct a) auto

lemma acomp_exec_n [dest!]:
  "acomp a \ (0,s,stk) \^n (size (acomp a),s',stk') \
  s' = s \ stk' = aval a s#stk"
proof (induction a arbitrary: n s' stk stk')
  case (Plus a1 a2)
  let ?sz = "size (acomp a1) + (size (acomp a2) + 1)"
  from Plus.prems
  have "acomp a1 @ acomp a2 @ [ADD] \ (0,s,stk) \^n (?sz, s', stk')"
    by (simp add: algebra_simps)

  then obtain n1 s1 stk1 n2 s2 stk2 n3 where
    "acomp a1 \ (0,s,stk) \^n1 (size (acomp a1), s1, stk1)"
    "acomp a2 \ (0,s1,stk1) \^n2 (size (acomp a2), s2, stk2)"
       "[ADD] \ (0,s2,stk2) \^n3 (1, s', stk')"
    by (auto dest!: exec_n_split_full)

  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps exec1_def)
qed (auto simp: exec_n_simps exec1_def)

lemma bcomp_split:
  fixes i j :: int
  assumes "bcomp b f i @ P' \ (0, s, stk) \^n (j, s', stk')"
          "j \ {0.. i"
  shows "\s'' stk'' (i'::int) k m.
           bcomp b f i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
           (i' = size (bcomp b f i) \ i' = i + size (bcomp b f i)) \
           bcomp b f i @ P' \ (i', s'', stk'') \^m (j, s', stk') \
           n = k + m"
  using assms by (cases "bcomp b f i = []") (fastforce dest!: exec_n_drop_right)+

lemma bcomp_exec_n [dest]:
  fixes i j :: int
  assumes "bcomp b f j \ (0, s, stk) \^n (i, s', stk')"
          "size (bcomp b f j) \ i" "0 \ j"
  shows "i = size(bcomp b f j) + (if f = bval b s then j else 0) \
         s' = s \ stk' = stk"
using assms proof (induction b arbitrary: f j i n s' stk')
  case Bc thus ?case
    by (simp split: if_split_asm add: exec_n_simps exec1_def)
next
  case (Not b)
  from Not.prems show ?case
    by (fastforce dest!: Not.IH)
next
  case (And b1 b2)

  let ?b2 = "bcomp b2 f j"
  let ?m  = "if f then size ?b2 else size ?b2 + j"
  let ?b1 = "bcomp b1 False ?m"

  have j: "size (bcomp (And b1 b2) f j) \ i" "0 \ j" by fact+

  from And.prems
  obtain s'' stk'' and i'::int and k m where
    b1: "?b1 \ (0, s, stk) \^k (i', s'', stk'')"
        "i' = size ?b1 \ i' = ?m + size ?b1" and
    b2: "?b2 \ (i' - size ?b1, s'', stk'') \^m (i - size ?b1, s', stk')"
    by (auto dest!: bcomp_split dest: exec_n_drop_left)
  from b1 j
  have "i' = size ?b1 + (if \bval b1 s then ?m else 0) \ s'' = s \ stk'' = stk"
    by (auto dest!: And.IH)
  with b2 j
  show ?case
    by (fastforce dest!: And.IH simp: exec_n_end split: if_split_asm)
next
  case Less
  thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def) (* takes time *)
qed

lemma ccomp_empty [elim!]:
  "ccomp c = [] \ (c,s) \ s"
  by (induct c) auto

declare assign_simp [simp]

lemma ccomp_exec_n:
  "ccomp c \ (0,s,stk) \^n (size(ccomp c),t,stk')
  \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
proof (induction c arbitrary: s t stk stk' n)
  case SKIP
  thus ?case by auto
next
  case (Assign x a)
  thus ?case
    by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps exec1_def)
next
  case (Seq c1 c2)
  thus ?case by (fastforce dest!: exec_n_split_full)
next
  case (If b c1 c2)
  note If.IH [dest!]

  let ?if = "IF b THEN c1 ELSE c2"
  let ?cs = "ccomp ?if"
  let ?bcomp = "bcomp b False (size (ccomp c1) + 1)"

  from \<open>?cs \<turnstile> (0,s,stk) \<rightarrow>^n (size ?cs,t,stk')\<close>
  obtain i' :: int and k m s'' stk'' where
    cs: "?cs \ (i',s'',stk'') \^m (size ?cs,t,stk')" and
        "?bcomp \ (0,s,stk) \^k (i', s'', stk'')"
        "i' = size ?bcomp \ i' = size ?bcomp + size (ccomp c1) + 1"
    by (auto dest!: bcomp_split)

  hence i':
    "s''=s" "stk'' = stk"
    "i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)"
    by auto

  with cs have cs':
    "ccomp c1@JMP (size (ccomp c2))#ccomp c2 \
       (if bval b s then 0 else size (ccomp c1)+1, s, stk) \<rightarrow>^m
       (1 + size (ccomp c1) + size (ccomp c2), t, stk')"
    by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)

  show ?case
  proof (cases "bval b s")
    case True with cs'
    show ?thesis
      by simp
         (fastforce dest: exec_n_drop_right
                   split: if_split_asm
                   simp: exec_n_simps exec1_def)
  next
    case False with cs'
    show ?thesis
      by (auto dest!: exec_n_drop_Cons exec_n_drop_left
               simp: exits_Cons isuccs_def)
  qed
next
  case (While b c)

  from While.prems
  show ?case
  proof (induction n arbitrary: s rule: nat_less_induct)
    case (1 n)

    have ?case if assm: "\ bval b s"
    proof -
      from assm "1.prems"
      show ?case
        by simp (fastforce dest!: bcomp_split simp: exec_n_simps)
    qed
    moreover
    have ?case if b: "bval b s"
    proof -
      let ?c0 = "WHILE b DO c"
      let ?cs = "ccomp ?c0"
      let ?bs = "bcomp b False (size (ccomp c) + 1)"
      let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]"

      from "1.prems" b
      obtain k where
        cs: "?cs \ (size ?bs, s, stk) \^k (size ?cs, t, stk')" and
        k:  "k \ n"
        by (fastforce dest!: bcomp_split)

      show ?case
      proof cases
        assume "ccomp c = []"
        with cs k
        obtain m where
          "?cs \ (0,s,stk) \^m (size (ccomp ?c0), t, stk')"
          "m < n"
          by (auto simp: exec_n_step [where k=k] exec1_def)
        with "1.IH"
        show ?case by blast
      next
        assume "ccomp c \ []"
        with cs
        obtain m m' s'' stk'' where
          c: "ccomp c \ (0, s, stk) \^m' (size (ccomp c), s'', stk'')" and
          rest: "?cs \ (size ?bs + size (ccomp c), s'', stk'') \^m
                       (size ?cs, t, stk')" and
          m: "k = m + m'"
          by (auto dest: exec_n_split [where i=0, simplified])
        from c
        have "(c,s) \ s''" and stk: "stk'' = stk"
          by (auto dest!: While.IH)
        moreover
        from rest m k stk
        obtain k' where
          "?cs \ (0, s'', stk) \^k' (size ?cs, t, stk')"
          "k' < n"
          by (auto simp: exec_n_step [where k=m] exec1_def)
        with "1.IH"
        have "(?c0, s'') \ t \ stk' = stk" by blast
        ultimately
        show ?case using b by blast
      qed
    qed
    ultimately show ?case by cases
  qed
qed

theorem ccomp_exec:
  "ccomp c \ (0,s,stk) \* (size(ccomp c),t,stk') \ (c,s) \ t"
  by (auto dest: exec_exec_n ccomp_exec_n)

corollary ccomp_sound:
  "ccomp c \ (0,s,stk) \* (size(ccomp c),t,stk) \ (c,s) \ t"
  by (blast intro!: ccomp_exec ccomp_bigstep)

end

quality97%

¤ Dauer der Verarbeitung: 0.19 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.