いいかげんな要求仕様を自動的にチェックする．

論文

CSVとか，RDBとか，XMLとかいろんなデータの寄せ集めにおいて，データの整合性をチェックする仕組みを模索していたら，「いいかげんなデータの整合性をチェックする」手法ではなくて「いいかげんな要求仕様の整合性をチェックする」手法がひっかかった．

Handling non-canonical software requirements based on Annotated Predicate Calculus
Knowledge and Information Systems
http://www.springerlink.com/content/5351217j00qh3183/?p=6e574e8eb36d455db44d1c6ad3a1bc5c&pi=3

Annotated Predicate Calculus

なんか，普通の論理式P の後ろに :t とか :f とか :T ， :⊥ ， :fp ， :tp などをつけて

  • P:t Pは必ず真
  • P:f Pは必ず偽
  • P:T Pは矛盾する
  • P:⊥ Pかどうかわからん
  • P:tp Pは真になることがある
  • P:fp Pは偽になることがある

というアノテーションをつける論理計算らしい

例：
図書館システムの例

  • ほとんどの場合，本が予約されていたら，予約した人がその本を借りることになる
    • Reserve(User,Book):t => Borrow(User,Book):tp
  • 今のところ，利用者が延滞している場合に通知するかについては規定がない
    • Borrow(User,Book):t ^ Overdue(Book):t => Notify(User,Book):⊥

「わからん」というのを論理体系にもってくるのは面白いけど，役に立つのかな？

要求仕様とシナリオとテストケース

Annotated Predicate Calculus を評価実験するための枠組み

  • 要求仕様
  • シナリオ（＝"入力"と"期待する出力"：テストケース？）

が与えられた時に，要求仕様を「必要」「有用」「不要」に分類する．

サンプルシナリオ

これを使ってこんな要求仕様とシナリオを作ったらしい．

住宅の駐車場に車が入ってよいかどうかを判断するシステム

要求仕様：

1) 管理人が特別に許可した車は入ってよい
2) 管理人は業務用車輌は許可する
3) 普通，許可された車にはシステムによって自動的にガレージが割り当てられる
4) 普通，業務用車輌にはガレージが必要である

1) Authorized(V):t => Enter(V):t
2) Logistics(V):t => Authorized(V):t
3) Authrized(V):t => Garage(V):tp
4) Logistics(V):t => Garage(V):tp

シナリオ：

input: Logistics(ダンプカー):t
expected output: Garage(ダンプカー):tp

この場合， 1) は「不要」 4) は「有用」だが「必要」ではない（2と3があれば導けるから)

「だから，1と4は要求仕様から消してよい」....て書いてあるんだけど，車が入ってよいかどうか判断できなくなるけどいいのか？

他にも，車を割り当てたガレージに対して，

9)壊れたガレージは修理する必要がある
10)普通，耐用期限が過ぎたガレージは修理する必要がある

9) Distributed(G):t ^ Damaged(G):t -> Maintain(G):t
10) Distributed(G):t ^ Expired(G):t -> Maintain(G):tp
※ Distributed(G) : Gは車が割り当てられているガレージである

という要求仕様を追加して

「この要求仕様の欠点を洗い出すために，こういうテストケースを考えました」

input: not Distributed(G3) :t ^ Damaged(G3) :t
output: Maintain(G3): t

「でも，これだけからは Maintain(G3): ⊥ （G3は修理していいかどうか不明）
となって，テストに失敗します」

「ほら，こうやってシステム開発者にガレージの種類（Distributed(G)かどうか？）
をチェックさせることを思い出させるでしょ」
で評価の章がおわっている

....うーん，なんかさっぱり有用性がわからん．

1000万件のデータと闘うには

仕事で1000万件超のデータを扱っているという知り合いから，データベースについていろいろと聞いてみた．

データベースを速くするコツは?

DBサーバとアプリケーションサーバを分けると24時間かかっていたものが2時間になった
おそらく，1つのタスクに集中したほうがキャッシュのヒット率があがるから？

Materialized View

いくら1000万件の生データをもっていても，それら直接扱うことはやっぱり稀らしい．普段は集計済みのデータを扱うらしい．
集計内容と生データは整合性がないといけない．でもViewを使うのは遅い，というときには
Materialized View というものがあるらしい．簡単にいうとクエリの結果を特定のテーブルにとっておいて，たまに更新をかける，というもの．

Oracle には create materialized view があるらしい．

http://www.akadia.com/services/ora_materialized_views.html

 create materialized view mv_bigtab
   build immediate
   refresh on commit
   enable query rewrite
 as
 select owner, count(*)
   from bigtab
  group by owner

MySQL では，単に Insert into .. を使ってテーブルを作る，のをストアドプロシージャに登録しておくことで実現する

http://www.shinguz.ch/MySQL/mysql_mv.html

サブクエリ

Select文をネスト（サブクエリ化）しまくることもある．そのほうが何度もクエリを発行するより速いらしい．

サブクエリの例を挙げてみる．

http://www.techscore.com/tech/sql/07_01.html 

  SELECT 受注番号 FROM 受注表
         WHERE 商品コード IN
         (SELECT 商品コード FROM 商品表
          WHERE 単価 = 400);

Java脳の人がこのクエリを実現しようとすると，

Set codes=(SELECT 商品コード FROM 商品表
                    WHERE 単価 = 400);
for (Integer bango in (SELECT 受注番号 FROM 受注表)) {
   if (codes.contains(bango)) {
         ...
   }
}

なんていうコードを書きかねない．Java脳，というか手続き脳の人は
「WHERE判定を行うたびに中のサブクエリを毎回実行してんじゃないのか」，つまり

for (Integer bango in (SELECT 受注番号 FROM 受注表)) {
   Set codes=(SELECT 商品コード FROM 商品表
                       WHERE 単価 = 400);
   if (codes.contains(bango)) {
         ...
   }
}

なんじゃないかと思い込んでいる．さすがにSQLはその辺は面倒みてくれているらしい．

Java脳が書いたクエリ＋プログラムを1個のクエリに自動統合する仕組みがあるといいかもしれない．

他にも Order by，Group By ，Union，Distinct などの機能はSQLに任せたほうがだんぜん速い．Group By をJavaのハッシュや集合で実現するような真似はしないこと．

Union の賢い使い方

  a  b  c
  T  1  X
  T  2  Z

と

  a  b  d
  T  1  Y
  S  1  P

をUnionすると

  a  b  c  d
  T  1  X  Y
  T  2  Z
  S  1     P

となるらしい

テーブルのスキーマが変わるときは

テーブルをDropしてCREATEするか，Insert intoするか，EXPORT&IMPORTする．ALTER TABLE は使っても結局時間がかかるらしい（1000万件に新しい列を追加するのはすごいコスト）．

もちろん，その間はDB更新をとめる必要がある．EXPORT中にDBを更新
したい場合は，....そんなのは想定したことないらしい．差分管理でがんばれ？

OracleのBitmapインデックス

http://www.intersystems.co.jp/support/cache_50/csp/rsql/rsql_createindex.html

たぶん，全文検索における「逆インデックス」のことだと思う．

  • 犬
  • 猫
  • 犬
  • 猫
  • 猫

というデータがあったら 犬= 10100 猫=01011 という値をもたせておく．

正規形とビジネスモデル

だいたいのテーブルはボイスコッド正規形くらいまで行うらしい．

第3正規形まではツールが自動的に行うが，n>=4 の場合，ビジネスモデルを知らないと，それが第n正規形かどうかの判定すらできない．

例えば， 時間帯がかぶる指定席券はとれるが， 同じ時限の授業はとれないとか，
生徒と先生と科目名というテーブルがあった場合に「フェルマー先生の物理」や「アインシュタイン先生の数学」というデータがありうるが，実際にはそんな授業はない．「存在しうる組み合わせを示すテーブル」まで用意すると第5正規形になる．

集計による高速化


MATERIALIZED VIEWの応用バージョン？ 1000万件の収支データ（細目）があったときに，それらをまともに検索したくないときは，1年以上前の決算について「その他」品目で，月ごとの合計値のみをもたせ，1年以上前の詳細は別テーブルにもたせて普段はさわらない，という構成でだいぶ速くなった．

On Type Systems for Object-Oriented Database Programming Languages

from ACM Computing Surveys (CSUR).

サーベイ論文というのは名前には聞いていたがこれくらい徹底してやるものだったとは．

