.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:…