Murphi入门（九）—— 用murphi实现GCD（4）

发表于 更新于 分类于 阅读次数：

该博文将继续从循环不变量的角度对gcd的murphi程序进行进阶修改：

  • 一条规则只执行一次辗转相除

  • 变量只有两个，把需要输入的数当作常量

  • 用swap程序，仅需执行一次交换

  • procedure与function的区别

预备知识

这次的GCD改进，是在之前三次改进的基础上进行。

快速通道：

gcd改进（1）

gcd改进（2）

gcd改进（3）

循环不变量、前置断言、后置断言

前言

由于在上一次改进时，我把while循环放在了rule中。其实这是不必要的。因为murphi本身就是可以无限执行下去，直到所有状态都在已有状态表中为止。所以这次对rule进行了改进。

而且，为了更关注辗转相除的两个变量本身，我把两个初始值当作常量，且定义了一个范围，这样使得状态中只有两个变量本身，没有多余的变量，非常清晰。

具体实现

定义类型部分

1
2
3
4
5
6
7
8
9
10
const
    RANGE : 1000;
	a : 20;
	b : 12;
type
    val_t: 0..RANGE;
    
var
	n : val_t;
	m : val_t;

可以看到，定义部分有三种类型的定义：

  • const：常量，不能改变。其中，RANGE是这个程序中所有变量的范围，a，b不能超过这个范围。
  • type：自定义类型。它定义了一个名为val_t 的类型，这个类型的范围是 [0，100]
  • var：变量，可以改变。这里定义了两个类型为val_t的变量m，n

规则部分

1
2
3
4
5
6
7
8
9
10
11
rule "loop"
	n != m & n > 0 & m > 0
==>
var temp: val_t; 
begin
    Swap(m, n); -- 保证减法能顺利进行
    temp := m - n;
    m := n;
    n := temp;
    Swap(m, n); -- 其实可以不用，但是为了保证统一的格式，即输出状态时始终 m > n
end;

可以看到，规则部分的前置断言是m，n不相等，且都大于0

第一个Swap是为了保证后面的减法能够顺利进行。如果不加这个交换，就会出现相减之后结果为负数的情况，则超出m，n定义的范围。后面的一个Swap其实可加可不加，因为下一次进入这个rule的时候依然会有一个交换保证减法顺利进行。但是加了这个，是为了在状态输出的时候，m始终大于n。

程序部分

这部分程序为了执行两数交换，保证前面的数总是比后面的数大

1
2
3
4
5
6
7
8
9
procedure Swap(var i, j: val_t); -- 子程序，执行交换i，j的值
var temp: val_t; 
begin
    if i < j then
        temp := i;
        i := j;
        j := temp; -- 直接交换
    end;
end;

需要注意的是，procedure和function的区别是：

  • 前者没有返回值，而是直接在原地进行处理。也就是说传入的两个参数，是传址的，不是传值
  • 后者是传回一个值的，需要有接收者。

具体的用法可以参考Murphi手册

初始状态

1
2
3
4
startstate
	m := a;
	n := b;
end;

运行结果

用murphi的-ta 执行.o 程序，就会打印出各个状态。

最后结束会出现死锁，可以用-ndl选择不打印死锁。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
State 1:
n:12
m:20

State 2:
n:8
m:12

State 3:
n:4
m:8

State 4:
n:4
m:4

分析

我们把各个状态（辗转相除的每个步骤）都列出来看看：

m n
20 12
12 8
8 4
4 4

可以看到，最后终止的时候，m == n，而且每一步都满足m>n。这样我们就可以提取出两个关键的循环不变量：（其实可以看作是一个）
$$
\forall m, n, m \geq n: f(m,n) = f(n, m-n)
$$

$$
\forall m, n, m < n: f(m,n) = f(m, n - m)
$$