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 08

This is the task for homework 08. Deadline: 11.12.2018, 10:00 am.


Download Files

Definitions File

theory Defs
  imports "IMP2.VCG"

lemma intvs_singleton[simp]: 
  "{i::int..<i + 1} = {i}" 
  "{i-1..<i::int} = {i-1}" 
  by auto

lemma intvs_incr_h:
  "l\<le>h \<Longrightarrow> {l::int..<h + 1} = insert h {l..<h}"
  by auto

lemma intvs_decr_h:
  "{l::int..<h - 1} = {l..<h} - {h-1}"
  by auto
lemma intvs_incr_l:
  "{l+1..<h::int} = {l..<h} - {l}"
  by auto

lemma intvs_decr_l:
  "l\<le>h \<Longrightarrow> {l-1..<h::int} = insert (l-1) {l..<h}"
  by auto
lemmas intvs_incdec = intvs_incr_h intvs_incr_l intvs_decr_h intvs_decr_l

lemma intvs_lower_incr: "l<h \<Longrightarrow> {l::int..<h} = insert l ({l+1..<h})" by auto
lemma intvs_upper_decr: "l<h \<Longrightarrow> {l::int..<h} = insert (h-1) ({l..<h-1})" by auto

definition "is_equil a l h i \<equiv> l\<le>i \<and> i<h \<and> (\<Sum>j=l..<i. a j) = (\<Sum>j=i..<h. a j)"


Template File

theory Submission
  imports Defs

program_spec euclid_extended
  assumes "a>0 \<and> b>0"
  ensures "old_r = gcd a\<^sub>0 b\<^sub>0 \<and> gcd a\<^sub>0 b\<^sub>0 = a\<^sub>0 * old_s + b\<^sub>0 * old_t"
defines \<open>
    s = 0;    old_s = 1;
    t = 1;    old_t = 0;
    r = b;    old_r = a;
    while (r\<noteq>0) 
      @invariant\<open>undefined :: bool\<close>      @variant\<open>nat undefined\<close>    {
      quotient = old_r / r;
      temp = old_r;
      old_r = r;
      r = temp - quotient * r;
      temp = old_s;
      old_s = s;
      s = temp - quotient * s;
      temp = old_t;
      old_t = t;
      t = temp - quotient * t

program_spec equilibrium
  assumes \<open>l\<le>h\<close>
  ensures \<open>is_equil a l h i \<or> i=h \<and> (\<nexists>i. is_equil a l h i)\<close>
  defines \<open>
    usum=0; i=l;
    while (i<h) 
      @variant\<open>nat undefined\<close>      @invariant\<open>undefined :: bool\<close>    { 
      usum = usum + a[i]; i=i+1 
    i=l; lsum=0;
    while (usum \<noteq> lsum \<and> i<h) 
      @variant\<open>nat undefined\<close>      @invariant\<open>undefined :: bool\<close>    {
      lsum = lsum + a[i];
      usum = usum - a[i];


Check File

theory Check
  imports Submission

theorem euclid_extended_spec:
 "HT_mods {''t'', ''r'', ''s'', ''temp'', ''old_t'', ''old_r'', ''old_s'', ''quotient''}
  (\<lambda>\<ss>. VAR (\<ss> ''b'' 0) (\<lambda>b. VAR (\<ss> ''a'' 0) (\<lambda>a. BB_PROTECT (0 < a \<and> 0 < b)))) euclid_extended
  (\<lambda>\<ss>\<^sub>0 \<ss>.
      VAR (\<ss>\<^sub>0 ''b'' 0)
       (\<lambda>b\<^sub>0. VAR (\<ss>\<^sub>0 ''a'' 0)
               (\<lambda>a\<^sub>0. VAR (\<ss> ''old_t'' 0)
                           VAR (\<ss> ''old_s'' 0)
                                VAR (\<ss> ''old_r'' 0)
                                      (old_r = gcd a\<^sub>0 b\<^sub>0 \<and> gcd a\<^sub>0 b\<^sub>0 = a\<^sub>0 * old_s + b\<^sub>0 * old_t)))))))"
  by (rule Submission.euclid_extended_spec)

theorem equilibrium_spec:
 "HT_mods {''i'', ''lsum'', ''usum''} (\<lambda>\<ss>. VAR (\<ss> ''l'' 0) (\<lambda>l. VAR (\<ss> ''h'' 0) (\<lambda>s. BB_PROTECT (l \<le> s))))
  (\<lambda>\<ss>\<^sub>0 \<ss>.
      VAR (\<ss> ''l'' 0)
       (\<lambda>l. VAR (\<ss> ''i'' 0)
             (\<lambda>i. VAR (\<ss> ''h'' 0)
                   (\<lambda>h. VAR (\<ss> ''a'') (\<lambda>a. BB_PROTECT (is_equil a l h i \<or> i = h \<and> \<not> Ex (is_equil a l h)))))))
  by (rule Submission.equilibrium_spec)


Terms and Conditions