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 07

This is the task for homework 07.

## Resources

### 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```

Terms and Conditions