ブラウザよりも高速アクセス！
9 関係: 定理、仕様、仕様記述言語、形式的検証、形式手法、システム、ソフトウェア工学、詳細化、正当性 (計算機科学)。
定理
定理（ていり、theorem）とは、数理論理学および数学において、証明された真なる命題をいう。 文脈によっては公理も定理に含む。また、数学においては論説における役割等から、補題（ほだい、lemma）あるいは補助定理（ほじょていり、helping theorem）、系（けい、corollary）、命題（めいだい、proposition）などとも呼ばれることがある。ここでの「命題」と冒頭文に言う命題とは意味が異なることに注意。 一般的に定理は、まずいくつかの条件を列挙し、次にその下で成り立つ結論を述べるという形をしている。例えば、次は代数学の基本定理の述べ方の1つである。 ある一定の条件（公理系）下で定理を述べそれを証明すること、というのが数学という分野の中心的な研究の形態である。 数学の多くの分野には、各々「基本定理」という名で呼ばれる中心的な定理が存在している。なお定理という名称と証明という手続きは、数学のみならず、物理や工学においても使用される。.
仕様
仕様（しよう、英: specification スペシフィケーション）とは、材料・製品・サービスなどが明確に満たさなければならない要求事項の集まりである。日常的には英語を短縮して「スペック」とも。.
仕様記述言語
仕様記述言語（しようきじゅつげんご）は、システムなどの仕様を記述する、コンピュータ言語（すなわち形式言語）である。形式的でない仕様記述もあるが（後述）、そういったものを含めて何らかの主張がされている場合もある。 プログラミング言語がシステムそのものに変換されるのに対し、仕様記述言語は必ずしもシステムに自動変換されるものではなく、あくまで仕様の妥当性を検証することに重きを置いている。ソフトウェア工学における一般的な設計プロセスの位置づけから、多くはプログラミング言語を記述する前段階に記述されることを期待している。 仕様記述と検証の方法について説明する。仕様記述では、何らかのシステムの仕様を論理学的あるいは代数学的に、形式的に記述する（形式仕様記述）。検証では、論理学や代数学に基づき（すなわち「機械的」に）、無矛盾性などといったシステムにおける「好ましい性質」の保証、あるいはデッドロックの可能性があるといった「好ましくない性質」の不存在を保証する（あるいは存在することを示し、修正を促す）。代表的な形式的仕様記述言語としてZ言語やLOTOSなどがある。研究段階では長い歴史を持つが、記述が複雑で高度なスキルを要求する上、システム全体の仕様を全て表現するには膨大な量の記述が必要になる。 また、検証ではない方法もある。たとえば、完全な妥当性は保証できないが、シミュレーションを行うことで、ある限られた場合においての動作を模擬して確かめる方法もある。SpecCはこの立場を取る。プロトタイピングもこの範疇にある。.
新しい！!: 形式仕様記述と仕様記述言語 · 続きを見る »
形式的検証
形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。.
新しい！!: 形式仕様記述と形式的検証 · 続きを見る »
形式手法
Z言語を使った形式仕様記述の例 形式手法（けいしきしゅほう、formal methods）は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている。 形式手法は理論計算機科学の様々な成果を基盤として応用したものであり、数理論理学、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う。.
新しい！!: 形式仕様記述と形式手法 · 続きを見る »
システム
テム（system）は、相互に影響を及ぼしあう要素から構成される、まとまりや仕組みの全体。一般性の高い概念であるため、文脈に応じて系、体系、制度、方式、機構、組織といった多種の言葉に該当する。系 (自然科学) の記事も参照。 それ自身がシステムでありながら同時に他のシステムの一部でもあるようなものをサブシステムという。.
新しい！!: 形式仕様記述とシステム · 続きを見る »
ソフトウェア工学
フトウェア工学（ソフトウェアこうがく、Software engineering）は、コンピュータのプログラム、およびその作成行為であるプログラミングを対象とした工学である。.
新しい！!: 形式仕様記述とソフトウェア工学 · 続きを見る »
詳細化
詳細化（しょうさいか、Refinement）とは、形式手法において、抽象的な形式仕様記述から具体的な実行プログラムへと検証可能な変換を行うことである。 段階的な詳細化として段階を踏んで詳細化を行うこともできる。論理的には、詳細化は含意による変換であるが、追加的な複雑化を生じる要因もある。 詳細化の反対語は抽象化である。.
新しい！!: 形式仕様記述と詳細化 · 続きを見る »
正当性 (計算機科学)
計算機科学における正当性（Correctness）とは、アルゴリズムがその仕様に照らして正しいことを意味する。「機能的」正当性とは、アルゴリズムの入出力動作に関する正当性である（すなわち、各入力に対して正しく出力を生成すること）。形式的検証を参照されたい。 完全正当性（Total Correctness）は、アルゴリズムが常に停止することも要求される。一方、部分正当性（Partial Correctness）は単に返ってくる答えが正しいことのみを要求する（常に答えが返ってくるとは限らない）。停止問題には汎用的解法はないので、完全正当性はより深い問題をはらんでいる。 例えば、整数を 1 から順に調べて奇数の完全数を探すとした場合、部分正当性を備えたプログラムを書くのは極めて簡単である（素因数分解を行って n が完全数かどうかを調べる）。しかし、そのプログラムが完全正当性を備えているとするには数論において未知の知識を必要とする。 正当性の証明は数学的証明でなければならず、アルゴリズムもその仕様記述も形式的に与えられなければならない（形式的仕様記述）。特にその証明は、そのアルゴリズムを特定のマシン上でプログラムとして実装したものについて正当性を意味するものではない。その場合メモリ量の限界を考慮する必要がある。 証明論におけるカリー・ハワード対応は、直観主義論理における機能的正当性の証明がラムダ計算における特定プログラムに対応するとしている。このような証明の変換を「プログラム抽出; program extraction」と呼ぶ。.
新しい！!: 形式仕様記述と正当性 (計算機科学) · 続きを見る »
