2009-09-01から1ヶ月間の記事一覧

Model Checking Abstract State Machines

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

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

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 …

Mathematics is the queen of science (and the king of arts)

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…

formal system

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…

Summary of Set-theoretic Specifications (tentative)

CS

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…

プリエンプティブマルチタスク

IT

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

The main components of B-method

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) executable

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…

Larch family (computer specification languages)

CS

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…

Model-based Specification

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)

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 モデルの品質確保のためのモデル検証において,プロジェクト固有のモデリング・ルールを容易に定義・検証できるモデル検証フレームワークを提案する.本フレームワークでは…