Homework 07

Definitions File

theory Defs
  imports "IMP2.VCG"
begin

fun factorial :: "int \<Rightarrow> int" where
  "factorial i = (if i \<le> 0 then 1 else i * factorial (i - 1))"

fun fib :: "int \<Rightarrow> int" where
  "fib i = (if i \<le> 0 then 0 else if i = 1 then 1 else fib (i - 2) + fib (i - 1))"

lemma fib_simps[simp]:
  "i \<le> 0 \<Longrightarrow> fib i = 0"
  "i = 1 \<Longrightarrow> fib i = 1"
  "i > 1 \<Longrightarrow> fib i = fib (i - 2) + fib (i - 1)"
  by simp+

lemmas [simp del] = fib.simps

end

Template File

theory Submission
  imports Defs
begin

program_spec factorial_prog
  assumes "n \<ge> 0" ensures "a = factorial n\<^sub>0"
  defines \<open>
    a = 1;
    i = 1;
    while (i \<le> n)
      @variant\<open>nat undefined\<close>
      @invariant\<open>undefined :: bool\<close>
    {
      a = a * i;
      i = i + 1
    }
  \<close>
  sorry


program_spec fib_prog
  assumes "n \<ge> 0" ensures "a = fib n"
  defines \<open>
    a = 0; b = 1;
    i = 0;
    while (i < n) 
      @variant\<open>nat undefined\<close>
      @invariant\<open>undefined :: bool\<close>   
    {
      c = b;
      b = a + b;
      a = c;
      i = i + 1
    }
  \<close>
  sorry


program_spec fib_prog'
  assumes True ensures "a = fib n\<^sub>0"
  defines \<open>
    a = 0; b = 1;
    i = 0;
    while (i < n) 
      @variant\<open>nat undefined\<close>
      @invariant\<open>undefined :: bool\<close>
    {
      c = b;
      b = a + b;
      a = c;
      i = i + 1
    }
  \<close>
  sorry


fun lhsv :: "com \<Rightarrow> vname set" where
  "lhsv _ = undefined"

theorem wp_strengthen_modset:
  "wp c Q s \<Longrightarrow> wp c (\<lambda>s'. Q s' \<and> (\<forall>x. x\<notin>lhsv c \<longrightarrow> s' x = s x)) s"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem factorial_prog_correct:
 "HT (\<lambda>\<ss>. VAR \<ss> ''n'' ((\<le>) 0)) factorial_prog
  (\<lambda>\<ss>\<^sub>0. VAR \<ss>\<^sub>0 ''n'' (\<lambda>n\<^sub>0 \<ss>. VAR \<ss> ''a'' (\<lambda>a. a = factorial n\<^sub>0)))"
  by (rule Submission.factorial_prog_spec)

theorem fib_prog_correct:
 "HT (\<lambda>\<ss>. VAR \<ss> ''n'' ((\<le>) 0)) fib_prog (\<lambda>\<ss>\<^sub>0 \<ss>. VAR \<ss> ''n'' (\<lambda>n. VAR \<ss> ''a'' (\<lambda>a. a = fib n)))"
  by (rule Submission.fib_prog_spec)

theorem fib_prog'_correct:
 "HT (\<lambda>\<ss>. True) fib_prog' (\<lambda>\<ss>\<^sub>0. VAR \<ss>\<^sub>0 ''n'' (\<lambda>n\<^sub>0 \<ss>. VAR \<ss> ''a'' (\<lambda>a. a = fib n\<^sub>0)))"
  by (rule Submission.fib_prog'_spec)

theorem wp_strengthen_modset:
  "wp c Q s \<Longrightarrow> wp c (\<lambda>s'. Q s' \<and> (\<forall>x. x\<notin>lhsv c \<longrightarrow> s' x = s x)) s"
  by (rule Submission.wp_strengthen_modset)

end