Talk is cheap, show me the code.——Linus Torvalds

我將貼出一些來自《形式化驗證》課程中的一些作業，並且在程式碼之後會附著一些關鍵的講解。在我看來，看manual來學語言和思想，太慢了，看code學習才是最具效率的。

Natural Number

fmod PNAT is
    sort Nat .
    
    op 0 : -> Nat .  
    op s_ : Nat -> Nat .
    
    vars Y X : Nat .
    
    op _+_ : Nat Nat -> Nat [assoc comm] .
    op _*_ : Nat Nat -> Nat [assoc comm] . 
    
    eq 0 + X = X .
    eq s X + Y = s (X + Y) .

    eq 0 * X = 0 .
    eq s X * Y = (X * Y) + Y .
endfm

 

這是一個描寫了自己定義的實數型別，pnat。

op是operation的意思，表名一個操作。其中認為 0 是 Nat。 _ 代表是一個引數的。s_表示這個引數的後繼。很明顯，在實數範圍內，任意實數的後繼都是實數，自然數也是如此 assoc 表示結合律 comm 表示交換律 vars 聲明瞭兩個自然數的變數，X、Y eq是equation，用等式來定義了之前宣告的op sX代表變數X的後繼。

在maude中，用以下兩行程式碼來檢測加法和乘法。

red s 0 + s 0 0 .
red s s 0 * s s s 0 .

List

一個LIst的定義

fmod LIST-NAT is 
    protecting NAT .
    sort List-Nat .
    subsort Nat  < List-Nat .
    sort List-NatPair .
    
    op <_;_> : List-Nat List-Nat -> List-NatPair [ctor] .
    op nil : -> List-Nat [ctor] .
    op _,_ : List-Nat List-Nat -> List-Nat [ctor assoc id: nil] .

    var N : Nat .
    var LN : List-Nat .
    ---len
    op len : List-Nat -> Nat .
    eq len(N) = 1 .
    eq len(nil) = 0 .
    eq len(N,LN) = len(LN) + 1 .
    
    ---reverse
    op reverse : List-Nat -> List-Nat .
    eq reverse(nil) = nil .
---    eq reverse(N) = N .
    eq reverse(N,LN) = reverse(LN),N .

    ---sortList
    op sortList : List-Nat -> List-Nat .
    op LessEqN : Nat List-Nat -> List-Nat .
    op GreaterN : Nat  List-Nat -> List-Nat .
    
    eq sortList(nil) = nil .
---    eq sortList(N,LN) = sortList(LessEqN(N,LN)), N ,sortList(GreaterN(N,LN)) .   
    eq LessEqN(N,nil) = nil .
    var N1 : Nat .
    eq LessEqN(N,(N1,LN)) = if N1 <= N then N1,LessEqN(N,LN) else LessEqN(N,LN) fi .

    eq GreaterN(N,nil) = nil .
    eq GreaterN(N,(N1,LN)) = if N1 > N then N1,GreaterN(N,LN) else GreaterN(N,LN) fi .

    ---split
    op split : Nat List-Nat -> List-NatPair .
    eq split(N,nil) = < nil ; nil > .
    vars LN1 LN2 : List-Nat .
    ceq split(N,(N1,LN)) =
      if N1 <= N then
	  < N1 , LN1 ; LN2 >
  	else
	  < LN1 ; N1, LN2 > fi
       if < LN1 ; LN2 > := split(N,LN) .
      --- quicksort method
    ceq sortList(N,LN) =
	sortList(LN1) , N , sortList(LN2)
      if < LN1 ; LN2 > := split(N,LN) .
    
    
endfm
 

這個List就複雜多了，他實現了很多功能：

1. len函式，得到list的長度
2. reserve函式，翻轉當前的list
3. sortlist函式，給當期list排序，用的是快排的思想，這是重點
4. split函式， 是給sortlist服務的

這一段是茅詩劍同學的程式碼，他額外實現了insert，delete，change，get等功能。

