Code: Getting it Right A new OS has been proven to be correct using mathematical proofs. The cost: astronomical. By Jack Ganssle Embedded.com (10/26/09, 02:28:00 HΠEDT)http://www.embedded.com/columns/breakpoint/220900551

Programming logic is a framework or system to prove properties of programs. Hoare logic is the representative basic theory, and certified programming is the technique/method for the programming logic. Hence "Programming language" and "prog…

Proof theory, also called metamathematics, is the study of mathematics and mathematical reasoning (Hofstadter 1989) in a general and abstract sense itself. Instead of studying the objects of a particular mathematical theory, it examines th…

「The difference between “theory” and “practice” is that in theory there is no difference between theory and practice, but in practice, there is.」 by Jan L. A. van de Snepscheut, a professor at Caltech.

バージョン管理ソフトウェアに，tortoisesvn を使用している．tortoisesvnはGUIを備えているのでとても便利．ただ今回，Windows の tortoisesvn でログに残すメッセージ部分を編集できないというトラブルに見舞われた．これに対し，以下のページを参考にする…

> runhaskell Setup.hs configure > runhaskell Setup.hs build > runhaskell Setup.hs install

Join calculusThe Join-calculus is a process calculus invented by Fournet and Gonthier, as an 'extended subset' of the asynchronous Pi-calculus, making the latter - offering a practically attractive basis for modelling concurrent and distri…

概要 型クラスとは型に関する性質を規定するための概念・仕組みである．型クラスを用いると，型に多相型の制約をつけることができる.つまり，ある型クラスが割り当てられた変数には，その型クラスの性質をもつ型によってのみ型付けができる． 型クラスは「ク…

in silico - Wikipediain silico（イン・シリコ）は、in vivo や in vitro などから派生して作られた用語で、「シリコン内で」というニュアンスであるが、実際の意味は「コンピュータを用いて」というものである。分子生物学などの実験や測定は通常、ウェッ…

Bisimulation - Wikipedia BisimulationIn theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other an…

Agda で入出力を扱う場合，Agda の FFI（Foreign Function Interface）を通し，Haskellの入出力関数を用いておこなう．実際に，「Hello, World」プログラムをAgdaで作成してみた．ちなみに，入出力をおこなうには，コンパイルしておこなう必要がある．詳細は…

Transition systems \not= finite automata there are no accept states set of states and actions may be countably infinite may have infinite branches actions may be subject to synchronization (concurrency)

http://www.google.co.jp/url?sa=t&source=web&ct=res&cd=2&url=http%3A%2F%2Fwww-i2.informatik.rwth-aachen.de%2FTeaching%2FCourse%2FPMC%2F2005%2Fpmc_lec1.pdf&ei=kbXISujQHYTq6gPl_dHwBA&usg=AFQjCNG1H8ss7A-Xogei2hgLSW6ctlaaKg&sig2=GvrtKwAJMrutnJT…

cited from http://www.b-core.com/ZVdmB.html - We are frequently asked to compare the AbstractMachine Notation (AMN) of the B-Method with Z and VDM. We have chosen the following points of comparison:- Underlying Logic Z and AMN are based in…

Abstract state machine - WikipediaAbstract state machinesFrom Wikipedia, the free encyclopediaIn computer science, an abstract state machine (ASM) is a state machine operating on states which are arbitrary data structures (structure in the…

Model Checking Abstract State Machines Kirsten Winter (著) Model Checking Abstract State Machines作者: Kirsten Winter出版社/メーカー: VDM Verlag発売日: 2008/05/30メディア: ペーパーバックこの商品を含むブログ (1件) を見る Product Description…

Formal Software Development: From VDM to Java作者: Quentin Charatan,Aaron Kans出版社/メーカー: Red Globe Press発売日: 2003/09/09メディア: ペーパーバック クリック: 2回この商品を含むブログ (2件) を見る Contents Preface xi 1 High Integrity So…

Hoare's logic and VDM http://www.springerlink.com/content/mk583100700h6ux0/by J. Coenen1 ContactReceived: 15 August 1993 Accepted: 15 March 1994 Abstract A relational framework which unifies Hoare's logic and VDM is presented. Within this …

Carl Friedrich Gauss referred to mathematics as "the Queen of the Sciences". Mathematics is the queen of science and the king of arts Mathematics is the queen of the sciences and number theory is the queen of mathematics. Gauss called math…

from : http://en.wikipedia.org/wiki/Formal_system In formal logic, a formal system (also called a logical system,[1] a logistic system,[1] a logical calculus,[2] or simply a logic[1]) consists of a formal language together with a deductive…

Set-theoretic specifications, which are also knows as "model-based specifications" or "model-oriented specifications" , model systems using sets which are either considered to be primitives sets or constructed by means of combinations of p…

cited from: http://e-words.jp/w/E38397E383AAE382A8E383B3E38397E38386E382A3E38396E3839EE383ABE38381E382BFE382B9E382AF.html プリエンプティブマルチタスクとは、一台のコンピュータで同時に複数の処理をこなすマルチタスク処理の実現方法のうち、CPUを…

The main components of B-method First-order logic (similar to Z); Set theory (similar to Z); Integer arithmetics (similar to Z); Generalized substitutions (specific of B). from Tutorial: Software Engineering with the B-Method http://www.co…

Specifications are not (necessarily) executableAbstract : Specifications can be written in languages which have formal semantics. Their very formality, and the similarities with some aspects of implementation languages, invites the idea th…

from http://en.wikipedia.org/wiki/Larch_(disambiguation)The Larch family of formal specification languages are intended for the precise specification of computing systems. They allow the clean specification of computer programs and the for…

The model-based approach to software specification is arguably the most popular style of formal software specification going today, both VDM and Z being based on this style [Hayes, Jones • Nicholis]. A model-based specification provides a …

Universal algebra From Wikipedia, the free encyclopedia http://en.wikipedia.org/wiki/Universal_algebraUniversal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures themselves, not exampl…

チューリング完全 出典: フリー百科事典『ウィキペディア（Wikipedia）』 移動: メニュー, 検索計算理論で、あるプログラミング言語がチューリング機械と同じ計算能力をもつとき、その言語はチューリング完全（チューリングかんぜん、Turing-complete）ある…

大規模開発におけるモデル品質向上のためのモデル検証フレームワーク 本論文は，UML モデルの品質確保のためのモデル検証において，プロジェクト固有のモデリング・ルールを容易に定義・検証できるモデル検証フレームワークを提案する．本フレームワークでは…