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.

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 :)

Hamed Hajisadeghian has marked this topic as resolved.

Last updated: Aug 13 2022 at 05:18 UTC