Stream: Beginner Questions

Topic: ✔ Proving lemma about IMP codes

Hamed Hajisadeghian (Oct 06 2021 at 20:12):

Hi, I've been reading IMP section from concrete-semantics up to Small-Step Semantics, I defined syntax and semantics for Irem which acts like mod operator. I wanted to prove following lemma about equivalence of imperative and declarative way of calculating gcd:

lemma "{map t [''m'', ''n'', ''M'', ''N'', ''c''] |t.
  (''M''::= V ''m'';;
   ''N''::= V ''n'';;
   WHILE Less (N 0) (V ''N'') DO
   (
       ''c'' ::= V ''M'';;
       ''M'' ::= V ''N'';;
       ''N'' ::= Irem (V ''c'') (V ''N'')
   ),
   <''m'' := m, ''n'' := n, ''M'' := 0, ''N'' := 0, ''c'' := 0>) ⇒ t} = {[m, n, (gcd m n), 0, (n - (gcd m n))]}"

How to prove this lemma or is there a better way of implementing imperative algorithms and proving their correctness (specially the equivalence of imperative and declarative form)? Thanks for your help.

Simon Wimmer (Nov 09 2021 at 14:01):

Hamed Hajisadeghian said:

Hi, I've been reading IMP section from concrete-semantics up to Small-Step Semantics, I defined syntax and semantics for Irem which acts like mod operator. I wanted to prove following lemma about equivalence of imperative and declarative way of calculating gcd:

lemma "{map t [''m'', ''n'', ''M'', ''N'', ''c''] |t.
  (''M''::= V ''m'';;
   ''N''::= V ''n'';;
   WHILE Less (N 0) (V ''N'') DO
   (
       ''c'' ::= V ''M'';;
       ''M'' ::= V ''N'';;
       ''N'' ::= Irem (V ''c'') (V ''N'')
   ),
   <''m'' := m, ''n'' := n, ''M'' := 0, ''N'' := 0, ''c'' := 0>) ⇒ t} = {[m, n, (gcd m n), 0, (n - (gcd m n))]}"

How to prove this lemma or is there a better way of implementing imperative algorithms and proving their correctness (specially the equivalence of imperative and declarative form)? Thanks for your help.

Hi Hamed,

you could try to prove this by induction. But then you would need to generalize your statement first and then you probably would use an induction on the value of V "N". However, this will likely be tedious.
If you read on in the book and eventually get to the chapter on Hoare logic, you will have the proper tools to prove your statement :)

Notification Bot (Dec 20 2021 at 15:21):

Hamed Hajisadeghian has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC