Guidedog / ドキュメント 0.2.0

アルゴリズムより先に不変条件¶

役に立つ不変条件は、実行中に保たれることと、終了後に呼び出し側が頼れることを示す。ループを書く前にそれを書く。

先行順走査の部分木区間¶

木を先行順で出力すると仮定する。各ノードは子より先に出力され、部分木は連続する。\(e_i\) をノード \(i\) と全ての子孫の直後の添字とする。

(3)¶\[\operatorname{subtree}(i) = [i,e_i), \qquad i < e_i \le N.\]

命題。 添字を \(e_i\) に進めれば、部分木を飛ばせる。

証明。 連続性により全ての子孫は \(e_i\) より前にある。排他的な終端の定義により、以後のノードは \(e_i\) 以降にある。そこへ進めば部分木だけを飛ばせる。レンダラーが頼る前に、バリデーターが仮定を検査する。

全体走査は各ノードを一度訪れ、走査コストは \(O(N)\)。部分木のスキップは添字の更新一回で済むが、ペイロード処理には相応のコストがある。定数時間のスキップを定数時間の描画と混同しない。

レンダラーはまずバイト数 \(m\) を測る。呼び出し側の出力容量を \(c\) とする。

\[m \le c \quad \Longrightarrow \quad \text{出力を開始できる}.\]

測定と出力の走査は同じ規則を使う。成功時は正確に \(m\) バイトを書く。失敗時に有効な部分成果物は返さない。公開はホストが担うため、不完全なバイト列が以前の出力を置き換えることはない。

キャッシュキーは結果を変え得る全データを含める。ソースだけでは足りない。インクルード、テンプレート、設定、参照検索、リソース、アダプターの版も出力に影響する。記録した依存関係が一致するときだけ再利用できる。キーが一致しても出力がなければ無効。

テストではコア境界に失敗するアロケーターを置き、出力内容を比較する。インポートも監査する。割り当て数だけを数えて結果を見なければ、拒否で文書の一部を黙って捨てる不具合を見逃し得る。