Windows GHC でText.regex を使おうとすると，regex-posix モジュールをロード時に次のようなエラーがでる． Loading package regex-posix-0.94.2 ... linking ... done. regex-posix はregex-posix-0.94.4 をインストールしているのだが，なぜか古いほうの …

CNF を自動計算するモジュールがほしかったのだけど，なかなか見つからなくて，ProcLogic にいきついた．ただProcLogic がバグだらけで理想どおりに使おうとすると苦労したんだけど，とりあえず以下のように書くととりあえず，できたので，メモ程度に残して…

そもそもテストとは何なのか？テストを一言で言うのは難しい．なぜなら，テストはいくつかの側面をもつからである．以下にテストが果たす役割の側面について考える．論文や新しいテスト技法を考えた時には，それがテストのどの側面に貢献するものなのかをこ…

Definition [Positive Normal Form (release PNF)]For a ∈ AP, LTL formulae in release positive normal form (release PNF, or simply PNF) are given by ϕ ::= true | false | a | ¬a | ϕ ∧ ϕ | ϕ ∨ ϕ | ○ϕ | ϕ U ϕ | ϕ R ϕ

Agdaのインストーラは非常に良くできていて，インストールするとAgdaのほか，GHC，Emacs やEmacsのHaskell-modeまで入ってくる．これはAgdaをインストールする上では非常に便利である．しかし，Agda インストール時にインストールされたEmacsからHaskll（GHC…

Haskell/Polymorphism - Wikibooks, open books for an open world 型システムはその表現力に関して、rank-1, rank-2, rank-n として分類されるのだそうだ。一般に rank-n type とは、少なくともひとつのrank-(n-1の引数を持ちかつそのランクより高い引数は…

Haskell でPolymorphism をふと調べてみたら、ちょっと面白いことを発見。Haskell では、たとえば、リストの長さを返す関数を書くときに以下のように書く。 length :: [a] -> Int これは Polymorphic 函数で、a であらわされる型にはさまざまな異なる型が入…

"Property Specification Patterns for Finite-State Verification" Matthew B. Dwyer Kansas State University, Department of Computing and Information Sciences, 234 Nichols Hall Manhattan, KS George S. Avrunin University of Massachusetts, Depar…

Feature model はソフトウェアプロダクトライン（Software Product Line:PLE）への要素 ソフトウェアプロダクトラインとは？ 昨今のソフトウェア開発におけるトレンドは複数の似通ったソフトウェア製品を開発する必要性である。たった一つの個別の製品を作る…

Feature model Feature model is a technical method for product line engineering. Product line engineering addresses the problem of efficient system development. In order to meet the demand of constraints on software system development which…

A feature [C&E 4.9.1] is "anything users or client programs might want to control about a concept. Thus, during feature modeling, we document no only functional features ... but also implementation features, ..., various optimizations, alt…

The hub and spoke model is a system which makes transportation much more efficient by greatly simplifying a network of routes. It is extensively used in commercial aviation for both passengers and freight, and the model has also been adopt…

weakest precondition For some given program statement S and some postcondition R there is a (possibly empty) set of program states such that if execution of S is initiated from one of these states then S is guaranteed to terminate in a sta…

In computer programming, particularly functional programming and type theory, an algebraic data type (sometimes also called a variant type[1]) is a datatype each of whose values is data from other datatypes wrapped in one of the constructo…

In computer programming languages, a recursive data type (also known as a recursively-defined, inductively-defined or inductive data type) is a data type for values that may contain other values of the same type. Data of recursive types ar…

Theorem: The Cartesian product of finitely many countable sets is countable.

.emacs に以下を追加する． ;; (require 'linum) ;; emacs 起動時にデフォルトで行番号を表示 (global-linum-mode) ちなみに，Emacs を起動してから行番号を表示する際には M-x linum-mode

代数にも論理学にも公理という概念がある．正確に言うと，代数構造を設計すると言うのは，公理系を設計することである．例えば，Bool 代数とか，・・・とか．それらのソフトウェア開発におけるプログラミング・モデリングの際の意味の違いは以下の通り．代数…

Jan Rutten の Universal coalgebra: a theory of systems によると Jan Rutten's Universal coalgebra Abstract: In the semantics of programming, finite data types such as finite lists, have traditionally been modelled by initial algebras. Later…

振る舞いを公理として記述する記述の方法論． 実装としては，OBJやMaude, CASL が有名．

データ型の数学基礎理論として代数は、プログラミング／モデリングにおける最も基本的な代数の使い方である。ここではまず、データ型の数学基礎理論として代数を見る。 1. まず、代数データ型とは データ型と代数データ型（Algebraic Data Type）Wikipediaに…

＃本稿は素人が書いたメモですので，間違いだらけなのをあらかじめご承知ください．また間違いがあればご教示ください代数はプログラミング／モデリングの数学的な基礎理論になっているようである．ここでは，代数とはなんだろうか，さらにそれがどのように…

先ほど「SPIN にはNext-0Step 演算子 (X) はない？ - x76789の研究メモ」の続きです．色々調べると，SPIN でも Next-0Step 演算子 (X) が使えるそうです．Promela Reference -- ltlの下のほうのNoteに書いてありました．基本的に，SPINのLTL構文にはNext-0St…

SPIN では，Next Step Operator (X) は使えないらしい．以下はそのSPIN開発者らによる言及． Spin Run-Time Optionsによれば， Spin Run-Time Optionsによれば，SPINには，Next Step Operator (X) がないらしい．なんでも， partial order reduction と互換…

What is the relationship between induction and algebra? What is the relationship between formal proof and induction? structural induction is a proof method to prove object x, which is recursively defined, has some property p

モデル検査器 Spin の動作実験 1. モデルの作成 まず検査対象のモデルを作成する．モデルは Promela と言う言語で作成する．ここでは，例えば，以下のようなOn とOff を繰り返すトグルスイッチのPromela コードを用意した．このコードを switch.p として適当…

Communicating Process Architecture for Multicores. David May. Bristol University and XMOS.

Transputer T425のFPGAへの実装 「より強力な並列処理Processorを目指して」 東京都立大学大学院理学研究科物理学専攻 計算システム物理研究室 大木豊、福地直也、田中誠、福永力

記号的に扱ったり、抽象的に扱うのにも限界ってものがあります。 うまくやれば 10^20 とか 10^1300 くらいのオーダーの状態数でも扱えますが、 無制限に状態数が増えるとすぐに限界が来ます。 http://www.epics.jp/mc/modelchecking.html 10種類の値を取り得…

テストベッドとは、大規模なシステム開発で用いられる、実際の運用環境に近づけた試験用プラットフォームの総称である。テストベッドは、実際に運用されているシステムを危険にさらすことなく、実際の運用体制に近い状況で稼動させる目的で用いられる。http:…