appD - Splint翻訳 Wiki - Splint翻訳

Up: マニュアル

Prev: Appendix C Annotations（アノテーション）

Next: Appendix E Annotated Bibliography（文献解題）

Section：1　2　3　4　5　6　7　8　9　10　11　12　13　14　A　B　C　D　E

Appendix D Specifications（仕様）

プログラムについてのより詳細情報を提供するもう一つの方法は、 形式仕様記述（Formal Specification）です。この文章は 主に仕様を無視していますが、Splintは当初、ソースコートのアノテーションの代わりに LCLの仕様の中の情報を使用するように設計されました。 追加の仕様ファイルを維持するよりもソースコードへアノテーションを追加する方が 労力が少なくないため、このドキュメントはアノテーションに焦点を当てています。 アノテーションはSplintのチェックに関連のあるLCLの仕様の中で表現できる全てのもの を表現することが可能です。 しかし、LCLの仕様はSplintのアノテーションで可能であるよりも プログラムインタフェース上でより正確なドキュメントを提供することが出来ます。 この付録（appendix）（[Evans94]から抜き取った）はLCLの仕様へのとても簡単な導入 です。詳細については、[GH93]を参照してください。

言語のラーチファミリー（Larch family）は2段重ねの形式仕様記述に近いです。 仕様は2つの言語を使用して構築されています。—Larch Shared Language (LSL)、 これは実装言語から独立しています。そして、Larch Interface Languageは特定の実装言語向けに設計されています。 LSLの仕様はsorts（ソート）、プログラミング言語の抽象型に類似のもの、 operators（演算子）、プロシージャに類似のものを定義しています。 これは抽象化の根底にある意味を表現しています。

インタフェース言語は特定のプログラミング言語の抽象化へのインタフェースの 仕様を定めます。 抽象化を使用することでクライアント（訳注：使う側のこと）が必要とする インタフェースの詳細を表現し、そして、正しい実装とモジュールの使用の両方に 制約を課します。 インタフェースの文法は、基本型、ソート、そして、LSLの仕様の中で定義された 演算子を使用して記述されています。 インタフェース言語はいくつかのプログラミング言語に対して設計されています。

LCL [GH93, Tan95]は標準C言語向けの ラーチインタフェース言語です。 LCLはC言語のような文法を使用します。 伝統的に、C言語モジュールMはソースファイルM.cと ヘッダーファイルM.hで構成されます。 ヘッダーファイルは、外部公開される関数、あるいは定数を実装するマクロ定義や 外部公開される型の定義と同じように、 Mによって 外部公開される関数、変数、定数のプロトタイプ宣言を含んでいます。 LCLの使用時、モジュールは2つの追加のファイル— M.lcl、Mの形式仕様記述、それから、M.lh、 （lhフラグがオンであれば、）M.lclから Splintによって導出される —を含みます。 クライアントは、 ドキュメントに対し、 M.lclを使用し、 どの実装ファイルも見る必要はありません。 導出されたファイル、M.lhには、 （Mが 他の指定されたモジュールに依存している場合）ディレクティブ、関数プロトタイプ、 それと、M.lclの中で 指定された変数の宣言が含まれます。 ファイルM.hは M.lhを 含むべきであり、古いM.hの 実装面を保持するべきであるが、しかし、クライアントとドキュメントに対して もはや使用はされていません。

Specification Flags（仕様フラグ）

これらのフラグはSplintがLCLの仕様で使用されている場合だけ、関係します。

Global Flags（グローバルフラグ）

lcs

(インポートのために使用される) .lclファイルの シンボリック状態を含む .lcsファイルを生成します。 デフォルトでは、.lcsファイルは 処理された各 .lclファイルに対して生成されます。 .lcsファイル の生成を防ぐためには、-lcsを使用して下さい。

lh

.lhファイルを生成します。 デフォルトでは、-lhが設定されおり、 .lhファイルは 生成されません。 .lhファイルの生成を有効にするには +lhを使用してください。

i <file>

<file>に LCL初期化ファイルを設定します。 任意の.lclファイルが コマンドライン上でリスト化された場合に、LCL初期化ファイルが読み込まれます。 デフォルトのファイルは、 LARCH_PATH 上で見つかった、lclinit.lciです。

lclexpect <number>

正確に<number>個の 仕様エラーが予期されています。 仕様エラーは仕様を確認するときに検出されたエラーです。 これらはソースコードには依存しません。

Implicit Globals Checking Qualifiers（暗黙のグローバルチェック修飾子）

m:-++-　imp-checked-spec-globs

チェックされていないアノテーションがあるLCLファイルの中で指定されたグローバル変数の暗黙的なchecked修飾子です。

m:----　imp-checkmod-spec-globs

チェックされていないアノテーションがあるLCLファイルの中で指定されたグローバル変数の暗黙的なcheckmod修飾子です。

m:---+　imp-checkedstrict-spec-globs

チェックされていないアノテーションがあるLCLファイルの中で指定されたグローバル変数の暗黙的なchecked修飾子です。

Implicit Annotations（暗黙のアノテーション）

P: -　spec-glob-imp-only

割り当てられていないアノテーションがあるLCLファイルの中のグローバル変数宣言の暗黙的なonlyアノテーションです。

P: -　spec-ret-imp-only

割り当てられていないアノテーションがあるLCLファイルの中の戻り値の宣言に暗黙的なonlyアノテーションです。

P: -　spec-struct-imp-only

割り当てられていないアノテーションがあるLCLファイルの中の構造体フィールドの宣言に暗黙的なonlyアノテーションです。

shortcut　spec-imp-only

spec-glob-imp-only、spec-ret-imp-onlyとspec-struct-imp-onlyを設定します。

Macro Expansion（マクロ展開）

P: +　spec-macros

指定された識別子を定義するマクロは展開されず、仕様に応じてチェックされます。

Complete Programs and Specifications

m:-+++　spec-undef

関数、変数、イテレータまたは定数が指定されていますが、定義されていません。

P: -　spec-undecl

関数、変数、イテレータまたは定数が指定されていますが、宣言されていません。

P: -　need-spec

構文上のコメントで重複していない仕様上の情報があります。 通常、これはエラーではありませんが、仕様がこの情報を使用することがない不完全なシステムを確実にチェックするためには、それを検知することは有益でしょう。

shortcut　export-any

公開されているが、指定されていない任意の識別子に対して、エラーが報告されます。（以下の全てのexportフラグを設定します。）

m:---+　export-const

定数が公開されていますが、指定されていません。

m:---+　export-var

変数が公開されていますが、指定されていません。

m:---+　export-fcn

関数が公開されていますが、指定されていません。

m:---+　export-iter

イテレータが公開されていますが、指定されていません。

m:---+　export-macro

展開されたマクロが公開されていますが、指定されていません。

m:---+　export-type

型定義が公開されていますが、指定されていません。

このドキュメントはSplint(英)のサイトを元に作成しました

Up: マニュアル

Prev: Appendix C Annotations（アノテーション）

Next: Appendix E Annotated Bibliography（文献解題）