Masao Ito (NIL)
Jan/7/2020

SPARK/Ada
英日辞書
SPARK/Ada
English-Japanese Dictionary

はじめに
SPARK/Ada における新しい概念は，単に日本語に置き換えただけでは，理解することができません．日本語が示す範囲と異なる可能性があります．場合によって，カタカナでそのまま受け入れる必要があります．

必要と思える箇所には，簡単な説明を付けています．

A/S は，Ada と SPARK の略です．A は Ada言語で用いるもの．S は SPARK で用いるものです．SPARK は，Ada 言語のサブセットなので，Ada 用語も利用します．

参照先は，以下です．
ARM: ISO/IEC 8652:2012(E) Ada Reference Manual
SUG: SPARK 2014 User’s Guide https://docs.adacore.com/spark2014-docs/html/ug/index.html

SPARK英日辞書（V1.0）

1（English Version）
SPARK/Ada
English-Japanese dictionary
Introduction
The new concepts in SPARK/Ada cannot be understood by simply replacing them withJapanese. It may be different from the meaning indicated in Japanese. In some cases, you may
need to accept katakana as is.
Where it seems necessary, a brief description is provided.
A/S stands for Ada and SPARK. A is the term used with the Ada language. S is for use withSPARK. SPARK is a subset of the Ada language, so it also uses Ada terminology.
References
ARM: ISO/IEC 8652:2012(E) Ada Reference Manual
SUG: SPARK 2014 User’s Guide https://docs.adacore.com/spark2014-docs/html/ug/index.html

SPARK英日辞書（V1.0）

2

A
英語

日本語

A/S

access type

アクセス型

Aaggregate

集成式

A

補足
Cにおけるポインタと同様，ただ，それ自身が型であることに注意が必要である．ARM 3.10
一般の配列およびレコード型（構造体）に対して値を与える方法．array aggregate といえば，配列集成式．
ARM 4.3

alias

別名（化）

A

同一オブジェクトを指す複数の名前のこと．エイリ
アス．明示的に別名を作成する aliased 予約語がある
ARM 3.3.1． SPARK では，別名は証明の妨げとなるため，使用しないことを推奨している．

array

配列A

同一の副型を要素として持つ複合型．添字と要素において型定義が可能である．Cなどの配列とは異なっている．ARM 3.6

assignment

代入A

オブジェクトの値を，右辺データ表現の評価結果に置き換える．制限付き副型への代入時には，範囲検査が行われる．ARM 5.2
Ada 2012 で導入された概念．with節とともに示す．

aspectassertion/
assert

アスペクト

表明AA

SPARKは，契約表現等をこのアスペクトを用いて行う．アスペクト指向プログラムのアスペクトとは無関係である契約を示す事前・事後条件等．契約には，「表明」が必要である．プラグマassert文は，証明時に検査対象となる SUG 5.6.1「スイッチ --assumptions が設定されたとき,assumption

仮定／前提

S

GNATprove は，その結果ファイル gnatprove.out 中の残っ ている仮定についての情報を出力します.」SUG
6.3.5

SPARK英日辞書（V1.0）

3

type Integer_Access is access all Integer;
V : Integer_Access := new Integer;
アクセス型の例

type Singleton is record
V : Integer;
end record;
V1 : Singleton := (V => 0);
集成式の例

SPARK英日辞書（V1.0）

4

B
日本語

A/S

補足

ボディ部／実体部A

単にボディ部と呼ばれる場合もある．仕様部に対応し，仕様部記述に対する実現を記述する

英語
body

SPARK英日辞書（V1.0）

5

C
日本語

A/S

check

検査／検査項目S

例えば，GNATprove による検査を指す

child package

子パッケージA

パッケージ内に包含されるパッケージ．柔軟に入れ子構造を取れるという特徴がある

英語補足

レコード型，配列型などの総称（ARM 3.2） JISXでcomposite type

複合型

A

は，構造型という訳語を与えている．Cなどの構造体との関係が連想されるため，避けている

component

コンポーネント／要素A

一般的には，コンポーネントとカタカナにする．配列要素を指す場合もあり，そのときは単に要素を指す

completion

完結化

A

実行時準備処理時に，必要な情報を補うこと

consequence

帰結S

特別な使い方としては，ケース文でガード条件が真の場合に選ばれる式を指す場合がある

