ブラウザよりも高速アクセス！
63 関係: ALGOL、Alloy Analyzer、Association for Computing Machinery、型システム、契約プログラミング、工学、代数的データ型、仕様及び記述言語、仕様記述言語、形式仕様記述、形式体系、形式的検証、形式言語、ペトリネット、ハードウェア、バッカス・ナウア記法、モデル検査、ユースケース、プログラミング言語、プログラム (コンピュータ)、プログラム意味論、プロセス計算、テイラーアンドフランシス、フレデリック・ブルックス、ドナルド・クヌース、アルゴリズム、アクターモデル、オートマトン、オブジェクト指向モデリング、シュプリンガー・サイエンス・アンド・ビジネス・メディア、ジョン・バッカス、ソフトウェア、ソフトウェア危機、ソフトウェア工学、ソフトウェア設計、ソフトウェア開発、ソフトウェア開発工程、公理的意味論、B-Method、Communicating Sequential Processes、理論計算機科学、神託機械、Esterel、銀の弾などない、領域理論、表示的意味論、表明、複雑性、証明、詳細化、...、論理学、航空宇宙工学、自動定理証明、自然言語、Live Search Academic、SPINモデルチェッカ、Uppaal、VDM、Z言語、操作的意味論、数学、数理論理学、曖昧。 インデックスを展開 (13 もっと) »
ALGOL
ALGOL（アルゴル）は、命令型プログラミング言語ファミリーの1つファミリー名は大文字/小文字をまじえて表記される場合 と、全て大文字で表記される場合 (ALGOL 68) がある。本項目では ALGOL で統一する。。名前「ALGOL」は「アルゴリズム言語」を意味する英語「algorithmic language」に由来する。1950年代中ごろに開発され、多くの言語に影響を及ぼし、ACMや教科書や学術論文などでアルゴリズム記述のデファクトスタンダードとして30年以上使われた。現代の多くの言語が「ALGOL系」あるいは「ALGOL風」(algol-like) とされているという意味で、ほぼ同世代の高水準言語である FORTRAN、LISP、COBOL に比べて最も成功したと言うこともできる。FORTRANで明らかとなった問題を防ぐよう設計され、BCPL、B、Pascal、Simula、Cといった様々なプログラミング言語に影響を与えた。ALGOLはLisp以外としては「begin と end で囲む」という構文によるブロック構造を導入し、制御構造を自在に入れ子（ネスト）にできる初の広まった言語となったFORTRANにはそのような構造は無い。COBOLではピリオドで全ての入れ子が終端するという仕様だったため（現在はend-ifなどを使う）、入れ子で書ける論理に制限があり、酷いバグの原因にもなりやすかった。。また構文の形式的定義を真剣に検討した最初のプログラミング言語でもあり、"Algol 60 Report" で導入されたバッカス・ナウア記法は、その後のコンピュータ言語等の構文の形式的定義を示す手法として（プログラミング言語だけに限られず）定番の記法となっている。.
新しい！!: 形式手法とALGOL · 続きを見る »
Alloy Analyzer
軽量形式手法の一つ。仕様をモデルとして記述し検証するシステム。定義したデータの関係がどうなるか、模擬試験した結果を順に表示する仕組みがある。 設計者が想定していない関係が現れたら、仕様記述の不具合の可能性がある。 UML記述システムとAlloy Analyzeとの連携ソフトウェアがあり、UMLの記述ができる技術者が容易に利用できるようになっている。.
新しい！!: 形式手法とAlloy Analyzer · 続きを見る »
Association for Computing Machinery
Association for Computing Machinery (ACM) は、ニューヨークに本部のあるコンピュータ科学分野の国際学会。1947年設立。IEEEとともに、この分野で最も影響力の強い学会であり、IEEEがその名と由来や歴史からエレクトロニクスや通信分野の工学に強いのに対し、数学的な理論計算機科学のような分野もカバーする。日本語に訳して「計算機械学会」とされることもあるが、こんにちこの訳語が用いられることはほとんどなく、通常は単に"ACM"という略称で呼ばれるのがもっぱらである。ACMの「A」は Association (学会、団体) の頭文字であるが、アメリカ数学会 (AMS) と混同して「米国計算機学会」と誤訳されることがある。 数多くの国際会議を開催しており、人目を惹くデモ映像のSIGGRAPHやSIGMODなどはよく知られている。他の多くの学会と同様にすぐれた業績などへの表彰もおこなっているが、チューリング賞は、特にこの分野の最高の賞とみなされており、物理や化学といった分野におけるノーベル賞に匹敵するものと扱われることもある（他の賞についても時折「～のノーベル賞」といったような表現が使われることがあるが、この分野の全てを対象とした世界トップクラスの賞という位置づけにあるのはチューリング賞をおいて他にない）。.
新しい！!: 形式手法とAssociation for Computing Machinery · 続きを見る »
型システム
型システム（type system）とは、プログラミング言語において、その式などの部分が持つ値を、その種類（型(type)、データ型も参照）に沿って分類し、プログラムが正しく振る舞うこと、といった性質について保証する手法である。型システムは、型理論に基づいており、プログラミング言語の理論において最も確立された軽量形式手法である。.
新しい！!: 形式手法と型システム · 続きを見る »
契約プログラミング
契約プログラミング（けいやくプログラミング、Programming By Contract）または契約による設計（けいやくによるせっけい、Design By Contract）とは、プログラムコードの中にプログラムが満たすべき仕様についての記述を盛り込む事で設計の安全性を高める技法。プログラミング言語Eiffelで初めて導入された。"Design by Contract" の頭文字からとった DbC (ディービーシー) でよばれることが多い。.
新しい！!: 形式手法と契約プログラミング · 続きを見る »
工学
工学（こうがく、engineering）とは、.
代数的データ型
代数的データ型（Algebraic data type）とはプログラミング、特に関数型プログラミングや型システムにおいて使われるデータ型である。それぞれの代数的データ型の値には、1個以上のコンストラクタがあり、各コンストラクタには0個以上の引数がある。 代数的データ型の値（データ）の感覚的な説明としては、引数で与えられた他のデータ型の値を、コンストラクタで包んだようなもの、である。コンストラクタに引数がある代数データ型は複合型（他のデータ型を組み合わせて形成する型）である。.
新しい！!: 形式手法と代数的データ型 · 続きを見る »
仕様及び記述言語
仕様及び記述言語（しようおよびきじゅつげんご、SDL: Specification and Description Language）は、システムの仕様を記述するための言語であり、曖昧さのない仕様記述を実現するために作られた。主な対象は受動的な分散システムである。.
新しい！!: 形式手法と仕様及び記述言語 · 続きを見る »
仕様記述言語
仕様記述言語（しようきじゅつげんご）は、システムなどの仕様を記述する、コンピュータ言語（すなわち形式言語）である。形式的でない仕様記述もあるが（後述）、そういったものを含めて何らかの主張がされている場合もある。 プログラミング言語がシステムそのものに変換されるのに対し、仕様記述言語は必ずしもシステムに自動変換されるものではなく、あくまで仕様の妥当性を検証することに重きを置いている。ソフトウェア工学における一般的な設計プロセスの位置づけから、多くはプログラミング言語を記述する前段階に記述されることを期待している。 仕様記述と検証の方法について説明する。仕様記述では、何らかのシステムの仕様を論理学的あるいは代数学的に、形式的に記述する（形式仕様記述）。検証では、論理学や代数学に基づき（すなわち「機械的」に）、無矛盾性などといったシステムにおける「好ましい性質」の保証、あるいはデッドロックの可能性があるといった「好ましくない性質」の不存在を保証する（あるいは存在することを示し、修正を促す）。代表的な形式的仕様記述言語としてZ言語やLOTOSなどがある。研究段階では長い歴史を持つが、記述が複雑で高度なスキルを要求する上、システム全体の仕様を全て表現するには膨大な量の記述が必要になる。 また、検証ではない方法もある。たとえば、完全な妥当性は保証できないが、シミュレーションを行うことで、ある限られた場合においての動作を模擬して確かめる方法もある。SpecCはこの立場を取る。プロトタイピングもこの範疇にある。.
新しい！!: 形式手法と仕様記述言語 · 続きを見る »
形式仕様記述
形式仕様記述（けいしきしようきじゅつ、formal specification）とは形式手法のひとつで、何らのシステムなどについて、その性質などの仕様を形式的に記述する手法や、そういった手法による仕様の記述である。 形式的な仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的に判定することが可能となる(形式的検証)。また、仕様策定の工程で仕様の不整合を検出することが可能となり、実装工程のような開発の後半での仕様不備発覚、それに伴う手戻り(多大なコストを要する場合が多い)を防ぐという利点がある。他の使われ方として、仕様から設計、設計から実装へと段階的に検証可能なステップを踏んで詳細化し、開発工程で不具合を作りこむのを防ぐ。 設計（や実装）の「正当性」はそれ自身だけで確認できないという点が重要である。正当性は与えられた仕様に照らして初めて検証可能であり、形式仕様記述が解決すべき問題を正しく記述できるかどうかは別の問題である。これもまた困難な問題であり、非形式的な実際の問題を抽象化された形式的仕様記述で正しく記述する問題に帰着する。そして、そのような抽象化は形式的証明が不可能である。しかし、仕様が表現することを期待されている特性に関わる定理を証明することによって仕様記述を検証することは可能である。もし検証結果が正しければ、それらの定理は仕様記述者の仕様記述および根底にある問題領域との関係への理解を深める。検証結果が正しくない場合、その仕様は元となっている問題領域を正しく反映しているとは言えないので、仕様記述者はさらに理解を深めて仕様記述を改訂することになるだろう。.
新しい！!: 形式手法と形式仕様記述 · 続きを見る »
形式体系
形式体系（けいしきたいけい、Formal System）は、数学のモデルに基づいた任意の well-defined な抽象思考体系と定義される。エウクレイデスの『原論』は史上初の形式体系とされることが多く、形式体系の特徴をよく表している。その論理的基盤による体系の命題と帰結の関係（論理包含）は、他の抽象モデルを何らかの基盤とする体系から形式体系を区別するものである。形式体系は大きな理論や分野（例えばユークリッド幾何学）の基盤またはそのものとなることが多く、現代数学では証明論やモデル理論などと同義に扱われる。ただし形式体系は必ずしも数学的である必然性はなく、例えばスピノザの『エチカ』はエウクレイデスの『原論』の形式を模倣した哲学（倫理学）書である。 形式体系には形式言語があり、その形式言語は基本的な記号（シンボル）で構成される。形式言語の文（式）は公理群を出発点として、所定の構成規則（推論規則）に従って発展する。従って形式体系は基本的な記号群の有限の組み合わせを通して構築された任意個の数式で構成され、その組み合わせは公理群と構成規則群から作り出される。 数学における形式体系は以下の要素から構成される.
形式的検証
形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。.
新しい！!: 形式手法と形式的検証 · 続きを見る »
形式言語
形式言語（けいしきげんご、formal language）は、その文法（構文、統語論）が、場合によっては意味（意味論）も、形式的に与えられている（形式体系を参照）言語である。形式的でないために、しばしば曖昧さが曖昧なまま残されたり、話者集団という不特定多数によってうつろいゆくような自然言語のそれに対して、一部の人工言語や、いわゆる機械可読な（機械可読目録を参照）ドキュメント類などは形式言語である。この記事では形式的な統語論すなわち構文の形式的な定義と形式文法について述べる。形式的な意味論については形式意味論の記事を参照。.
ペトリネット
ペトリネット ペトリネット（Petri net）とは、カール・アダム・ペトリが1962年に発表した離散分散システムを数学的に表現する手法である。モデリング言語としては分散システムを注釈付の有向2部グラフとして視覚的に表現する。.
新しい！!: 形式手法とペトリネット · 続きを見る »
ハードウェア
ハードウェア (hardware) とは、システムの物理的な構成要素を指す一般用語である。日本語では機械、装置、設備のことを指す。ソフトウェアとの対比語であり、単に「ハード」とも呼ばれる。.
新しい！!: 形式手法とハードウェア · 続きを見る »
バッカス・ナウア記法
バッカス・ナウア記法（Backus-Naur form）とは、文脈自由文法を定義するのに用いられるメタ言語のことで、一般にBNFやBN記法と略される。現在はこのBNFを拡張したEBNF (Extended BNF) が一般的に使われている。EBNFでは正規表現を用いてより簡単に記述でき、プロトコル規定言語であるASN.1や、XMLの構文定義にも利用されている。 ジョン・バッカスとピーター・ナウアがALGOL 60 の文法定義のために考案。当初は文脈自由文法の本来の定義に則り or（|）以外の定義はなく、繰り返しは再帰を利用して表現されている。*、?等を含む正規表現はBNFを拡張したEBNFによって導入された。パーサジェネレータを使用して構文解析器を生成する際に、構文を定義するためにも使う。 ISO/IEC 14977:1996においてEBNFの標準が定義されているが、EBNFにもいろいろな亜種や変種がある。例えば、RFC2234にはABNFという変種が定義されている。しかし、ABNFは標準のEBNFとかなり異なる部分がある。.
新しい！!: 形式手法とバッカス・ナウア記法 · 続きを見る »
モデル検査
モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。.
新しい！!: 形式手法とモデル検査 · 続きを見る »
ユースケース
ユースケース（Use Case）は、ソフトウェア工学やシステム工学でシステム（あるいはシステムのシステム）の機能的要求を含む振舞を把握するための技法である。各ユースケースは、何らかの目的・目標/機能に関する台本（シナリオ）での主体（アクター(actor)）と呼ぶ利用者（ユーザ）とシステムのやりとりを描いている。ユースケースのアクターはエンドユーザーの場合もあるし、別のシステムの場合もある。ユースケースでは技術専門用語をなるべく使わず、エンドユーザーやそのビジネスの専門家に分かり易い用語を用いる。ユースケースの作成は、ビジネスアナリストとエンドユーザーが共同で行う。ユースケースを図にしたものがユースケース図であり、両者を厳密に区別すべき根拠はない。 1986年、後に統一モデリング言語(UML)やラショナル統一プロセス (RUP) で重要な役割を演じたイヴァー・ヤコブソンは、初めてユースケースの視覚化モデリング技法を成文化した。当初彼は usage scenarios とか usage case という用語を使用していたが、それらが英語として不自然であると気づき use case という用語を使うようになった。ヤコブソンが創始したユースケースのモデリングに対して、Kurt Bittner、Alistair Cockburn、Gunnar Overgaard といった人々が改良を加えていった。 1990年代、ユースケースは機能要求を含む振舞を把握する手法として使われるようになってきた。発祥の分野であるオブジェクト指向関連で顕著である。ユースケースの有効性はオブジェクト指向に限らない。ユースケースの仕様は、オブジェクト指向とは直接的な関係がない。 システム工学において、ユースケースはソフトウェア工学よりも抽象度の高いレベルで利用され、システムの任務やシステム保有者の目標を描くのに使われる。より詳細な要求は SysML のリクワイアメント図などで把握される。.
新しい！!: 形式手法とユースケース · 続きを見る »
プログラミング言語
プログラミング言語（プログラミングげんご、programming language）とは、コンピュータプログラムを記述するための形式言語である。なお、コンピュータ以外にもプログラマブルなものがあることを考慮するならば、この記事で扱っている内容については、「コンピュータプログラミング言語」（computer programming language）に限定されている。.
新しい！!: 形式手法とプログラミング言語 · 続きを見る »
プログラム (コンピュータ)
ンピュータプログラム（英：computer programs）とは、コンピュータに対する命令（処理）を記述したものである。コンピュータが機能を実現するためには、CPUで実行するプログラムの命令が必要である。 コンピュータが、高度な処理を人間の手によらず遂行できているように見える場合でも、コンピュータは設計者の意図であるプログラムに従い、忠実に処理を行っている。実際には、外部からの割り込み、ノイズなどにより、設計者の意図しない動作をすることがある。また設計者が、外部からの割り込みの種類を網羅的に確認していない場合もある。.
新しい！!: 形式手法とプログラム (コンピュータ) · 続きを見る »
プログラム意味論
プログラム意味論（program semantics）とは、計算機科学（特に理論計算機科学と分類されることもある）の一分野で、プログラミング言語の意味と計算モデルに関する分野である。形式的なものは、プログラミング言語の形式意味論とも呼ばれる。標準規格等では形式的でなく意味論を与えているものも多い。.
新しい！!: 形式手法とプログラム意味論 · 続きを見る »
プロセス計算
プロセス計算（プロセスけいさん、Process calculus）またはプロセス代数（プロセスだいすう、Process algebras）は、計算機科学において並行システムを形式的にモデリングする各種手法の総称。プロセス計算は、独立エージェントやプロセスの集まりにおける相互作用/通信/同期を抽象的に記述するツールである。また、プロセス記述を操作・分析可能にする代数学的規則も提供し、プロセス間の等価性について（双模倣性を使った）形式的推論を可能とする。主な具体例としては、CSP、CCS、ACP があるJ.C.M. Baeten:, Rapport CSR 04-02, Vakgroep Informatica, Technische Universiteit Eindhoven, 2004年。近年ではこれら以外に π計算(英語)、アンビエント計算、PEPA などもある。.
新しい！!: 形式手法とプロセス計算 · 続きを見る »
テイラーアンドフランシス
テイラー・アンド・フランシス・グループ（Taylor & Francis Group）は、イギリスを本拠とするインフォーマ（Informa）社の一部門である学術書出版社である。本社はイギリスのオックスフォード。イギリスの他、アメリカ合衆国、オーストラリア、シンガポール、中国、日本、マレーシア、スイス、インド、南アフリカの世界各国にオフィスを持つ。 同社は1852年、リチャード・テイラーの出版業に、化学者ウィリアム・フランシスが加わり、設立された。 1936年に有限責任株式会社化、1998年にロンドン証券取引所上場、2004年にはインフォーマと合併。合併以降同社は、インフォーマの学術出版部門として運営されている。 Taylor & Francis Groupは、毎年約2400の学術誌、7000タイトル以上の書籍を新刊し、約13万の既刊書を有する。.
新しい！!: 形式手法とテイラーアンドフランシス · 続きを見る »
フレデリック・ブルックス
フレデリック・フィリップス・ブルックス・ジュニア（Frederick Phillips Brooks, Jr.
新しい！!: 形式手法とフレデリック・ブルックス · 続きを見る »
ドナルド・クヌース
ドナルド・エルビン・クヌース（Donald Ervin Knuth, 1938年1月10日 -）は数学者、計算機科学者。スタンフォード大学名誉教授。 クヌースによるアルゴリズムに関する著作 The Art of Computer Programming のシリーズはプログラミングに携わるものの間では有名である。アルゴリズム解析と呼ばれる分野を開拓し、計算理論の発展に多大な貢献をしている。その過程で漸近記法で計算量を表すことを一般化させた。 理論計算機科学への貢献とは別に、コンピュータによる組版システム TeX とフォント設計システム METAFONT の開発者でもあり、Computer Modern という書体ファミリも開発した。 作家であり学者であるクヌースは、文芸的プログラミングのコンセプトを生み出し、そのためのプログラミングシステム WEB / CWEB を開発。また、MIX / MMIX 命令セットアーキテクチャを設計。.
新しい！!: 形式手法とドナルド・クヌース · 続きを見る »
アルゴリズム
フローチャートはアルゴリズムの視覚的表現としてよく使われる。これはランプがつかない時のフローチャート。 アルゴリズム（algorithm ）とは、数学、コンピューティング、言語学、あるいは関連する分野において、問題を解くための手順を定式化した形で表現したものを言う。算法と訳されることもある。 「問題」はその「解」を持っているが、アルゴリズムは正しくその解を得るための具体的手順および根拠を与える。さらに多くの場合において効率性が重要となる。 コンピュータにアルゴリズムをソフトウェア的に実装するものがコンピュータプログラムである。人間より速く大量に計算ができるのがコンピュータの強みであるが、その計算が正しく効率的であるためには、正しく効率的なアルゴリズムに基づいたものでなければならない。.
新しい！!: 形式手法とアルゴリズム · 続きを見る »
アクターモデル
アクターモデル（actor model）とは、1973年、カール・ヒューイット、Peter Bishop、Richard Steiger が発表した並行計算の数学的モデルの一種Carl Hewitt（1973年）, "A Universal Modular Actor Formalism for Artificial Intelligence".
新しい！!: 形式手法とアクターモデル · 続きを見る »
オートマトン
ートマトン (単数形: automaton, 複数形: オートマタ（automata ）) とは、自動人形などとも呼ばれる「オートマタ」と同じ語であるが、計算理論において、計算モデルに関して有限オートマトンなどの総称として使われる。また特に「オートマトン理論」と呼ばれる分野では、計算機械のうち計算可能性の点でチューリングマシンよりも制限されているものを特に指して言うこともある。.
新しい！!: 形式手法とオートマトン · 続きを見る »
オブジェクト指向モデリング
ブジェクト指向モデリング (オブジェクトしこうモデリング、英: Object-Oriented Modeling 、OOM) とは、システム等のモデリングにおいて、オブジェクト指向を取り入れたものである。以下、主としてコンピュータプログラムの設計におけるそれに関して述べる。.
新しい！!: 形式手法とオブジェクト指向モデリング · 続きを見る »
シュプリンガー・サイエンス・アンド・ビジネス・メディア
ュプリンガー・サイエンス・アンド・ビジネス・メディア（Springer Science+Business Media, Springer）は、科学（Science）、技術（Technology、工学など）、医学（Medicine）、すなわちSTM関連の書籍、電子書籍、査読済みジャーナルを出版するグローバル企業である。シュプリンガーはまた、"SpringerLink"（「シュプリンガー・リンク」） 、"SpringerProtocols"（「」） 、"SpringerImages"（「シュプリンガー・イメージ」） 、"SpringerMaterials"（「シュプリンガー・マテリアル」） などいくつかの科学データベース・サービスのホスティングも行っている。 出版物には、参考図書（Reference works、レ（リ）ファレンス・ワークス）、教科書、モノグラフ（Monograph）、（Proceedings）、叢書など多数が含まれる。また、シュプリンガー・リンクには45,000以上のタイトルが自然科学など13の主題・テーマで集められており、それらは電子書籍として利用可能である。シュプリンガーはSTM分野の書籍に関しては世界最大の出版規模を持ち、ジャーナルでは世界第2位である（第1位はエルゼビア）。 多数のインプリントや、20ヶ国に約55の発行所（パブリッシング・ハウス）、5,000人以上の従業員を抱え、毎年約2,000のジャーナル、7,000以上の新書（これにはSTM分野だけではなく、B2B分野のものも含まれる）を発刊している。シュプリンガーはベルリン、ハイデルベルク、ドルトレヒト、ニューヨークに主要オフィスを構える。近年成長著しいアジア市場のために、アジア地域本部を香港に置いており、2005年8月からは北京に代表部を設置している 。 2015年5月、シュプリンガー・サイエンス+ビジネスメディアとマクミラン・サイエンス・アンド・エデュケーションの大半の事業の合併が、欧州連合や米国司法省などの主要な公正競争監視機関により承認された。新会社の名称は「シュプリンガー・ネイチャー（Springer Nature）」。.
新しい！!: 形式手法とシュプリンガー・サイエンス・アンド・ビジネス・メディア · 続きを見る »
ジョン・バッカス
ョン・ワーナー・バッカス（John Warner Backus, 1924年12月3日 - 2007年3月17日）は、アメリカ合衆国の数学者。初期の高水準プログラミング言語 (FORTRAN) の発明者、（形式言語の文法の定義に汎用的に用いられる）バッカス・ナウア記法の発明者、また (Function-level Programming) の提唱者でもある。.
新しい！!: 形式手法とジョン・バッカス · 続きを見る »
ソフトウェア
フトウェア（software）は、コンピューター分野でハードウェア（物理的な機械）と対比される用語で、何らかの処理を行うコンピュータ・プログラムや、更には関連する文書などを指す。ソフトウェアは、一般的にはワープロソフトなど特定の作業や業務を目的としたアプリケーションソフトウェア（応用ソフトウェア、アプリ）と、ハードウェアの管理や基本的な処理をアプリケーションソフトウェアやユーザーに提供するオペレーティングシステム (OS) などのシステムソフトウェアに分類される。.
新しい！!: 形式手法とソフトウェア · 続きを見る »
ソフトウェア危機
フトウェア危機（ソフトウェアきき、Software Crisis）とは、ソフトウェア工学がまだ十分に確立していなかった頃、よく使われた言葉である。この言葉は、コンピュータの急激な高性能化によってコンピュータ上のシステムが扱う問題が益々複雑化することによる影響を表したものである。基本的にソフトウェア危機は、正しく、可読性が高く、検証可能なコンピュータプログラムを書くことの困難さから発した考え方である。ソフトウェア危機の根本は、複雑性と予測と変化である。.
新しい！!: 形式手法とソフトウェア危機 · 続きを見る »
ソフトウェア工学
フトウェア工学（ソフトウェアこうがく、Software engineering）は、コンピュータのプログラム、およびその作成行為であるプログラミングを対象とした工学である。.
新しい！!: 形式手法とソフトウェア工学 · 続きを見る »
ソフトウェア設計
フトウェア設計（Software design）は、ソフトウェアのための問題解決と計画の工程である。ソフトウェアの目的と仕様が決定した後で、ソフトウェア開発者が設計をしたり、専門の設計者が開発計画を立てる。細かいコンポーネントやアルゴリズムの実装だけではなく、アーキテクチャ的観点での検討も行われる。 ソフトウェア開発工程での要求分析によって、ソフトウェア工学における仕様が確定する。そのソフトウェアがユーザーとの対話を必要とするものか、あるいはユーザー中心設計であれば、ソフトウェア設計にはユーザーエクスペリエンス設計も関わり、絵コンテなども仕様に含まれることになる。完全に自動的に動作するソフトウェア（ユーザインタフェースのないソフトウェア）であれば、ソフトウェア設計は単なるフローチャート作成程度の作業となるかもしれない。また、統一モデリング言語 (UML) などの半形式的手法もある。いずれにしても、ソフトウェア設計工程の成果物としては、何らかのソフトウェア設計文書が生成される。.
新しい！!: 形式手法とソフトウェア設計 · 続きを見る »
ソフトウェア開発
フトウェア開発（ソフトウェアかいはつ、Software Development）とは、ユーザーのニーズやマーケティング上の目標をソフトウェア製品に変換する作業である。ソフトウェア開発には、ソフトウェア工学の研究的側面とソフトウェア製品を開発するマーケティング的側面が含まれていると言われることがある。ソフトウェア製品のマーケティング活動そのものは、必ずしも新商品開発とは結びつかない。顧客の期待を満足させるべく開発されたソフトウェア製品の成功/失敗の責任が工学的側面にあるのかマーケティング的側面にあるのかを判別するのは、多くの場合困難である。そのため、ソフトウェア開発全体として工学的側面とマーケティング的側面を共に理解し、それらの協調を促進することが重要である。工学とマーケティングの両方の側面をまとめ、バランスをとるのは、プロジェクトマネージャなどと呼ばれる立場の人である。 マーケティングとの関わりはソフトウェア要求分析としても知られている。ソフトウェア開発はクライアントが必要とするもの以上の機能を開発しようとしたり、逆に妥協しようとしたりする。そのため、ソフトウェア開発は通常の工学/技術とは関連付けられていなかった各種プロセス（市場調査、人材登用、リスクマネジメント、知的財産権、予算、危機管理など）まで取り込もうとする場合がある。その場合、ソフトウェア開発は Business Development と呼ばれる領域ともオーバーラップすることになる。 Alan M. Davis は著書 "Great Software Debates" の章 "Requirements" の節 "The Missing Piece of Software Development" で次のように述べている.
新しい！!: 形式手法とソフトウェア開発 · 続きを見る »
ソフトウェア開発工程
フトウェア開発工程（ソフトウェアかいはつこうてい、Software Development Process）とは、ソフトウェア製品の開発の構造を意味する。ソフトウェアライフサイクル、ソフトウェア開発プロセス、ソフトウェアプロセスもほぼ同義語である。開発工程にはいくつかのモデルがあり、開発工程内の各種タスク・活動のための手法を提案している。.
新しい！!: 形式手法とソフトウェア開発工程 · 続きを見る »
公理的意味論
公理的意味論（こうりてきいみろん、Axiomatics Semantics）とは、数理論理学に基づいてプログラムの正当性を証明する手法。ホーア論理と密接に関連している。.
新しい！!: 形式手法と公理的意味論 · 続きを見る »
B-Method
B-Methodとは、AMN（Abstract Machine Notation）という仕様記述言語（兼プログラミング言語）を中心とした形式手法に基づいたソフトウェア開発手法である。B-Method で使用する形式手法やそのツール群は単に B と呼ぶ。.
新しい！!: 形式手法とB-Method · 続きを見る »
Communicating Sequential Processes
Communicating Sequential Processes（CSP）とは、並行性に関するプロセス計算の理論のひとつである.
新しい！!: 形式手法とCommunicating Sequential Processes · 続きを見る »
理論計算機科学
論計算機科学（りろんけいさんきかがく、英語：theoretical computer science）は計算機を理論的に研究する学問で、計算機科学の一分野である。計算機を数理モデル化して数学的に研究することを特徴としている。「数学的」という言葉は広義には公理的に扱えるもの全てを指すので、理論計算機科学は広義の数学の一分野でもある。理論計算機科学では、現実のコンピュータを扱うことも多いが、チューリングマシンなどの計算モデルを扱うことも多い。 理論計算機科学の代表的な分野として以下のものがある。.
新しい！!: 形式手法と理論計算機科学 · 続きを見る »
神託機械
託機械（しんたくきかい、oracle machine）または預言機械（よげんきかい）は、計算複雑性理論や計算可能性理論における抽象機械の一種であり、決定問題の研究で使われる。チューリングマシンに神託（oracle）と呼ばれるブラックボックスが付加されたものであり、そのブラックボックスは特定の決定問題を1ステップで決定可能である。チューリングマシンの停止問題のような決定不能な問題にも神託機械を想定することができる。.
Esterel
Esterel は、複雑なリアルタイムシステム向けの同期型プログラミング言語である。命令型プログラミングのスタイルで、並列性とプリエンプションを単純に表せる。従って、制御系の設計に非常に適している。 開発は、Gérard Berry に率いられたパリ国立高等鉱業学校と INRIA のチームにより、1980年代初めに開始された。現在のコンパイラは、Esterel のソースコードからC言語のコードかレジスタ転送レベルのハードウェア記述（VHDLかVerilog）を生成する。 開発は今も継続している。商用版には統合開発環境 Esterel Studio がある。その開発会社 Esterel Technologies は IEEE での標準化を開始している。現在、 が一般に公開されている。.
新しい！!: 形式手法とEsterel · 続きを見る »
銀の弾などない
『銀の弾などない— ソフトウェアエンジニアリングの本質と偶有的事項』（ぎんのたまなどない ソフトウェアエンジニアリングのほんしつとぐうゆうてきじこう、No Silver Bullet - essence and accidents of software engineering）とは、フレデリック・ブルックスが1986年に著した、ソフトウェア工学の広く知られた論文である。.
新しい！!: 形式手法と銀の弾などない · 続きを見る »
領域理論
域理論 （りょういきりろん、domain theory）は、領域 (domain) と呼ばれる特別な種類の半順序集合を研究する数学の分野であり、順序理論の一分野である。 計算機科学の表示的意味論（denotational semantics）を構築するために用いられる。 領域理論は、近似と収束という直観的概念を極めて一般的な枠組で形式化し、位相空間と密接な関係をもつ。 表示的意味論に対する他の重要なアプローチとしては距離空間を用いるものがある。.
表示的意味論
表示的意味論（ひょうじてきいみろん、Denotational Semantics）とは、計算機科学（理論計算機科学）の一分野で、プログラミング言語の形式意味論（プログラム意味論）の手法のひとつである。初期には「数理的意味論」（mathematical semantics）、「スコット-ストレイチー意味論」（Scott–Strachey semantics）のようにも呼ばれた。プログラムの意味をあらわす数学的オブジェクト（これを「表示」（denotation）と呼ぶ）を構築することで、プログラミング言語の意味論を形式化する手法である。 表示的意味論の起源は、1960年代のクリストファー・ストレイチーやデイナ・スコットの研究である。ストレイチーやスコットが開発した本来の表示的意味論は、プログラムの表示（意味）を入力を出力にマッピングする関数に変換するものである。後にこれはプログラムの表示（意味）を定義するには非力であることが証明され、例えば再帰定義関数・データ構造を表現できないことが判明した。これを解決するため、スコットはより汎用的な領域理論に基づいた表示的意味論を提案したS.
新しい！!: 形式手法と表示的意味論 · 続きを見る »
表明
表明（ひょうめい、assertion）とは、プログラミングにおける概念のひとつであり、そのプログラムの前提条件を示すのに使われる。アサーションとも呼ばれる。表明は、プログラムのその箇所で必ず真であるべき式の形式をとる。多くの言語ではそのような前提条件のチェックに表明を使用するが、設計上の判断を文書化するのに使う場合もある。表明が偽となった場合、プログラムにバグが潜在していることを示している。これを「表明違反; assertion failure」と呼ぶ。表明を言語構文や標準ライブラリとしてサポートするプログラミング言語も存在する。 プログラマは、開発過程でソースコードに表明を追加する。デバッグを単純化し、問題を早期に検出するためである。表明違反はバグを示していることが多いため、表明の実装では問題の元を示すために追加情報を表示するようになっていることが多い（ソースコードのファイル名と行番号、スタックトレースなど）。ほとんどの実装では、そのプログラムの実行が即座に停止する。.
複雑性
複雑性（ふくざつせい、complexity）という用語は、多数の部品が入り組んで配置された何らかのものを特徴付ける言葉として使われる。科学として複雑性を研究するアプローチはいくつか存在しており、本項目ではそれらを概説する。マサチューセッツ工科大学のセス・ロイドは、複雑性の定義を32種類集めてプレゼンテーションしたことがあるという。.
証明
証明（しょうめい）とは、ある事柄が真理もしくは事実であることを明らかにすること。また、その内容。.
詳細化
詳細化（しょうさいか、Refinement）とは、形式手法において、抽象的な形式仕様記述から具体的な実行プログラムへと検証可能な変換を行うことである。 段階的な詳細化として段階を踏んで詳細化を行うこともできる。論理的には、詳細化は含意による変換であるが、追加的な複雑化を生じる要因もある。 詳細化の反対語は抽象化である。.
論理学
論理学（ろんりがく、）とは、「論理」を成り立たせる論証の構成やその体系を研究する学問である。.
航空宇宙工学
航空宇宙工学（こうくううちゅうこうがく、）とは、航空工学と宇宙工学の総称であり、航空機・ロケット・人工衛星などの設計・製造・運用に関する工学の一分野。宇宙開発は航空機の発展ときわめて密接に関係しながら発達してきた歴史的経緯もあり、航空機と宇宙機はともに研究・開発されることが多い。 航空機・宇宙機はその性質上、気圧・温度の急激な変化にさらされたり、機体構造に大きな荷重がかかったりするなど過酷な環境におかれる、といったことが目に見えてわかりやすいが、真の難しさは、航空機や宇宙機がその機能を果たすためには安全係数を大きく取れないことにある。そのため、その過程では空気力学・構造力学をはじめとして様々な科学技術の知識が必要となり、これら航空宇宙機に用いられる知識体系が集合的に航空宇宙工学という分野を形成している。このように関係する分野の多彩さから、航空宇宙工学に携わる者が一人で全容を把握することは極めて困難であり、必然的に実際の開発は様々な分野の専門家がチームを形成し、分担して関わることになる。また、各分野からみて望ましい機体の形状や性能は互いに矛盾する場合があり、開発に当たっては各観点の重要度を総合的に判断し、性能・価格・技術的課題のバランスをみながら進めていくというのも、航空宇宙工学の特徴の１つである。.
新しい！!: 形式手法と航空宇宙工学 · 続きを見る »
自動定理証明
アルゴンヌ国立研究所は1960年代以降2000年代まで、自動定理証明のリーダーだった。 自動定理証明（automated theorem proving, ATP）とは、自動推論 (AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。.
新しい！!: 形式手法と自動定理証明 · 続きを見る »
自然言語
自然言語（しぜんげんご、natural language）とは、人間によって日常の意思疎通のために用いられる、文化的背景を持って自然に発展してきた言語である。分類として、音声言語と文字言語、口頭言語と書記言語、口語と文語といったような分類があるが、いずれも似ているようだが着目点や対比軸が異なる分類であり、混同してはならない。また、以上のような分類がいずれも当たらない言語もあり、例えば日本手話（「日本語対応手話」とは異なる）がそうである。.
Live Search Academic
Live Search Academic（ライブ サーチ アカデミック 和名：Windows Live 学術論文検索）は、2006年から2008年まで提供されていた、Windows Liveサービスの1つ、学術論文や、著者、雑誌、および会議の議事録を検索することができた。2008年5月に同サービスの終了が発表され、その短い歴史に幕を下ろした。.
新しい！!: 形式手法とLive Search Academic · 続きを見る »
SPINモデルチェッカ
SPINモデルチェッカ（英: SPIN model checker）は、ソフトウェアのモデル検査のためのツールである。Gerard J. Holzmann らが開発し、15年以上に渡って改良を続けてきた。2001年にAssociation for Computing Machinery (ACM) のソフトウェアシステム賞を受賞している。1995年以来、ほぼ毎年モデル検査に興味のある SPIN ユーザーや研究者による SPIN ワークショップが開催されている。.
新しい！!: 形式手法とSPINモデルチェッカ · 続きを見る »
Uppaal
形式言語のうち、モデル検査の機能を持つシステム。 時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。 学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。 JAXAなど、研究開発機関での利用が進んでいる。.
新しい！!: 形式手法とUppaal · 続きを見る »
VDM
VDM（Vienna Development Method）は、IBMのウィーン研究所で1960年代から70年代にかけて開発された形式手法。 その仕様記述言語VDM-SLは1996年にISO標準（ISO_IEC_13817-1）となっている。VDM-SLをオブジェクト指向拡張したVDM++も、欧州連合ESPRIT計画のAFRODITEプロジェクトで開発された。.
Z言語
Z言語 (ぜっどげんご) は、Z記法 (ぜっどきほう) ともいい、形式仕様記述言語であり、コンピュータシステムの記述とモデリングを行うために使われる。 ZはZF集合論から名前をとって命名された。 Zは次のことに焦点を当てている。.
操作的意味論
操作的意味論（そうさてきいみろん、Operational Semantics）とは、プログラムの意味を数学的に厳密に与える計算機科学の手法の一種（プログラム意味論参照）。.
新しい！!: 形式手法と操作的意味論 · 続きを見る »
数学
数学（すうがく、μαθηματικά, mathematica, math）は、量（数）、構造、空間、変化について研究する学問である。数学の範囲と定義については、数学者や哲学者の間で様々な見解がある。.
数理論理学
数理論理学（mathematische Logik、mathematical logic）は、論理学（形式論理学）の数学への応用の探求ないしは論理学の数学的な解析を主たる目的とする、数学の関連分野である。局所的には数理論理学は超数学、数学基礎論、理論計算機科学などと密接に関係している。数理論理学の共通な課題としては形式体系の表現力や形式証明系の演繹の能力の研究が含まれる。 数理論理学はしばしば集合論、モデル理論、再帰理論、証明論の4つの領域に分類される。これらの領域はロジックのとくに一階述語論理や定義可能性に関する結果を共有している。計算機科学（とくに）における数理論理学の役割の詳細はこの記事には含まれていない。詳細はを参照。 この分野が始まって以来、数理論理学は数学基礎論の研究に貢献し、また逆に動機付けられてきた。数学基礎論は幾何学、算術、解析学に対する公理的な枠組みの開発とともに19世紀末に始まった。20世紀初頭、数学基礎論は、ヒルベルトのプログラムによって、数学の基礎理論の無矛盾性を証明するものとして形成された。クルト・ゲーデルとゲルハルト・ゲンツェンによる結果やその他は、プログラムの部分的な解決を提供しつつ、無矛盾性の証明に伴う問題点を明らかにした。集合論における仕事は殆ど全ての通常の数学を集合の言葉で形式化できることを示した。しかしながら、集合論に共通の公理からは証明することができない幾つかの命題が存在することも知られた。むしろ現代の数学基礎論では、全ての数学を展開できる公理系を見つけるよりも、数学の一部がどのような特定の形式的体系で形式化することが可能であるか（逆数学のように）ということに焦点を当てている。.
新しい！!: 形式手法と数理論理学 · 続きを見る »
曖昧
曖昧（あいまい）とは、1つの表現や文字列、項目などが2つ以上の意味にとれること、もしくは、周辺が不明瞭なことである。.
