Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Altern.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/BV/Altern.thy
    Author:     Martin Strecker
*)

section \<open>Alternative definition of well-typing of bytecode,  used in compiler type correctness proof\<close>

theory Altern
imports BVSpec
begin

definition check_type :: "jvm_prog \ nat \ nat \ JVMType.state \ bool" where
  "check_type G mxs mxr s \ s \ states G mxs mxr"

definition wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
                exception_table,p_count] \<Rightarrow> bool" where
  "wt_instr_altern i G rT phi mxs mxr max_pc et pc \
  app i G mxs rT pc et (phi!pc) \<and>
  check_type G mxs mxr (OK (phi!pc)) \<and>
  (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"

definition wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
                 exception_table,method_type] \<Rightarrow> bool" where
  "wt_method_altern G C pTs rT mxs mxl ins et phi \
  let max_pc = length ins in
  0 < max_pc \<and>
  length phi = length ins \<and>
  check_bounded ins et \<and>
  wt_start G C pTs mxl phi \<and>
  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)"

lemma wt_method_wt_method_altern :
  "wt_method G C pTs rT mxs mxl ins et phi \ wt_method_altern G C pTs rT mxs mxl ins et phi"
apply (simp add: wt_method_def wt_method_altern_def)
apply (intro strip)
apply clarify
apply (drule spec, drule mp, assumption)
apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def)
apply (auto  intro: imageI)
done

lemma check_type_check_types [rule_format]:
  "(\pc. pc < length phi \ check_type G mxs mxr (OK (phi ! pc)))
  \<longrightarrow> check_types G mxs mxr (map OK phi)"
apply (induct phi)
apply (simp add: check_types_def)
apply (simp add: check_types_def)
apply clarify
apply (frule_tac x=0 in spec)
apply (simp add: check_type_def)
apply auto
done

lemma wt_method_altern_wt_method [rule_format]:
  "wt_method_altern G C pTs rT mxs mxl ins et phi \ wt_method G C pTs rT mxs mxl ins et phi"
apply (simp add: wt_method_def wt_method_altern_def)
apply (intro strip)
apply clarify
apply (rule conjI)
  (* show check_types *)
apply (rule check_type_check_types)
apply (simp add: wt_instr_altern_def)

  (* show wt_instr *)
apply (intro strip)
apply (drule spec, drule mp, assumption)
apply (simp add: wt_instr_def wt_instr_altern_def)
done

end

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