タグ

specification-languageに関するnabinnoのブックマーク (3)

  • 仕様及び記述言語 - Wikipedia

    この記事は検証可能な参考文献や出典が全く示されていないか、不十分です。 出典を追加して記事の信頼性向上にご協力ください。(このテンプレートの使い方) 出典検索?: "仕様及び記述言語" – ニュース · 書籍 · スカラー · CiNii · J-STAGE · NDL · dlib.jp · ジャパンサーチ · TWL (2015年6月) 仕様及び記述言語(しようおよびきじゅつげんご、SDL: Specification and Description Language)は、システムの仕様を記述するための言語であり、曖昧さのない仕様記述を実現するために作られた。主な対象は受動的な分散システムである。スウェーデンの計算機科学者イヴァー・ヤコブソンは、ソフトウェア開発を行うために青写真 (blueprints) が必要であると考え、仕様記述言語、 SDL(Specification and

  • 形式手法 - Wikipedia

    Z言語を使った形式仕様記述の例 形式手法(けいしきしゅほう、英: formal methods)は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である[1]。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている[2]。 形式手法は理論計算機科学の様々な成果を基盤として応用したものであり、数理論理学、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う[3]。 分類[編集] 形式手法はいくつかの水準で使用可能である: 水準0 形式仕様記述を行い、プログラム自体を非形式主義的に行う。「軽い形式手法」と呼ぶ。費用対効果が早く得るこ

    形式手法 - Wikipedia
  • 仕様記述言語 - Wikipedia

    仕様記述言語(しようきじゅつげんご)は、システムなどの仕様を記述する、コンピュータ言語(すなわち形式言語)である。形式的でない仕様記述もあるが(後述)、そういったものを含めて何らかの主張がされている場合もある。 プログラミング言語がシステムそのものに変換されるのに対し、仕様記述言語は必ずしもシステムに自動変換されるものではなく、あくまで仕様の妥当性を検証することに重きを置いている。ソフトウェア工学における一般的な設計プロセスの位置づけから、多くはプログラミング言語を記述する前段階に記述されることを期待している。 仕様記述と検証の方法について説明する。仕様記述では、何らかのシステムの仕様を論理学的あるいは代数学的に、形式的に記述する(形式仕様記述)。検証では、論理学や代数学に基づき(すなわち「機械的」に)、無矛盾性などといったシステムにおける「好ましい性質」の保証、あるいはデッドロックの可能

  • 1