値の契約

Annotated で型に Refine(lambda ...) を付けます。最初の引数は制約する値です。複数の述語はすべて満たす必要があります。

from refinepy import Refine
from typing import Annotated

Nat = Annotated[int, Refine(lambda v: v >= 0)]

def increment(x: Nat) -> Annotated[int, Refine(lambda result, x: result == x + 1)]:
    return x + 1

from collections.abc import Sequence

def at(
    xs: Sequence[int],
    i: Annotated[int, Refine(lambda v, xs: 0 <= v < len(xs))],
) -> int:
    return xs[i]

追加の引数は関数入口の入力を指定します。引数の契約では先行する引数、戻り値の契約では全引数を参照できます。本体で再代入しても、契約内の入口の値は変わりません。

型エイリアスとローカル宣言の述語は引数を1つ取ります。count: Nat = 0 などのローカル契約は後の代入にも適用します。引数の契約は入口だけを制約します。関数の引数と戻り値には型が必要です。ローカルの型は推論できます。

Literal と固定長タプル

Literal は値を、同じ基本型の int、bool、str、None の非空のリテラル集合に制限します。符号付き整数、静的な型エイリアス、引用した型注釈に対応します。

from refinepy import Refine
from typing import Literal

Mode = Literal["read", "write"]

def switch(mode: Mode) -> Mode:
    return "write" if mode == "read" else "read"

def reverse_pair(pair: tuple[Literal[0, 1], Mode]) -> tuple[Mode, Literal[0, 1]]:
    return pair[::-1]

基本型の混在、計算した値や名前、enum、入れ子の Literal は未対応です。True は Literal[1] を満たしますが、整数の 1 は Literal[True] を満たしません。既定値は定義時に基本型、使用時に細分化の条件を検査します。

固定長タプルは構築、リテラル添字、連結、等価比較、非ゼロの静的ステップによるスライスに対応します。境界は静的な値、省略、None に限ります。空スライスや結果が既知の比較でも、全フィールドを評価して検査します。等価比較は再帰的で、リストのフィールドには比較可能な一致する要素型が必要です。マッピングと抽象シーケンスのフィールドの等価比較は未対応です。長さや無関係なスカラー型が異なる場合は不等になります。

順序は、互換性のある整数・bool、文字列、入れ子のタプル、対応する None のフィールドを辞書式に比較し、同じ接頭辞なら長さで決まります。共通フィールドが省略可能型やコンテナーなら拒否します。入れ子の値を含められますが、別名は残ります。更新したリストをタプルに格納したり、フィールドからリストを取り出したりしても、書き込み可能な所有権は得られません。

事前条件

@requires(lambda ...) は、後に宣言した引数も含めて入口の入力を制約します。複数の事前条件はすべて満たす必要があります。

from refinepy import requires

@requires(lambda xs, i: 0 <= i < len(xs))
def read_at(xs: Sequence[int], i: int) -> int:
    return xs[i]

requires、ensures、decreases は、通常の必須位置引数を持つリテラル lambda を、位置引数として1つ取ります。インポート、別名、再エクスポートに対応します。同名のユーザー関数は対象外です。@reflect に括弧は付けません。reflect と decreases の重複はエラーです。デコレーターの順序は影響しません。定義より前に、TYPE_CHECKING の外でインポートする必要があります。他のデコレーターと旧式の関数コメント指示は未対応です。

呼び出しは引数の契約と事前条件を満たす必要があります。ソース内の呼び出し先を検証してから、その戻り値の契約を使います。デコレーターは実行時に述語を評価したり契約を強制したりしません。検証器は対象コードをインポートしません。

事後条件

@ensures は、必須の戻り値の基本型に述語を加えます。最初の引数は結果、残りは不変な入口の入力です。-> None では結果の引数を省き、lambda: proposition も使えます。

from refinepy import ensures

@ensures(lambda result, n: result == n + 1)
def increment(n: int) -> int:
    return n + 1

@ensures(lambda n: n + 0 == n)
def identity_lemma(n: int) -> None:
    return None

複数の ensures と戻り値の Refine はすべて満たす必要があります。各述語は独立に安全に評価できる必要があり、自分や他の述語の定義可能性を正当化できません。定義を取り込む関数には細分化のない戻り値が必要で、ensures は使えません。

停止性の尺度