fmod mylist is

	including NAT .
	sort ListNat .
	subsort Nat < ListNat .

	op nil : -> ListNat[ctor] .
	op _,_ : ListNat ListNat -> ListNat[ctor assoc id: nil] .

	op sortList : ListNat -> ListNat .
	op len : ListNat -> Nat .
	op revert : ListNat -> ListNat .
	op insert : ListNat Nat Nat -> ListNat .
	op delete : ListNat Nat -> ListNat .
	op change : ListNat Nat Nat -> ListNat .	
	op get : ListNat Nat -> Nat .

	vars N N1 N2 : Nat .
	var LN :  ListNat .

	eq len(nil) = 0 .
	eq len (N,LN) = len(LN) + 1 .
	
	eq revert(nil) = nil .
    eq revert(N,LN) = revert(LN), N .

	op lessEqN : Nat ListNat -> ListNat .
	op greaterN : Nat ListNat -> ListNat .
	eq lessEqN(N,nil) = nil .
	eq lessEqN(N, (N1,LN)) = if N1 <= N then N1,lessEqN(N,LN) else lessEqN(N,LN) fi .
	eq greaterN(N,nil) = nil .
	eq greaterN(N, (N1,LN)) = if N1 > N then N1,greaterN(N,LN) else greaterN(N,LN) fi .
	eq sortList(nil) = nil .
	eq sortList(N,LN) = sortList(lessEqN(N,LN)),N,sortList(greaterN(N,LN)) .
	
	eq get(nil,N) = nil .
	eq get((N,LN),0) = N .
	eq get((N,LN),s N1) = get(LN,N1) .
	
	eq change(nil,N,N1) = nil .
	eq change((N1,LN),N,0) = N,LN .
	eq change((N1,LN),N,s N2) = N1,change(LN,N,N2) .
	
	eq insert(nil,N,N1) = N .
	eq insert(LN,N,0) = N,LN .
	eq insert((N1,LN),N,s N2) = N1,insert(LN,N,N2) .
	
	eq delete(nil,N) = nil .
	eq delete((N,LN),0) = LN .
	eq delete((N,LN),s N1) = N,delete(LN,N1) .
	

	op sorting : ListNat -> ListNat .

    eq sorting(nil) = nil .
    ceq sorting(N,LN) =
	(sorting(LN1) , N , sorting(LN2)) 
      if < LN1 ; LN2 > := split(LN, N) .
    
    sort ListNatPair .
    op <_;_> : ListNat ListNat -> ListNatPair .
    
    op split : ListNat Nat -> ListNatPair .
    eq split(nil, N) = < nil ; nil > .

    var N' : Nat .
    vars LN1 LN2 : ListNat .
    
    ceq split((N', LN), N) = 
	(if N' <= N then < (N', LN1) ; LN2 >
	  else < LN1 ;  (N', LN2) > fi) 
    if < LN1 ; LN2 > := split(LN, N) .

endfm

 

BinarySearchTree

一顆二叉搜尋樹，左兒子比父親小，右兒子比父親大。

fmod BST is
    including NAT .
    sort BinaryTree .
    sort BinarySearchTree .
    subsort BinarySearchTree < BinaryTree .

    op et : -> BinarySearchTree .
    op <_,_,_> : Nat BinarySearchTree BinarySearchTree -> BinarySearchTree .

    var N : Nat .
    vars L R : BinaryTree .

    cmb < N, L, R > : BinarySearchTree
      if L =/= et /\
         L :: BinarySearchTree /\
         rightmostNode(L) < N .

    cmb < N, L, R > : BinarySearchTree
      if R =/= et /\
         R :: BinarySearchTree /\
         leftmostNode(R) > N .
     
    cmb < N, L, R > : BinarySearchTree
      if L =/= et /\
         R =/= et /\
         L :: BinarySearchTree /\
         R :: BinarySearchTree /\
         rightmostNode(L) < N /\
         leftmostNode(R) > N .

    mb < N, et, et > : BinarySearchTree .

    ops leftmostNode rightmostNode : BinaryTree -> Nat .
    op errorNat : -> [Nat] .
    eq rightmostNode(et) = errorNat .
    eq rightmostNode(< N, L, R >) =
	if R == et then N else rightmostNode(R)
      fi .

    eq leftmostNode(et) = errorNat .
    eq leftmostNode(< N, L, R >) =
       if L == et then N else leftmostNode(L)
       fi .
endfm

以下是一些重點。

 cmb < N, L, R > : BinarySearchTree
      if L =/= et /\
         L :: BinarySearchTree /\
         rightmostNode(L) < N .

cmb代表是一個condition membership，是有條件的成員定義，定義如果L不等於空並且L是BinarySearchTree，並且 rightmostNode(L) < N，此時，< N, L, R > 是一個 BinarySearchTree。 兩個冒號一般是型別判定，類似於c++中的“==” 一個冒號表示型別的確定，類似於c++中的“=”

在理解cmb後，mb就很簡單了，就是一個無條件的成員定義。定義了< N, et, et >一定是BinarySearchTree。

可以用以下程式碼來測試：

red leftmostNode( < 5 , < 3 , et ,et > , < 7 , et , et > > ).

red (< 5, < 3, et, et > , < 6, et, et > > ) :: BinarySearchTree .

Square Root Calculations

兩種來平方根的演算法，第一種就是傻愣愣的遞增，找到平方根，第二種則使用的二分的方法。

fmod SQRT is
    including NAT .

    op sqrt : Nat -> Nat .
    op sqrt' : Nat Nat -> Nat .
    vars N N' : Nat .

    eq sqrt(N) = sqrt'(N,0) .
    eq sqrt'(N,N') =
      if N' * N' <= N and N < (N' + 1) * (N' + 1)
	then N'
	else sqrt'(N, N' + 1)
	fi .

    op sqrt2 : Nat -> Nat .
    op sqrt2' : Nat Nat Nat Nat -> Nat .
    op pivot : Nat Nat -> Nat .
    vars L R X : Nat .

    eq sqrt2(N) = sqrt2'(0,N,pivot(0,N),N) .
    eq sqrt2'(L,R,X,N) = (if L == R
	then L
	else (
	  if X * X > N
	    then sqrt2'(L, sd(X,1) , pivot(L,sd(X,1)), N)
	    else sqrt2'(X,R,pivot(X,R),N)
	    fi)
      fi) .
    
    eq pivot(L,R) = (if (sd(R,L) divides 2) == false
	  then  (sd(R,L) quo 2 + L)
	  else  ((sd(R,L) + 1) quo 2 + L)
	    fi) .
    

endfm
    

sd(a,b) 表示a-b x divides y表示x mod y，返回bool值，整除為true，其他為false(這裡坑了我很長時間，多虧問了張民老師……) 使用以下程式碼來測試程式

red sqrt(100) .
red sqrt2(100) .