いろんな言語における型の健全性を調べているのだが

  • データベースの側面から，どういう型の性質が求められているか
  • オブジェクト指向の側面から，どういう型の性質が求められているか

というのを論じたあと，10個のテストプログラムを用意している．名前だけ挙げてみる

  • PERSON
  • POINT
  • COMPARABLE
  • STREAMS
  • SORT
  • GENSORT
  • LIST
  • SET
  • APPLY
  • BROWSER


例えばSTREAMSテストはこんなの：

 class InputStream { ... }
 class Point {}
 class ColoredPoint extends Point {}
 ColoerdPoint cp;
 Point p;
 InputStream ps;
 InputStream cps;
 p =ps.read(); //1 Should be passed
 cp=ps.read(); //2 Should be compile error
 p =cps.read();//3 Should be passed
 cp=cps.read();//4 Should be passed

Javaだと， //3 のところがコンパイルエラーになるので失格．というかJavaは10個のテストのうち9個に失格している．

こんな感じで，10個のテストを，36個ぐらいの言語について行っている（つまり360回テストしている）という内容．

気になるのは優勝者（一番テストに合格した言語）だけど，TransframeとMini-Cecil が9個でトップ．おめでとう！って誰？

Functional Reactive Programming

Dynamicの機構の似ているような違うような機構でFunctional Reactive Programming というものもある．
電子回路とかロボット制御に使われているらしい．ある瞬間における電圧とかアームの位置とかを，時間t の 微分方程式で表現するそうだ

Functional Reactive Programming (FRP) is a framework for reactive programming in a functional setting. FRP has been applied to a number of domains, such as graphical animation, graphical user interfaces, robotics, and computer vision.

ところで，Reactive Functional Programming を使ってコンパイラを作る酔狂な方はいないのか．

Compiler :: [Source] -> ([Binary], [Error])

[Source] の一部が変わったら，[Binary] や [Error] の一部が変わる，というコンパイラが簡単に作れそうだ

MathematicaのDynamicがすごくExcelぽい振る舞いをしています

例の代入可能な関数型言語について，

Mathematica は Dynamic と書くと自動的に値の更新を検出するらしい，要するにExcelぽくふるまうらしい

一度標準出力(?)に表示した値があとから変化する．このダイナミックさはSqueakを思い出す．

In[1]:= x=3
Out[1] := 3
In[2]:= Dynamic[x]
Out[2] := 3

In[1]:= x=3
Out[1] := 3
In[2]:= Dynamic[x]
Out[2] := 5 <---- ここも変化!
In[3]:= x=5
Out[3] := 5


本家の解説
http://reference.wolfram.com/mathematica/tutorial/IntroductionToDynamic.html

アドレス情報を保持するコンパイラ

宣言された変数に対して，順番にアドレスを確保していくコンパイラ

Parse> r "var a; var b; a=3; b=a+2;"
Loading package parsec-2.0 ... linking ... done.
Found value[ ["VarDecl","0"],
["VarDecl","1"],
["0","3","=","POP"],
["1","0","Read","2","+","=","POP"] ]
Parse>

昨日のMap.hsが別途必要です

module Parse where
import Text.ParserCombinators.Parsec
import Data.HashTable
import Map

 --main
r :: String -> IO ()
r input = 
   case runParser source (PStat 0 []) "lisp" input of
     Left err  -> putStrLn $ "No match: " 
                  ++ show err
     Right val -> putStrLn $ "Found value" 
                  ++ (show $ map (toCode RVal) val)

newSym = new (==) hashString :: IO (HashTable String Int)
 --util
data ParserState = PStat Int [(String,Int)]
getNum :: ParserState -> Int
getNum (PStat i _) = i
getSyms :: ParserState -> [(String,Int)]
getSyms (PStat _ h) = h

type SParser a = GenParser Char ParserState a

mny :: SParser a -> SParser [a] 
mny p = many (do { spc; p } )
toks1 :: SParser Char -> SParser String 
toks1 p = do {res<-many1 p ; spc; return res } 

spc :: SParser ()
spc = skipMany space

tok :: String -> SParser String
tok str = do { s <- string str; spc ; return s }

 --grammar
