Quelle AxSem.thy Sprache: Isabelle

(*  Title:      HOL/NanoJava/AxSem.thy
    Author:     David von Oheimb, Technische Universitaet Muenchen
*)

section "Axiomatic Semantics"

theory AxSem imports State begin

type_synonym assn = "state => bool"
type_synonym vassn = "val => assn"
type_synonym triple = "assn \ stmt \ assn"
type_synonym etriple = "assn \ expr \ vassn"
translations
  (type) "assn" \<leftharpoondown> (type) "state => bool"
  (type) "vassn" \<leftharpoondown> (type) "val => assn"
  (type) "triple" \<leftharpoondown> (type) "assn \<times> stmt \<times> assn"
  (type) "etriple" \<leftharpoondown> (type) "assn \<times> expr \<times> vassn"

subsection "Hoare Logic Rules"

inductive
hoare :: "[triple set, triple set] => bool"  (\<open>_ |\<turnstile>/ _\<close> [61, 61] 60)
and ehoare :: "[triple set, etriple] => bool"  (\<open>_ |\<turnstile>\<^sub>e/ _\<close> [61, 61] 60)
and hoare1 :: "[triple set, assn,stmt,assn] => bool"
   (\<open>_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})\<close> [61, 3, 90, 3] 60)
and ehoare1 :: "[triple set, assn,expr,vassn]=> bool"
   (\<open>_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})\<close> [61, 3, 90, 3] 60)
where

  "A \ {P}c{Q} \ A |\ {(P,c,Q)}"
| "A \\<^sub>e {P}e{Q} \ A |\\<^sub>e (P,e,Q)"

| Skip:  "A \ {P} Skip {P}"

| Comp: "[| A \ {P} c1 {Q}; A \ {Q} c2 {R} |] ==> A \ {P} c1;;c2 {R}"

| Cond: "[| A \\<^sub>e {P} e {Q};
            \<forall>v. A \<turnstile> {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
            A \<turnstile> {P} If(e) c1 Else c2 {R}"

| Loop: "A \ {\s. P s \ s \ Null} c {P} ==>
         A \<turnstile> {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"

| LAcc: "A \\<^sub>e {\s. P (s) s} LAcc x {P}"

| LAss: "A \\<^sub>e {P} e {\v s. Q (lupd(x\v) s)} ==>
         A \<turnstile>  {P} x:==e {Q}"

| FAcc: "A \\<^sub>e {P} e {\v s. \a. v=Addr a --> Q (get_field s a f) s} ==>
         A \<turnstile>\<^sub>e {P} e..f {Q}"

| FAss: "[| A \\<^sub>e {P} e1 {\v s. \a. v=Addr a --> Q a s};
        \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
            A \<turnstile>  {P} e1..f:==e2 {R}"

| NewC: "A \\<^sub>e {\s. \a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
                new C {P}"

| Cast: "A \\<^sub>e {P} e {\v s. (case v of Null => True
                                 | Addr a => obj_class s a \<preceq>C C) --> Q v s} ==>
         A \<turnstile>\<^sub>e {P} Cast C e {Q}"

