ソースや関数の指定を変えると結果が消えます。サンプルの読み込みはソースと取り消し履歴を置き換え、ページの再読み込みは最初のサンプルに戻します。検証中はエディターが読み取り専用になります。

EN / JP で言語を切り替えます。ガイド・リファレンスへの移動や言語の切替では、編集中の内容を保持します。パネルの境界はドラッグ、またはフォーカスして矢印キーで調整できます。ブラウザーでは最大1 MiBの単一モジュールを扱い、Python を実行せずに検証します。

ページのリンクには #/playground、#/guide、#/reference を使えます。見出しへのリンクは #/reference/value-contracts の形です。従来の .html リンクも使えます。サンプルを選ぶとURLも更新します。#/playground/division を直接開くと、符号付き除算を読み込みます。

契約を書く

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

入力は非負、結果は入力より1大きい値である必要があります。x + 1 を x - 1 に変えると契約に違反します。

事前条件を付ける

from refinepy import requires

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

ensures で戻り値の契約を書く

戻り値の基本型と @ensures を組み合わせます。最初の引数は結果、残りは関数入口の入力です。戻り値が None の場合は結果の引数を省きます。

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

文字列を検証する

文字を読む前に、添字が範囲内にあることを証明します。文字列の内容比較、長さ、連結、ステップ1のスライスに対応しています。

from typing import Annotated
from refinepy import Refine, requires

@requires(lambda text: len(text) > 0)
def first(text: str) -> Annotated[str, Refine(lambda result: len(result) == 1)]:
    return text[0]

def append(left: str, right: str) -> Annotated[str, Refine(lambda result, left, right: len(result) == len(left) + len(right))]:
    return left + right

負の添字は末尾から数えます。文字列メソッドと f-string は未対応です。

整数で割る

事前条件や分岐で除数が0でないことを示します。商と余りは Python の切り下げと符号の規則に従います。

from refinepy import requires, ensures

@requires(lambda d: d != 0)
@ensures(lambda r, a, d: a == r[0] * d + r[1] and
    (0 <= r[1] < d if d > 0 else d < r[1] <= 0))
def divide(a: int, d: int) -> tuple[int, int]:
    return a // d, a % d

0になり得る除数をガードせずに使うと検証に失敗します。非線形演算や変数による除算の証明は unknown になる場合があります。

ローカルリストを作って更新する

新しいリストを1つのローカル名で保持すると、入力を変えずに更新できます。

from refinepy import requires, ensures

@requires(lambda xs, i: -len(xs) <= i < len(xs))
@ensures(lambda r, xs, i, value:
    len(r) == len(xs) and r[i] == value
    and r == xs[:i if i >= 0 else len(xs) + i] + [value]
        + xs[(i if i >= 0 else len(xs) + i) + 1:])
def replace(xs: list[int], i: int, value: int) -> list[int]:
    out = xs[:]
    out[i] = value
    return out

append、extend、+=、整数添字による代入に対応します。空リストには out: list[int] = [] などの型が必要です。更新後も要素とリスト全体の契約を検査します。入力リスト、共有された別名、取り出した入れ子のリストには書き込めません。ヘルパーの戻り値の所有権と制約はリファレンスを参照してください。

再帰の停止性を検証する

@decreases で、直接の再帰呼び出しごとに尺度が減ることを示します。

import refinepy
from refinepy import Refine
from typing import Annotated

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

@refinepy.decreases(lambda n: n)
def count(n: Nat) -> Annotated[int, Refine(lambda r, n: r == n)]:
    return 0 if n == 0 else 1 + count(n - 1)

再帰の各段階で 0 <= next < entry を満たす必要があります。整数タプルによる辞書式の減少も使えます。呼び出し先も停止する必要があります。

ループの停止性を検証する

ループの直前に invariant と decreases を置きます。不変条件は開始時と各反復後に成立し、尺度はループに戻るたびに非負のまま厳密に減る必要があります。

from typing import Annotated
from refinepy import Refine, invariant, decreases

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

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

入れ子のループにも、それぞれ尺度が必要です。停止性の証拠がない検証結果は、関数が正常に戻る場合に限って適用します。

関数の等式を証明する

@reflect で検査済みの定義を述語から使えるようにします。補題は戻り値の契約に等式を記述します。

from __future__ import annotations
import refinepy
from refinepy import Refine
from typing import Annotated

@refinepy.reflect
def inc(x: int) -> int:
    return x + 1

def lemma(x: int) -> Annotated[None, Refine(lambda _, x: inc(inc(x)) == x + 2)]:
    return None

lemma を選んで検証します。x + 2 を x + 3 に変えると証明に失敗します。定義を取り込む関数では、事前条件、細分化した型注釈、ループ、コンテナーへの書き込みは使えません。再帰定義と帰納補題の追加の制約はリファレンスを参照してください。

補題を実行せずに使う

前の例に追加します。Assert は束縛済みのローカル変数について、その位置で命題を検査します。using には、独立に停止性を検証した補題を指定します。Python はこのローカル注釈を実行しません。

from typing import Annotated
from refinepy import Assert

def use_lemma(x: int) -> int:
    x: Annotated[int, Assert(
        lambda value: inc(inc(value)) == value + 2,
        using=lambda arg: lemma(arg),
    )]
    return x

using を省くと、現在の事実から命題を証明します。Assert は後の代入を制約しません。値の契約には Refine を使います。束縛の規則はリファレンスを参照してください。

結果を読む

各関数に状態と停止性の要約を表示します。検証の詳細で診断と証拠、JSON レポート全文で完全なレポートを確認できます。

状態	意味
`verified`	必要な証明義務をすべて検証した。
`counterexample`	検証済みの具体的な入力が契約に違反する。
`unproved`	未証明の義務が残る。これだけではソースのバグとはいえない。
`unsupported`	対応範囲外の構文を使っている。
`unknown`	制限やソルバーの不確実性により結論が出なかった。
`error`	ソース、契約、設定、実行でエラーが起きた。診断を確認する。

verified は契約を満たす入力とモデル化した実行環境に適用します。これだけでは停止性を保証せず、Python 実行時に契約を強制しません。再帰深度と資源の制限は保証の対象外です。対応構文はリファレンスを参照してください。

ガイド

関数を検証する