ブラウザよりも高速アクセス！
27 関係: 契約プログラミング、仕様記述言語、形式仕様記述、形式的検証、形式手法、ユーザー、トップダウン設計とボトムアップ設計、プログラム (コンピュータ)、テストケース、ウォーターフォール・モデル、エクストリーム・プログラミング、システム、ソースコード、ソフトウェア、ソフトウェア工学、ソフトウェアテスト、ソフトウェアドキュメンテーション、ソフトウェア開発、公理的意味論、表示的意味論、要求仕様、要求分析、詳細化、VDM、Z言語、操作的意味論、数学。
契約プログラミング
契約プログラミング（けいやくプログラミング、Programming By Contract）または契約による設計（けいやくによるせっけい、Design By Contract）とは、プログラムコードの中にプログラムが満たすべき仕様についての記述を盛り込む事で設計の安全性を高める技法。プログラミング言語Eiffelで初めて導入された。"Design by Contract" の頭文字からとった DbC (ディービーシー) でよばれることが多い。.
新しい！!: プログラム仕様と契約プログラミング · 続きを見る »
仕様記述言語
仕様記述言語（しようきじゅつげんご）は、システムなどの仕様を記述する、コンピュータ言語（すなわち形式言語）である。形式的でない仕様記述もあるが（後述）、そういったものを含めて何らかの主張がされている場合もある。 プログラミング言語がシステムそのものに変換されるのに対し、仕様記述言語は必ずしもシステムに自動変換されるものではなく、あくまで仕様の妥当性を検証することに重きを置いている。ソフトウェア工学における一般的な設計プロセスの位置づけから、多くはプログラミング言語を記述する前段階に記述されることを期待している。 仕様記述と検証の方法について説明する。仕様記述では、何らかのシステムの仕様を論理学的あるいは代数学的に、形式的に記述する（形式仕様記述）。検証では、論理学や代数学に基づき（すなわち「機械的」に）、無矛盾性などといったシステムにおける「好ましい性質」の保証、あるいはデッドロックの可能性があるといった「好ましくない性質」の不存在を保証する（あるいは存在することを示し、修正を促す）。代表的な形式的仕様記述言語としてZ言語やLOTOSなどがある。研究段階では長い歴史を持つが、記述が複雑で高度なスキルを要求する上、システム全体の仕様を全て表現するには膨大な量の記述が必要になる。 また、検証ではない方法もある。たとえば、完全な妥当性は保証できないが、シミュレーションを行うことで、ある限られた場合においての動作を模擬して確かめる方法もある。SpecCはこの立場を取る。プロトタイピングもこの範疇にある。.
新しい！!: プログラム仕様と仕様記述言語 · 続きを見る »
形式仕様記述
形式仕様記述（けいしきしようきじゅつ、formal specification）とは形式手法のひとつで、何らのシステムなどについて、その性質などの仕様を形式的に記述する手法や、そういった手法による仕様の記述である。 形式的な仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的に判定することが可能となる(形式的検証)。また、仕様策定の工程で仕様の不整合を検出することが可能となり、実装工程のような開発の後半での仕様不備発覚、それに伴う手戻り(多大なコストを要する場合が多い)を防ぐという利点がある。他の使われ方として、仕様から設計、設計から実装へと段階的に検証可能なステップを踏んで詳細化し、開発工程で不具合を作りこむのを防ぐ。 設計（や実装）の「正当性」はそれ自身だけで確認できないという点が重要である。正当性は与えられた仕様に照らして初めて検証可能であり、形式仕様記述が解決すべき問題を正しく記述できるかどうかは別の問題である。これもまた困難な問題であり、非形式的な実際の問題を抽象化された形式的仕様記述で正しく記述する問題に帰着する。そして、そのような抽象化は形式的証明が不可能である。しかし、仕様が表現することを期待されている特性に関わる定理を証明することによって仕様記述を検証することは可能である。もし検証結果が正しければ、それらの定理は仕様記述者の仕様記述および根底にある問題領域との関係への理解を深める。検証結果が正しくない場合、その仕様は元となっている問題領域を正しく反映しているとは言えないので、仕様記述者はさらに理解を深めて仕様記述を改訂することになるだろう。.
新しい！!: プログラム仕様と形式仕様記述 · 続きを見る »
形式的検証
形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。.
新しい！!: プログラム仕様と形式的検証 · 続きを見る »
形式手法
Z言語を使った形式仕様記述の例 形式手法（けいしきしゅほう、formal methods）は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている。 形式手法は理論計算機科学の様々な成果を基盤として応用したものであり、数理論理学、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う。.
新しい！!: プログラム仕様と形式手法 · 続きを見る »
ユーザー
ユーザー（英語: user）または使用者（しようしゃ）とは、実際に商品やサービスなどを使う人、または買う人。 use（使う）に接尾辞 -er（〜する人）が合わさった派生語。 使用者、利用者、需要者、最終消費者、また企業にとっては顧客の意味もある。.
新しい！!: プログラム仕様とユーザー · 続きを見る »
トップダウン設計とボトムアップ設計
トップダウン設計とボトムアップ設計（トップダウンせっけいとボトムアップせっけい）とは、設計戦略である。トップダウンとボトムアップは、情報や知識の順序付け戦略であり、様々な分野で使われる用語である。この記事では、主にソフトウェア工学での用法について解説する。.
新しい！!: プログラム仕様とトップダウン設計とボトムアップ設計 · 続きを見る »
プログラム (コンピュータ)
ンピュータプログラム（英：computer programs）とは、コンピュータに対する命令（処理）を記述したものである。コンピュータが機能を実現するためには、CPUで実行するプログラムの命令が必要である。 コンピュータが、高度な処理を人間の手によらず遂行できているように見える場合でも、コンピュータは設計者の意図であるプログラムに従い、忠実に処理を行っている。実際には、外部からの割り込み、ノイズなどにより、設計者の意図しない動作をすることがある。また設計者が、外部からの割り込みの種類を網羅的に確認していない場合もある。.
新しい！!: プログラム仕様とプログラム (コンピュータ) · 続きを見る »
テストケース
テストケー.
新しい！!: プログラム仕様とテストケース · 続きを見る »
ウォーターフォール・モデル
ウォーターフォール・モデルは、ソフトウェア工学では非常に古くからある、もっともポピュラーな開発モデル。.
新しい！!: プログラム仕様とウォーターフォール・モデル · 続きを見る »
エクストリーム・プログラミング
トリーム・プログラミング、XP（extreme programming）は、ケント・ベックらによって定式化され、提唱されているソフトウェア開発手法である。柔軟性の高い開発手法であるため、難易度の高い開発やビジネス上の要求が刻々と変わるような状況に向いた開発手法である。事前計画よりも柔軟性を重視する。1999年に書籍『XPエクストリーム・プログラミング入門―ソフトウェア開発の究極の手法』によって発表された。 XPは、軽量開発手法あるいはアジャイルソフトウェア開発手法と呼ばれる、同種の開発手法のなかで代表的なものである。柔軟性の高い開発手法であるが、古典的には開発が進むにつれ変更コストは大きくなると言うことを前提に開発手法が構築されているのに対して、自動テストを導入するなど様々な対策をすることにより開発が進んでも変更コストが大きくならないような工夫を持ち込むことにより、変更に対する柔軟性を実現している。この変更コストが増大しないという前提が破綻すると、この手法も破綻する。 XPは比較的少人数の開発にもっとも適用しやすく、5つの価値と19の具体的なプラクティス（実践）が定義されている。XPはドキュメントよりもソースコードを、組織的開発の歯車となることよりも、個人の責任と勇気を重んじる人間中心の開発プロセスであるとしている。.
新しい！!: プログラム仕様とエクストリーム・プログラミング · 続きを見る »
システム
テム（system）は、相互に影響を及ぼしあう要素から構成される、まとまりや仕組みの全体。一般性の高い概念であるため、文脈に応じて系、体系、制度、方式、機構、組織といった多種の言葉に該当する。系 (自然科学) の記事も参照。 それ自身がシステムでありながら同時に他のシステムの一部でもあるようなものをサブシステムという。.
新しい！!: プログラム仕様とシステム · 続きを見る »
ソースコード
青で示されているのが有効なコードである。 ソースコード（source code）とは、コンピュータプログラミング言語で書かれた、コンピュータプログラムである文字列（テキストないしテキストファイル）のことである。.
新しい！!: プログラム仕様とソースコード · 続きを見る »
ソフトウェア
フトウェア（software）は、コンピューター分野でハードウェア（物理的な機械）と対比される用語で、何らかの処理を行うコンピュータ・プログラムや、更には関連する文書などを指す。ソフトウェアは、一般的にはワープロソフトなど特定の作業や業務を目的としたアプリケーションソフトウェア（応用ソフトウェア、アプリ）と、ハードウェアの管理や基本的な処理をアプリケーションソフトウェアやユーザーに提供するオペレーティングシステム (OS) などのシステムソフトウェアに分類される。.
新しい！!: プログラム仕様とソフトウェア · 続きを見る »
ソフトウェア工学
フトウェア工学（ソフトウェアこうがく、Software engineering）は、コンピュータのプログラム、およびその作成行為であるプログラミングを対象とした工学である。.
新しい！!: プログラム仕様とソフトウェア工学 · 続きを見る »
ソフトウェアテスト
フトウェアテスト（）は、コンピュータのプログラムから仕様にない振舞または欠陥（バグ）を見つけ出す作業のことである。ソフトウェアテストで見つかったプログラム中の欠陥を修正する作業をデバッグという。ソフトウェアテストに成功するとは、テストで欠陥が発見されるか、規定した試験項目にすべて合格するか、規定した品質目標に到達することである。目標とした品質には、規定した試験項目にすべて合格することもある。例えば、OS, プログラミング言語では、仕様を満たしているかどうかの適合試験を規定している。ソフトウェアテストでは、欠陥が存在することを示すことはできるが、欠陥が存在しないことは証明できない。ソフトウェアに仕様にない振舞がないことを保証する作業を証明といい、証明用のシステム、証明しやすい言語も多数存在している。本項では動的なソフトウェアテストを中心に扱う。.
新しい！!: プログラム仕様とソフトウェアテスト · 続きを見る »
ソフトウェアドキュメンテーション
フトウェアドキュメンテーションとは、コンピュータのソフトウェアに付随する文書、またはそのような文書を作成することを意味する。類似の用語としてソースコードドキュメンテーションがある。 仕様書を含むか、含まないかは立場により異なる。仕様書は設計/実装のために事前または事後に作成する文書である。ドキュメンテーションは開発中あるいは既に完成したソフトウェアに付随する文書を指す訳ではない。ソフトウェアに関する文書には作成する順番があるとは限らない。図からソフトウェアを生成する場合もあれば、ソフトウェアから図を生成する場合もある。ソフトウェアから仕様を生成する場合もあれば、仕様からソフトウェアを生成する場合もある。.
新しい！!: プログラム仕様とソフトウェアドキュメンテーション · 続きを見る »
ソフトウェア開発
フトウェア開発（ソフトウェアかいはつ、Software Development）とは、ユーザーのニーズやマーケティング上の目標をソフトウェア製品に変換する作業である。ソフトウェア開発には、ソフトウェア工学の研究的側面とソフトウェア製品を開発するマーケティング的側面が含まれていると言われることがある。ソフトウェア製品のマーケティング活動そのものは、必ずしも新商品開発とは結びつかない。顧客の期待を満足させるべく開発されたソフトウェア製品の成功/失敗の責任が工学的側面にあるのかマーケティング的側面にあるのかを判別するのは、多くの場合困難である。そのため、ソフトウェア開発全体として工学的側面とマーケティング的側面を共に理解し、それらの協調を促進することが重要である。工学とマーケティングの両方の側面をまとめ、バランスをとるのは、プロジェクトマネージャなどと呼ばれる立場の人である。 マーケティングとの関わりはソフトウェア要求分析としても知られている。ソフトウェア開発はクライアントが必要とするもの以上の機能を開発しようとしたり、逆に妥協しようとしたりする。そのため、ソフトウェア開発は通常の工学/技術とは関連付けられていなかった各種プロセス（市場調査、人材登用、リスクマネジメント、知的財産権、予算、危機管理など）まで取り込もうとする場合がある。その場合、ソフトウェア開発は Business Development と呼ばれる領域ともオーバーラップすることになる。 Alan M. Davis は著書 "Great Software Debates" の章 "Requirements" の節 "The Missing Piece of Software Development" で次のように述べている.
新しい！!: プログラム仕様とソフトウェア開発 · 続きを見る »
公理的意味論
公理的意味論（こうりてきいみろん、Axiomatics Semantics）とは、数理論理学に基づいてプログラムの正当性を証明する手法。ホーア論理と密接に関連している。.
新しい！!: プログラム仕様と公理的意味論 · 続きを見る »
表示的意味論
表示的意味論（ひょうじてきいみろん、Denotational Semantics）とは、計算機科学（理論計算機科学）の一分野で、プログラミング言語の形式意味論（プログラム意味論）の手法のひとつである。初期には「数理的意味論」（mathematical semantics）、「スコット-ストレイチー意味論」（Scott–Strachey semantics）のようにも呼ばれた。プログラムの意味をあらわす数学的オブジェクト（これを「表示」（denotation）と呼ぶ）を構築することで、プログラミング言語の意味論を形式化する手法である。 表示的意味論の起源は、1960年代のクリストファー・ストレイチーやデイナ・スコットの研究である。ストレイチーやスコットが開発した本来の表示的意味論は、プログラムの表示（意味）を入力を出力にマッピングする関数に変換するものである。後にこれはプログラムの表示（意味）を定義するには非力であることが証明され、例えば再帰定義関数・データ構造を表現できないことが判明した。これを解決するため、スコットはより汎用的な領域理論に基づいた表示的意味論を提案したS.
新しい！!: プログラム仕様と表示的意味論 · 続きを見る »
要求仕様
要求仕様（ようきゅうしよう、Requirements Specification）とは、工学分野において特定の製品やサービスがどうあるべきかを記述する文書を指す。主にシステム工学とソフトウェア工学で使われる用語である。英語のrequirementからリクワイアメント（リクワイヤメント）ともいう。 従来からの工学的手法では、要求仕様を入力として製品開発における設計工程が行われる。 要求仕様作成工程の前に一般に実現可能性調査（feasibility study）や概念的分析の工程が置かれることがある。要求仕様作成工程は、要求収集（関係者からのヒアリングなど）、要求分析（一貫性と完全性の検証）、要求定義（開発者に要求を理解させるための文書を作成）、要求仕様記述（要求と設計の橋渡しとなる文書を作成）の各工程にさらに分けることができる。.
新しい！!: プログラム仕様と要求仕様 · 続きを見る »
要求分析
要求分析（ようきゅうぶんせき、Requirements Analysis）とは、システム工学やソフトウェア工学において新たなシステムやシステム更新に際しての調査/定義に関わる工程を指す。要求分析はシステム設計工程でも重要な部分であり、アナリストやシステムエンジニア/ソフトウェア開発者が顧客の必要性や要求を特定する工程である。顧客の要求が特定されたら、システム設計者がその解決策を設計することになる。.
新しい！!: プログラム仕様と要求分析 · 続きを見る »
詳細化
詳細化（しょうさいか、Refinement）とは、形式手法において、抽象的な形式仕様記述から具体的な実行プログラムへと検証可能な変換を行うことである。 段階的な詳細化として段階を踏んで詳細化を行うこともできる。論理的には、詳細化は含意による変換であるが、追加的な複雑化を生じる要因もある。 詳細化の反対語は抽象化である。.
新しい！!: プログラム仕様と詳細化 · 続きを見る »
VDM
VDM（Vienna Development Method）は、IBMのウィーン研究所で1960年代から70年代にかけて開発された形式手法。 その仕様記述言語VDM-SLは1996年にISO標準（ISO_IEC_13817-1）となっている。VDM-SLをオブジェクト指向拡張したVDM++も、欧州連合ESPRIT計画のAFRODITEプロジェクトで開発された。.
新しい！!: プログラム仕様とVDM · 続きを見る »
Z言語
Z言語 (ぜっどげんご) は、Z記法 (ぜっどきほう) ともいい、形式仕様記述言語であり、コンピュータシステムの記述とモデリングを行うために使われる。 ZはZF集合論から名前をとって命名された。 Zは次のことに焦点を当てている。.
新しい！!: プログラム仕様とZ言語 · 続きを見る »
操作的意味論
操作的意味論（そうさてきいみろん、Operational Semantics）とは、プログラムの意味を数学的に厳密に与える計算機科学の手法の一種（プログラム意味論参照）。.
新しい！!: プログラム仕様と操作的意味論 · 続きを見る »
数学
数学（すうがく、μαθηματικά, mathematica, math）は、量（数）、構造、空間、変化について研究する学問である。数学の範囲と定義については、数学者や哲学者の間で様々な見解がある。.
新しい！!: プログラム仕様と数学 · 続きを見る »