| Call: "[| A \\<^sub>e {P} e1 {Q}; \a. A \\<^sub>e {Q a} e2 {R a};
    \<forall>a p ls. A \<turnstile> {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and>
                    s' = lupd(This\a)(lupd(Par\p)(del_locs s))}
                  Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
             A \<turnstile>\<^sub>e {P} {C}e1..m(e2) {S}"

| Meth: "\D. A \ {\s'. \s a. s = Addr a \ D = obj_class s a \ D \C C \
                        P s \<and> s' = init_locs D m s}
                  Impl (D,m) {Q} ==>
             A \<turnstile> {P} Meth (C,m) {Q}"

  \<comment> \<open>\<open>\<Union>Z\<close> instead of \<open>\<forall>Z\<close> in the conclusion and\\
       Z restricted to type state due to limitations of the inductive package\<close>
| Impl: "\Z::state. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\
                            (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
                      A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"

\<comment> \<open>structural rules\<close>

| Asm:  " a \ A ==> A |\ {a}"

| ConjI: " \c \ C. A |\ {c} ==> A |\ C"

| ConjE: "[|A |\ C; c \ C |] ==> A |\ {c}"

  \<comment> \<open>Z restricted to type state due to limitations of the inductive package\<close>
| Conseq:"[| \Z::state. A \ {P' Z} c {Q' Z};
             \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
            A \<turnstile> {P} c {Q }"

  \<comment> \<open>Z restricted to type state due to limitations of the inductive package\<close>
| eConseq:"[| \Z::state. A \\<^sub>e {P' Z} e {Q' Z};
             \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
            A \<turnstile>\<^sub>e {P} e {Q }"

subsection "Fully polymorphic variants, required for Example only"

axiomatization where
  Conseq:"[| \Z. A \ {P' Z} c {Q' Z};
             \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
                 A \<turnstile> {P} c {Q }"

axiomatization where
  eConseq:"[| \Z. A \\<^sub>e {P' Z} e {Q' Z};
             \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
                 A \<turnstile>\<^sub>e {P} e {Q }"

axiomatization where
  Impl: "\Z. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\
                          (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
                    A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"

subsection "Derived Rules"

lemma Conseq1: "\A \ {P'} c {Q}; \s. P s \ P' s\ \ A \ {P} c {Q}"
apply (rule hoare_ehoare.Conseq)
apply  (rule allI, assumption)
apply fast
done

lemma Conseq2: "\A \ {P} c {Q'}; \t. Q' t \ Q t\ \ A \ {P} c {Q}"
apply (rule hoare_ehoare.Conseq)
apply  (rule allI, assumption)
apply fast
done

lemma eConseq1: "\A \\<^sub>e {P'} e {Q}; \s. P s \ P' s\ \ A \\<^sub>e {P} e {Q}"
apply (rule hoare_ehoare.eConseq)
apply  (rule allI, assumption)
apply fast
done

lemma eConseq2: "\A \\<^sub>e {P} e {Q'}; \v t. Q' v t \ Q v t\ \ A \\<^sub>e {P} e {Q}"
apply (rule hoare_ehoare.eConseq)
apply  (rule allI, assumption)
apply fast
done

lemma Weaken: "\A |\ C'; C \ C'\ \ A |\ C"
apply (rule hoare_ehoare.ConjI)
apply clarify
apply (drule hoare_ehoare.ConjE)
apply  fast
apply assumption
done

lemma Thin_lemma:
  "(A' |\ C \ (\A. A' \ A \ A |\ C )) \
   (A' \\<^sub>e {P} e {Q} \ (\A. A' \ A \ A \\<^sub>e {P} e {Q}))"
apply (rule hoare_ehoare.induct)
apply (tactic "ALLGOALS(EVERY'[clarify_tac \<^context>, REPEAT o smp_tac \<^context> 1])")
apply (blast intro: hoare_ehoare.Skip)
apply (blast intro: hoare_ehoare.Comp)
apply (blast intro: hoare_ehoare.Cond)
apply (blast intro: hoare_ehoare.Loop)
apply (blast intro: hoare_ehoare.LAcc)
apply (blast intro: hoare_ehoare.LAss)
apply (blast intro: hoare_ehoare.FAcc)
apply (blast intro: hoare_ehoare.FAss)
apply (blast intro: hoare_ehoare.NewC)
apply (blast intro: hoare_ehoare.Cast)
apply (erule hoare_ehoare.Call)
apply   (rule, drule spec, erule conjE, tactic "smp_tac \<^context> 1 1", assumption)
apply  blast
apply (blast intro!: hoare_ehoare.Meth)
apply (blast intro!: hoare_ehoare.Impl)
apply (blast intro!: hoare_ehoare.Asm)
apply (blast intro: hoare_ehoare.ConjI)
apply (blast intro: hoare_ehoare.ConjE)
apply (rule hoare_ehoare.Conseq)
apply  (rule, drule spec, erule conjE, tactic "smp_tac \<^context> 1 1", assumption+)
apply (rule hoare_ehoare.eConseq)
apply  (rule, drule spec, erule conjE, tactic "smp_tac \<^context> 1 1", assumption+)
done

lemma cThin: "\A' |\ C; A' \ A\ \ A |\ C"
by (erule (1) conjunct1 [OF Thin_lemma, rule_format])

lemma eThin: "\A' \\<^sub>e {P} e {Q}; A' \ A\ \ A \\<^sub>e {P} e {Q}"
by (erule (1) conjunct2 [OF Thin_lemma, rule_format])

lemma Union: "A |\ (\Z. C Z) = (\Z. A |\ C Z)"
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)

lemma Impl1':
   "\\Z::state. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\
                 (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms;
    Cm \<in> Ms\<rbrakk> \<Longrightarrow>
                A   \<turnstile>  {P Z Cm} Impl Cm {Q Z Cm}"
apply (drule AxSem.Impl)
apply (erule Weaken)
apply (auto del: image_eqI intro: rev_image_eqI)
done

lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified] for Cm

end

quality98%

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