constrainedarray

制限付き配列型

A

添字範囲が確定している配列型

constraint

制約A

副型の宣言時に加える制限のこと． ARM 3.2.2

S

契約型設計に由来する．
副プログラム契約：副プログラム（手続き・関数）がサービスを提供するためには，事前条件を満足していないといけない．その代わりに手続き・関数は，事後条件を満足するということを「契約」として表現する．
パッケージ契約：広域変数の状態・初期化，パッケージの初期化を規定する
型契約：スカラー型範囲，レコード型区別子，述語

contract

controlled type

契約

被制御型

A

タグ付き型の一つで，インスタンスを開放するときに（finalization），ユーザ指定による特別な処理を必要とする場合に用いる型．ARM 7.6

SPARK英日辞書（V1.0）

6

D
英語A/S

日本語

補足

derived type

導出型

A

他の型によって定義された型． ARM 3.4

discrete type離散型

A

曜日や交通信号の色といった離散的な値をとる型．
「型（type）」の項参照. ARM 3.5.5, 3.6.1

A

複合型のパラメータ化に用いる．判別子という訳語を用いる場合もある．オブジェクトの生成時には，制約を加える必要がある．ARM 3.7

discriminant

区別子

type Shape_Kind is (Circle, Line, Torus);
type Shape (Kind : Shape_Kind) is record
X, Y : Float;case Kind iswhen Line=>

X2, Y2 : Float;
when Torus=>

Outer_Radius, Inner_Radius : Float;
when Circle=>

Radius : Float;
end case;end record;

区別子の利用例（パラメータ化されたレコード型）

SPARK英日辞書（V1.0）

7

E日本語

A/S

補足elaboration

実行時準備処理A

メインが呼ばれる前に行われる実行系の処理を指す

enclosingconstruct

内包構成要素A

変異レコード型における構成要素

entry family

エントリー属A

タスキングにおける同一名のエントリー集合

enumeration
type

列挙型

Aexpression

式A

ARM 4.4

expressionfunction式関数

A

仕様部で実体部の内容を内包している小さな関数のこと．ARM 6.8

英語

SPARK英日辞書（V1.0）

Cと異なり位置に対する整数は与えられない．「型（type）」の項参照．ARM 3.5.1

8

F
日本語

A/S

補足

failed

不合格となったS

証明後のメッセージに表示される場合がある．通常
は反例とともに示される

flow analysis

フロー分析

S

データフローを検査すること．SUG 5.2.5

formalparameter

仮パラメータA

一般の言語における仮引数に相当する

S

何らかの数学的モデルに基づいて仕様の（表明）内容が実現されていることを証明すること．SPARKに英語

formalverification

形式検証function

関数おいては，演繹的方法を用いる

SPARK英日辞書（V1.0）

A

副プログラムの一つ．返り値を持ち，返り値をムシすることはできない．ARM 6.59

G
英語

日本語

A/S

補足
一種のテンプレートであり，パラメータ化することができる．汎用副プログラムないしは，汎用パッケージを作ることができる．C++等のテンプレート

generic unit

汎用体

Aは，この汎用体概念を取り入れたもの．Adaは強い型付けを特徴とするため，汎用体を使わないとさまざまなパッケージを作ることになってしまう．総称体．ARM 12

ghost code

ゴーストコードS

主として検証を容易にするために用いるコード．スイッチによりコンパイル時には削除できるために，ゴーストという名がある．ゴースト関数，ゴースト変数，ゴースト型，ゴースト手続き等がある．SUG 5.5.10

global

広域S

スコープが広域であること．フロー分析用のデータ依存に関するアスペクト記述にも用いる

SPARK英日辞書（V1.0）

10

H
日本語

A/S

妥当性を持つS

英語
holdSPARK英日辞書（V1.0）

補足

11

I
英語

日本語

A/S

補足

illegal

規則違反-

文法規則に違反していること

index

添字

A

配列における添字として，或いは，タスキングでのエントリー属における添字として使用する ARM 9.1

instance

実体／インスタンスA

オブジェクト指向で使われるインスタンスと基本的には同じ．オブジェクトの項も併せて参照のこと

instantiate

実体化A

汎用体を実体化すること．ARM 12.3

integrity

完全性-invariant

不変条件

A

