Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Homework 9

This is the task corresponding to homework 9.


Download Files

Definitions File

theory Defs
  imports "HOL-IMP.BExp"

  com = SKIP
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
      | Seq    com  com         ("_;;/ _"  [60, 61] 60)
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
      | CONTINUE
    big_step :: "com \<times> state \<Rightarrow> bool \<times> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
  Skip: "(SKIP,s) \<Rightarrow> (False,s)" |
  Assign: "(x ::= a,s) \<Rightarrow> (False,s(x := aval a s))" |
  Seq1: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow> (False,s\<^sub>2);  (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
  Seq2: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow> (True,s\<^sub>2) \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> (True,s\<^sub>2)" |
  IfTrue: "\<lbrakk> bval b s;  (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
  IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
  WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> (False,s)" |
  "\<lbrakk> bval b s\<^sub>1;  (c,s\<^sub>1) \<Rightarrow> (_, s\<^sub>2);  (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk>
  \<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" | \<comment> \<open>We can simply reset the continue flag in a while loop\<close>
  Continue: "(CONTINUE,s) \<Rightarrow> (True,s)"

declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
inductive_cases ContinueE[elim!]: "(CONTINUE,s) \<Rightarrow> t"
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"

abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
  ("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

type_synonym assn = "state \<Rightarrow> bool"

hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile> {P}c{Q} = (\<forall>s f t. P s \<and> (c,s) \<Rightarrow> (f, t)  \<longrightarrow>  Q t)"

hoare_valid\<^sub>c :: "assn \<Rightarrow> assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile>\<^sub>c{(1_)}/ {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile>\<^sub>c{I} {P}c{Q} = (\<forall>s f t. P s \<and> (c,s) \<Rightarrow> (f, t)  \<longrightarrow> (if f then I t else Q t))"

consts hoare :: "assn \<Rightarrow> assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool"

consts wp :: "com \<Rightarrow> assn \<Rightarrow> assn \<Rightarrow> assn"


Template File

theory Submission
  imports Defs

  hoare :: "assn \<Rightarrow> assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>{(1_)}/ ({(1_)}/ (_)/ {(1_)})" 50)
Skip: "\<turnstile>{I} {P} SKIP {P}"  |
Assign:  "\<turnstile>{I} {\<lambda>s. P(s[a/x])} x::=a {P}"  |
Seq: "\<lbrakk> \<turnstile>{I} {P} c\<^sub>1 {Q};  \<turnstile>{I} {Q} c\<^sub>2 {R} \<rbrakk>
      \<Longrightarrow> \<turnstile>{I} {P} c\<^sub>1;;c\<^sub>2 {R}"  |
If: "\<lbrakk> \<turnstile>{I} {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q};  \<turnstile>{I} {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
     \<Longrightarrow> \<turnstile>{I} {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"  |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile>{I} {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
        \<Longrightarrow> \<turnstile>{I} {P'} c {Q'}" |
\<comment> \<open>Add your cases here\<close>
theorem hoare_sound: "\<turnstile>{I} {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>c{I} {P}c{Q}"

definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn \<Rightarrow> assn"  where
  "wp _ = undefined"

lemma hoare_complete: assumes "\<Turnstile> {P}c{Q}"
  shows "\<turnstile>{Q} {P}c{Q}"

theorem hoare_sound_complete: "\<turnstile>{Q} {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}"


Check File

theory Check
  imports Submission

theorem hoare_sound: "\<turnstile>{I} {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>c{I} {P}c{Q}"
  by (rule Submission.hoare_sound)

lemma hoare_complete: "(\<Turnstile> {P}c{Q}) \<Longrightarrow> \<turnstile>{Q} {P}c{Q}"
  by (rule Submission.hoare_complete)

theorem hoare_sound_complete: "\<turnstile>{Q} {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}"
  by (rule Submission.hoare_sound_complete)


Terms and Conditions