直接再帰する関数には @decreases(lambda ...) を1つ付けます。引数は入口の入力です。尺度は整数、または通常の整数からなる非空の平坦なリテラルタプルです。各自己呼び出しで定義可能性と厳密な減少を示し、現在と次の全成分を非負に保ちます。スカラーなら 0 <= next < entry です。タプルは辞書式に比較し、先行成分が減れば後続成分は増やせます。基底ケースの尺度は非負でなくても構いません。bool の成分は拒否します。

ループ直前の decreases(lambda ...) は、現在束縛されているヘッダーのローカル値を使います。通常の反復と continue では、最終反復も含め、次の尺度が定義可能、非負、かつ厳密に小さいことを示します。break、return、反復0回では減少は不要です。入れ子の各ループにも尺度が必要です。未束縛の for ターゲットや内部の反復カウンターは引数に指定できません。

呼び出し先も独立に停止する必要があります。減少は呼び出し結果の契約を使わずに検査するため、結果に依存する減少は未証明になる場合があります。信頼された外部モデルや相互再帰は停止性の根拠にできません。停止性を要求した場合、到達不能なループも含めて全ループに尺度が必要です。

verified だけでは正常に戻る場合の契約を保証します。停止性には対象関数とその呼び出し先の証拠が必要です。Python の再帰深度や利用可能な資源は保証しません。

静的アサーション

Assert は、その位置で命題を検査し、後の代入には契約を課しません。対象は確実に束縛済みの関数ローカル変数です。引用しない注釈に初期値を付けず、Assert をちょうど1つ指定します。

from typing import Annotated
from refinepy import Assert

def absolute(n: int) -> int:
    x = abs(n)
    x: Annotated[int, Assert(lambda value: value >= 0)]
    return x

基本型は現在の値と一致する必要があり、既存の細分化も検査します。lambda の最初の引数は現在の値、追加引数は現在束縛済みのローカル変数です。自由変数としてのローカル参照、既定値、可変長引数は未対応です。後の再代入で確立済みの事実は更新されません。

Assert(lambda v: P(v), using=lambda arg: lemma(arg)) は、戻り値が細分化された None のソース補題を直接1回呼び出します。引数と事前条件を検査し、補題の全呼び出し先の停止性を独立に証明する必要があります。外部モデル、ループ、相互再帰、循環するアサーションの証拠は静的証明に使えません。using を省くと、現在の事実と受け入れ済みの定義から命題を証明します。Python はこのローカル注釈を評価しません。引数、戻り値、エイリアス、入れ子の型、モジュール注釈には Assert を使えません。

定義の取り込みと補題

@reflect で検査済みの定義を述語から呼び出せます。入力と結果は細分化のない対応型にし、入れ子の細分化、事前条件、ensures は使えません。代入、平坦なアンパック、アサーション、分岐、return に対応します。ループとコンテナーへの書き込みは未対応です。使わない計算も含め、元の本体と全引数の評価が安全である必要があります。

補題は、戻り値の契約に命題を記述した検査対象関数です。Annotated[None, Refine(lambda _, x: ...)] や -> None と @ensures を使います。本体で命題を証明し、呼び出すと正常に戻る場合の契約を使えます。通常の契約だけでは、関数を論理式から呼び出せません。ガイドの例を参照してください。

再帰定義の取り込み

定義を取り込む関数は、宣言名で自身を呼び出せます。入力と結果は細分化のない対応型、本体はループなし、事前条件なしとし、整数の decreases 尺度を明示します。等式を使う前に本体の安全性と減少を検証し、他の呼び出し先も検証と停止性が必要です。

展開はスカラーだけのシグネチャで8層、コンテナーを含む場合は3層までです。残りの呼び出しは未解釈のままなので、偽の等式も含めて unknown になる場合があります。展開の制限で受け入れや証明が止まることもあります。相互再帰、別名での自己呼び出し、複合要素を持つコンテナーを含む再帰シグネチャは対象外です。有界展開を超える等式には、検査済みの帰納補題を使います。

帰納補題

戻り値が細分化された None の直接再帰関数は、整数または辞書式の decreases 尺度で命題を帰納的に証明できます。各自己呼び出しは契約と厳密な減少を満たす必要があり、宣言した戻り値の命題を局所的な帰納仮説として使います。基底ケースと再帰ケースの全 return で命題を証明します。減少は呼び出し結果の契約から独立に検査します。依存先は検証と停止性、ループは尺度が必要です。定義の取り込みは別途受け入れられる必要があります。

自動帰納探索と相互帰納は未対応です。尺度なしの補題は、正常に戻る場合の部分正当性だけを保証します。

コンテナーと省略可能な値