source :: SParser [Decl]
source = do { bodies <- mny ( vardecl <|> statement)
            ; return bodies 
            }

vardecl :: SParser Decl

変数宣言をして，変数のアドレスを割り当てている部分．
ここで使っているlet は，ふつけるP279 にある「特別なlet節」．実はうっかりinを書き忘れたことで偶然みつけた．便利．

vardecl = do { tok "var" 
             ; name <- symbol; tok ";"
             ; st <- getState 
             ; let syms = getSyms st 
             ; let addr = getNum  st 
             ; setState (PStat (addr+1) 
                               (put syms name addr))
             ; return $ VarDecl name addr 
             } 



statement :: SParser Decl
statement = do { e <- expr
               ; tok ";"
               ; return $ StmtDecl $ ExprStmt e
               }


expr :: SParser Expr
expr = do {
         left <- add ;
         option left (do {
             tok "=" ; a<-add ;
             return (BinOp left "=" a) 
         })
       }
add = do { left <- element
          ; rights <- mny (do { op   <- operators 
                              ; e    <- element 
                              ; return (op,e) } )
          ; return (makeBinOp left rights)
          }
operators :: SParser String
operators = tok "+" <|> tok "-" 

element :: SParser Expr
element = intConst <|> varRef

ここは，変数を見て，その変数のアドレスを取り出しているところ

varRef :: SParser Expr
varRef = do {
   n <- symbol ;
   st <- getState ;
   return $ VarRef (defMaybe (-1) (get (getSyms st) n))
}
defMaybe:: a -> (Maybe a) -> a
defMaybe def (Just x) = x
defMaybe def Nothing = def 

intConst :: SParser Expr
intConst = do { v <- digits 
              ; return $ IntConst v 
              }

symbol  :: SParser String
symbol  = toks1 letter
digits  :: SParser Int
digits  = do { d <- toks1 (oneOf "0123456789")
             ; return (read d::Int)  -- ???
             }

 --semantics
makeBinOp :: Expr -> [(String,Expr)] -> Expr
makeBinOp left [] = left
makeBinOp left ((op,elem):rest) = 
   makeBinOp (BinOp left op elem) rest

data Decl = VarDecl String Int  |
            StmtDecl Statement  -- !
            
data Statement = ExprStmt Expr
			
data Expr = BinOp Expr String Expr |
            IntConst Int  |
            VarRef Int 
data CodeState = LVal | RVal

class ToCodable a where
     toCode:: CodeState -> a -> [String]

instance ToCodable Statement where
  toCode c (ExprStmt e) = (toCode c e)  ++ ["POP"] 
  
instance ToCodable Expr where
  toCode c (BinOp l "=" r) =
     (toCode LVal l) ++ (toCode RVal r) ++ ["="]  
  toCode c (BinOp l o r)   = 
     (toCode RVal l) ++ (toCode RVal r) ++ [o]
  toCode c (IntConst i)    = [show i] 
  toCode RVal (VarRef addr )  = [show addr , "Read"];
  toCode LVal (VarRef addr )  = [show addr ];

instance ToCodable Decl where
  toCode c (StmtDecl st)  = toCode c st
  toCode c (VarDecl name addr) = ["VarDecl", show addr]

しょうがないから作ってみた 

 module Map where
	put :: (Eq k) => [(k,v)] -> k -> v -> [(k,v)]   
	put  nk nv = [(nk,nv)] 
	put ((k,v):rest) nk nv = 
	    if (k==nk) then 
	        (nk,nv):rest
	    else 
	        (k,v):(put rest nk nv)
	     
	get :: (Eq k) => [(k,v)] -> k -> Maybe v
	get  k = Nothing
	get ((k,v):rest) k2 = 
	    if (k==k2) then
	        Just v
	    else 
	        get rest k

線形サーチなのでHashを名乗ることはできず．

Map> put [] 2 "bar"
[(2,"bar")]
Map> put [(2,"bar")] 3 "foo"
[(2,"bar"),(3,"foo")]
Map> get [(2,"bar"),(3,"foo")] 2
Just "bar"
Map> get [(2,"bar"),(3,"foo")] 5
Nothing
Map> put [(2,"bar"),(3,"foo")] 2 "baz"
[(2,"baz"),(3,"foo")]
Map>