型 T とアドレス L について T@L をなす駐観 (at-view) は他の形の観をコンストラクトするブロックを形成します。 そのような形成されたブロックを一緒に配置するメカニズムはデータ観 (dataview) として宣言されます。 大部分においてそれはデータ命題 (dataprop) の宣言と同じです。 この章ではいくつかの一般なデータ観とその使い方を紹介します。
この章で解説するコードは オンライン から入手できます。
データ観 option_v は次のように宣言されます:
この宣言はデータ観 option_v が1番目の引数に対して共変で、 関連する2つの証明コンストラクタ Some_v と None_v があることを示しています。 観 V が与えられ、b がブールの時、option_v(V, b) はしばしばオプショナル観 (optional view) と呼ばれます。 明確に観 option_v(V, true) の証明は観 V の証明を含んでいますが、観 option_v(V, false) の証明は何も含んでいません。例として、次の関数インターフェイスはオプショナル観の典型的な使用例です:
型 T が与えられた時、 関数 ptr_alloc_opt<T> はオプショナル観の証明とポインタのペアを返します; もし返されたポインタが NULL でなければ、 ポインタが指す場所 L についてその証明は観 T?@L の証明に成ることができます; そうでなければ、返されたポインタに関連する駐観は含まれません。