安全性や信頼性を強く要求されるシステムを，HighIntegrity System と呼ぶ．ARM Annex H
実行中に変化しない変数等の値．ループ不変条件，型不変条件がある．ループ不変条件（loop invariant）
および型不変条件（type invariant）の項参照

SPARK英日辞書（V1.0）

12J
英語justify

日本語

正当化

A/SS

補足
証明器で証明が困難だが，他の手段によって明らかに正しいと分かっている場合に，注記を付加すること
で，証明範囲から，該当箇所を外すことが可能である．pragma Annotateを用いることで，代替できる．
SUG “Uses of Pragma Annotate GNATprove”

SPARK英日辞書（V1.0）

13

L
英語日本語

A/S

補足
SPARKには，専用の補題のライブラリがある．SUG5.10.3．補題とは，（数学的には）既に証明済みの定理であり，証明したいこと（定理）から見ると補助的な役割を果たすものである．ここでは，既に明らかであるものとして，証明器に対してユーザが与える補助的定理のことを指している．それ自身が実際に正しいかどうかを示すのは，ユーザの責務である．

lemma

補題

S

limited type

限定型

A

等値演算子を持たず，同一型同士であっても代入ができない型 ARM 7.5

linked list

連結リスト

S

SPARKライブラリに含まれるデータ構造の一つ

loop invariant

ループ不変条件S

表明の一つ．ループ中で変化しないプロパティを示す．SUG 5.6.3loop variant

ループ変化条件S

表明の一つ．ループ中でのスカラー値の変化（増加・減少）を規定する．SUG 5.6.4

Prop := False;
for J in 1 .. 10 loop
pragma Loop_Invariant (Prop);
Prop := True;end loop;

ループ不変条件
最初のループでは不変条件はFalseになるが，それ以降ではTrueとなる

SPARK英日辞書（V1.0）

14

procedure Terminating_Loops (X : Natural)with SPARK_ModeisY : Natural;
begin
Y := 0;while X - Y >= 3 loop
Y := Y + 3;
pragma Loop_Variant (Increases => Y);
end loop;
Y := 0;while X - Y >= 3 loop
Y := Y + 3;
pragma Loop_Variant (Decreases => X - Y);
end loop;
end Terminating_Loops;

ループ変化条件
上記の例では，増加・減少の変化条件は全て真となる

SPARK英日辞書（V1.0）

15

M
A/S

英語

日本語

memorycorruption

メモリ不斉-modular type

剰余型

Amodularity

モジュール性-SPARK英日辞書（V1.0）

補足

剰余の値を返す型．「型（type）」の項参照．ARM
3.5.4

16

N
英語

日本語

A/S

nullヌルAnull procedure

ヌル手続き

A

null record

ヌルレコード型

A

SPARK英日辞書（V1.0）

補足
予約語．ARM 2.9. 例えばアクセス型を初期化しない
場合，指している領域は，ヌルとなる

ARM3.3.1

実体部を持たない手続き宣言の簡略版．ARM 6.7
要素を持たないレコード型．record null; end recordに同じ．ARM 3.817O
A/S

補足

オブジェクトA

一般には変数の意味で用いる．あるメモリ領域を占めるものを指す．オブジェクト指向でいうオブジェク
ト・インスタンスと同じではありません．かつて
は，「算体」という訳語与えられていた

オーバーロードA

副プログラムオーバロードや演算子オーバロードといった一般的なオブジェクト指向プログラムにおける意味と同じ．ARM 6.4, 6.6

英語objectoverload

日本語

SPARK英日辞書（V1.0）

18

P
日本語

A/S

package

パッケージ

A

Ada言語におけるプログラム単位．ARM 7parmeter

パラメータ

A

引数

part

領域／部

A

例えば，body part はボディ部と呼ぶ

postcondition

事後条件

A

手続き・関数が実行後に満足しているべき条件．契約の項参照．ARM 6.1.1

pragma

プラグマ

A

一般的なプラグマと同じ．コンパイラに対する指示を示す．ARM 2.8 pragmas

precondition

事前条件

A

手続き・関数が実行する前に満足すべき条件を示す．
ARM 6.1.1predicate

述語Aprivate

非公開A

かつては，密閉型という訳語が与えられていた．プ
ライベートとカタカナにする訳語もある．ARM 7.3