要素の契約はすべての有効な要素、外側の契約はコンテナーを制約します。読み取りには範囲やキーの存在の証明が必要です。シーケンスの負の添字と、T | None・Optional[T] の不在検査や型の絞り込みに対応します。

NonEmptyNats = Annotated[Sequence[Nat], Refine(lambda xs: len(xs) > 0)]

def first(xs: NonEmptyNats) -> Nat:
    return xs[0]

from collections.abc import Mapping

def port_or_zero(ports: Mapping[str, Nat]) -> Nat:
    port = ports.get("http")
    if port is None:
        return 0
    return port

新しい共有されていないローカルリストは、単独の append・extend、+=、整数添字による代入で更新できます。要素とリスト全体の細分化も検査します。入力・共有リスト、反復中のリストへの書き込み、pop、スライス代入、辞書への書き込みは未対応です。

新しいリストを返す検査済みのソースヘルパーは、1つのローカル名に書き込み可能な所有権を移せます。独立に確保され、共有のない可変コンテナーのタプルを返すヘルパーなら、left, right = split(xs) のような直接の平坦なアンパックでリストの所有権を移せます。借用・共有フィールド、先にタプルを保存する操作、入れ子のアンパックでは所有権を得られません。内容が等しい契約だけでは不十分で、全依存先と戻り値の全選択肢の検証が必要です。抽象 Sequence と省略可能な戻り値は所有権を移しません。

要素には対応するタプル、省略可能な値、入れ子のコンテナーを使えます。外側のリストを所有しても、取り出した内側のリストには書き込めません。更新した別のローカルリストを要素として格納すると拒否します。リストの等価比較は、細分化が異なっても、再帰的に比較可能な一致するスカラー、省略可能型、タプル、リストの要素型に対応します。抽象 Sequence とマッピングの要素は比較できません。連結には一致する要素契約が必要で、書き込み可能なコンテナー型は不変です。ガイドに例があります。

ループとアサーション

推論で必要な性質を示せない場合は、ループの直前に invariant(lambda ...) を置きます。引数は現在のヘッダーのローカル値です。停止性を要求するには decreases(lambda ...) を1つ加えます。

from refinepy import invariant, decreases

def count_to(n: Nat) -> Annotated[int, Refine(lambda result, n: result == n)]:
    i = 0
    invariant(lambda i, n: 0 <= i <= n)
    decreases(lambda i, n: n - i)
    while i < n:
        i += 1
    return i

各マーカーは必須引数を持つリテラル lambda を位置引数として1つ取ります。同じブロックで連続するマーカーは次のループに適用されます。間にコメントや空行は置けますが、他の文は置けません。インポート、別名、再エクスポートに対応します。実行時に述語は評価しません。旧式の不変条件コメントは受け付けますが非推奨です。

不変条件は開始時と各反復後に検査します。assert も証明義務であり、対応する述語の構文を使う必要があります。

対応構文と制限

構文が対応範囲内でも、すべての性質を証明できるとは限りません。未対応の構文、ソルバーの不確実性、解析やモデル復元の上限到達を検証成功として扱いません。

述語と組み込み関数

述語は bool を返し、宣言型と確立済みの事実の下で安全に評価できる必要があります。len(xs) > 0 and xs[0] >= 0 のように短絡ガードで読み取りを正当化できます。

リストリテラル、等価比較、連結、定数ステップのスライスを使えます。空リストには文脈からの要素型が必要です。タプルの構築、連結、静的スライスも使えますが、全フィールドの安全性を検査します。定義を取り込まないユーザー関数の呼び出し、明示的な量化、マッピング構築、内包表記は述語内では使えません。sum、all、any、sorted、isinstance、スカラー変換、第三者 API には既定のモデルがありません。

結果の適用範囲

検証済みの契約は、入口の契約を満たす入力とモデル化した組み込み実行環境に適用します。モデル化した実行時エラーと正常に戻る場合の契約を検査し、停止性は別の証拠で示します。Python の注釈は契約を強制しません。ブラウザーは単一モジュールを Python を実行せずに読みます。パッケージ解決と外部モデル登録はネイティブのワークフローで扱います。ページ移動には #/playground、#/guide、#/reference と見出しへのリンクを使えます。サンプルは #/playground/<sample> で指定し、bounds、fibonacci、squareRoot、series、rounding、division を使えます。

要確認は unproved、unknown、unsupported、失敗は counterexample、error をまとめたものです。個別の状態も表示します。レポート全体に診断がある場合は「すべて検証済み」にはなりません。状態の意味と停止性の要約はガイドを参照してください。