TrueLogic 仕事日記 このページをアンテナに追加 RSSフィード

2010-02-12Principles of the Spin Model Checker P108の脚注

"Principles of the Spin Model Checker" P108の脚注で言及されている問題について,最新バージョンでは修正されていることを確認した.

シミュレーションモードでは検出されない点に注意のこと.

bash-3.2$ ./spin -V
Spin Version 5.2.4 -- 2 December 2009

bash-3.2$ ./spin p108.pml
     timeout
#processes: 3
 2:    proc  2 (P) line   5 "/Users/nonaka/SpinBookTest/p108.pml" (state 1)
 2:    proc  1 (P) line   5 "/Users/nonaka/SpinBookTest/p108.pml" (state 1)
 2:    proc  0 (:init:) line  11 "/Users/nonaka/SpinBookTest/p108.pml" (state 3) <valid end state>
3 processes created

$ ./spin -a p108.pml
$ cc -o pan pan.c
$ ./pan
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan: too few parameters in send stmnt (at depth 2)
pan: wrote foobar.pml.trail


bash-3.2$ cat p108.pml
chan ch1 = [0] of {byte};
chan ch2 = [0] of {byte, byte};

proctype P(chan c){
 c ! 5
}

init {
 run P(ch1);
 run P(ch2)
}
トラックバック - http://specverification.g.hatena.ne.jp/n757uf/20100212

2010-01-31 Real World Haskell 第3章の練習問題

第3章の練習問題(P72)をやってみた.

1.リストの長さ

myLength :: [a] -> Int
myLength [] = 0
myLength (x:xs) = 1 + myLength xs

2. そのテストプログラム

testLength :: [a] -> String
testLength l
  | length l == myLength l = "OK"
  | otherwise = "NG"
                
-- testLength []
-- testLength [1,2,3,4,5]

3.リストの平均値

sumList :: [Double] -> Double                
sumList [] = 0
sumList (x:xs) = x + sumList xs

aveList :: [Double] ->  Double
aveList a = (sumList a) / fromIntegral (myLength a)

-- aveList [3,4]

4. 回文をつくる

myKaibun :: [a] -> [a]
myKaibun  = 
myKaibun (x:xs) = [x] ++ (myKaibun xs) ++ [x]

5. 回文の判定

myKaibunHantei :: [Char] -> String
myKaibunHantei [] = "OK"
myKaibunHantei (x:[]) = "OK"
myKaibunHantei (x:xs) =
    if x == (last xs)
    then myKaibunHantei (init xs)
    else "NG"

n757ufn757uf2010/02/12 16:49メーリングリストで頂いたコメントをメモしておきます.
--
リストが空かどうかを判定するには、少なくとも二つの方法があります。
(1) 空リスト [] でパターンマッチ
(2) 関数 null :: [a] -> Bool で判定

パターンマッチは遅延評価されることもあり、(2) のほうが
(1)よりも計算時間の意味で効率的です。特に、文字列など
で顕著に差が現れるので、知っておくといいでしょう。

--
foldrパターンが使える(これは高度だな)

myLength :: [a] -> Int
myLength = foldr (\x y -> y + 1) 0
= foldr (const (+ 1)) 0
--
これはエレガント!

isKaibun :: String -> Bool
isKaibun xs = xs == reverse xs

トラックバック - http://specverification.g.hatena.ne.jp/n757uf/20100131

2009-11-30 ε-δのトレーニング

トラックバック - http://specverification.g.hatena.ne.jp/n757uf/20091130

2009-11-02

Real World Haskellを購入

これで実用的なHaskellプログラムを書けるようになりたいものです.今のプロジェクトに使えるようがんばります.

トラックバック - http://specverification.g.hatena.ne.jp/n757uf/20091102

2009-07-25Redmineを導入してみる

挙動がおかしい(新規チケットの発行やチケットの変更で異常に時間がかかる)のでいろいろ調べ回ってみた. FAQ*1でそれらしいものが見つかった.どうやら原因はこれのようだ.月曜日に試してみよう!

Q:When I create a new issue, Redmine freeze during one minute.

Make sure your SMTP server is properly configured or desactive email notifications (remove config/email.yml) and restart redmine.
トラックバック - http://specverification.g.hatena.ne.jp/n757uf/20090725