procedure

手続きA

副プログラムの一つ．関数と異なり返り値を持たな
い．ARM 6.5.1
演繹的に命題或いは論理式の正しさを示すこと．プ
ログラムにおいては，表明に記された命題或いは論理式が，実装と合っていることを示す

英語

proof

証明S

prover証明器

Sprotected type

public

保護型

公開

SPARK英日辞書（V1.0）

補足

副型のプロパティを表現するために用いる．ARM
3.2.4 subtype predicate

例えば，CVC4などの定理証明ツールを指す．SUG“SPARK architecture, quality assurance and maturity”

A

複合型の一つ．その要素は，複数のタスクから並行的にアクセスされる保護操作を通じてのみアクセス可能であるAスコープの一つ．パッケージにおいては，デフォルトのスコープ．パッケージ利用者は，その仕様部で公開されている情報を利用できる

19

Q
英語qualification

日本語型限定SPARK英日辞書（V1.0）

A/S
A

補足
ある型の所属を示す．例えば P.T とするとき，型 Tは,パッケージ P で定義している T 型に限定される

20

R
英語

日本語

A/S

補足

recordレコード

A

構造体に類似している．歴史的には「記録」が訳語として用いられた．ARM 3.8

representation

データ表現

A

データ構造表現という意味の場合もある

SPARK英日辞書（V1.0）

21

S
英語

日本語

A/S

scalar type

スカラー型

Ascope

スコープ

A

補足
単一の値をとる型．「型（type）」の項参照．ARM
3.5
可視範囲．一般的な言語と同様の意味を持つが，細かな制御が可能である
ブール演算子 and, or は省略制御ではなく，常に両オ

short-circuitcontrol

省略制御

signed integertype

符号付き整数型

A

処理系により定まる最小値と最大値を持つ．他の整数型は，剰余整数型．ARM3.5.4

statement

命令文A

或いは単に「文」

storage pool

記憶域プールA

オブジェクトの型により，記憶域プールの一部がAllocator により割り当てられる．ARM 13.11

subtype

副型

A型から導出される新しい型．副型が示す範囲は，導出もとに対して，常に狭い範囲をカバーする

subprogram

副プログラムA

手続きと関数のこと

A

ペランドを評価する．”and then” “or else” は省略制御形式である ARM 4.5.1

suspension object という場合，同期に関係する．
suspension

保留A

Ravenscar特有のオブジェクトを指す（セマフォー）
場合がある．

SPARK英日辞書（V1.0）

22

T
英語

日本語

A/S

tagged type

タグ付き型

A

補足
型拡張可能な型のこと．ARM 3.9
Adaにおいては，抽象データ型を指す．型を厳密に定type

A型

義することで，暗黙的な型変換や勘違いによる異なる型同士の演算を検出する．静的にプログラム誤りをみつけるために型を用いる．このような言語は，「強い型付け（strong-typing」の言語と呼ばれる．
基本型については，下図参照

type invariant

型不変条件

S

型の要素が持つ不変条件を示す．例えば，円の中の各点は，中心から一定の距離内にあることを示す．これは個別の座標 X, Y だけでは表現できない．ARM
7.3.2

Ada言語定義基本型（一部：ARM3.2）

SPARK英日辞書（V1.0）

23

package Root_Pkg istype Root_Type is tagged
record-- component1-- component2-- etcend record;
procedure Op1(params);
procedure Op2(params);
function Op2(params) return Return_Type;-- etcend Root_Pkg.

ベース Root_Type 型（タグ付き型）

with Root_Pkg; use Root_Pkg;
package Extended_Pkg istype Extended_Type is new Root_Type withrecord-- component3 (extension)
end record;
procedure Op1(params); -- override Op1
procedure Op4(params); -- new operationend Extended_Pkg;

Root_Type型を拡張した Extended_Type 型

SPARK英日辞書（V1.0）

24

U
日本語

A/S

unconstrainedarray

無制約配列型A

範囲指定がない配列

unconstrainedtype

無制限型

A

範囲指定がない型．例えば，String型

英語

SPARK英日辞書（V1.0）

補足

25

V
英語

日本語

A/S

variant record

変異レコード型

A

SPARK英日辞書（V1.0）

補足
要素を可変にできるレコード型. discriminant （区別子）参照

26