Goのコードを数学的に証明する

Goのコードを数学的に証明する

Dennis Metzger

2026-02-18

golang.tokyo #43

Dennis(デニス) Metzger(メッツガー)

Backend Engineer @ Finatext

数学的に証明する？

自動推論の

素晴らしい世界

へようこそ

早くコード見せろ

assert

「この行に到達した時点で、

次の条件が正しいことを証明せよ」

func Double(n int) (res int) {
                    	res = 2 * n
                    	// @ assert res > n
                    	return
                    }


Gobra 1.1-SNAPSHOT (@)
(c) Copyright ETH Zurich 2012 - 2024
INFO viper.gobra.Gobra - Verifying package  - main
ERROR viper.gobra.reporting.FileWriterReporter -
    Error at: <main.go:7:2> Assert might fail.
Assertion res > n might not hold.
ERROR viper.gobra.Gobra - Gobra found 1 error.

ensures

「この関数の返却値が、

次の条件を満たしていることを証明せよ」

// @ ensures res >= 0 && (res == x || res == -x)
func Abs(x int) (res int) {
	if x < 0 {
		return -x
	} else {
		return x
	}
}

type Formatter interface {
	// @ ensures len(s) > 0
	Format() (s string)
}

var _ Formatter = a{}

type a struct{}

func (a) Format() (s string) {
	return "a"
}

type Formatter interface {
	// @ ensures len(s) > 0
	Format() (s string)
}

var _ Formatter = a{}

type a struct{}

func (a) Format() (s string) { 未設定
	return "a"
}

type Formatter interface {
	// @ ensures len(s) > 0
	Format() (s string)
}

var _ Formatter = a{}

type a struct{}

// @ ensures len(s) >= 0
func (a) Format() (s string) {
	return "a"
}

type Formatter interface {
	// @ ensures len(s) > 0
	Format() (s string)
}

var _ Formatter = a{}

type a struct{}

// @ ensures len(s) >= 0　満たしていない
func (a) Format() (s string) {
	return "a"
}

type Formatter interface {
	// @ ensures len(s) > 0
	Format() (s string)
}

var _ Formatter = a{}

type a struct{}

// @ ensures len(s) == 1　満たしている
func (a) Format() (s string) {
	return "a"
}

requires

「この関数が呼び出される際に引数が

次の条件を満たさなければならない」

// @ requires b != 0
func Div(a, b int) int {
	return a / b
}

func _() {
	_ = Div(10, 2)
	_ = Div(10, 0)
}

// @ requires b != 0
func Div(a, b int) int {
	return a / b
}

func _() {
	_ = Div(10, 2)　OK
	_ = Div(10, 0)　満たしていない
}

invariant

「ループの実行中に、

次の条件が常に正しいことを証明せよ」

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

assertじゃダメなんでしょうか？

ソルバーはコードを
実行しているわけではない

ループが何回実行されるかはわからない
数学的帰納法に似た方法で証明せざるを得ない

数学的帰納法？？

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant 0 >= 0 && 0 <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant 0 >= 0 && 0 <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant 0 >= 0 && 0 <= b → true
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant 0 >= 0 && 0 <= b → true
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant 0 >= 0 && 0 <= b → true
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant 0 >= 0 && 0 <= b → true
	// @ invariant 0 == a * 0
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 1: 初回のループを証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant 0 >= 0 && 0 <= b → true
	// @ invariant 0 == a * 0 → true
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b trueとする
	// @ invariant result == a * i  trueとする
	for i < b {                     trueとする
		result = result + a
		i = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b trueとする
	// @ invariant result == a * i  trueとする
	for i < b {                     trueとする
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b
	// @ invariant result_new == a * i_new
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b
	// @ invariant result_new == a * i_new
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b
	// @ invariant result_new == a * i_new
	for i < b {
		result_new = result + a
		i_new = i + 1         → i + 1 >= 0
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b
	// @ invariant result_new == a * i_new
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b
	// @ invariant result_new == a * i_new
	for i < b {             → i + 1 <= b
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b → true
	// @ invariant result_new == a * i_new
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b → true
	// @ invariant result_new == a * i_new
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b → true
	// @ invariant result + a == a * (i + 1)
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b trueとする
	// @ invariant result == a * i  trueとする
	for i < b {                     trueとする
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b → true
	// @ invariant result + a == a * (i + 1)
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b → true
	// @ invariant (a * i) + a == a * (i + 1)
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 2: 帰納

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i_new >= 0 && i_new <= b → true
	// @ invariant a * i + a == a * i + a → true
	for i < b {
		result_new = result + a
		i_new = i + 1
	}
	return result
}

Step 3: ループ終了後の証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 3: ループ終了後の証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i < b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 3: ループ終了後の証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for !(i < b) {
		result = result + a
		i = i + 1
	}
	return result
}

Step 3: ループ終了後の証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i >= b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 3: ループ終了後の証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i >= b {
		result = result + a
		i = i + 1
	}
	return result
}

Step 3: ループ終了後の証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i >= b {
		result = result + a
		i = i + 1
	}
	→ i == b
	return result
}

Step 3: ループ終了後の証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i >= b {
		result = result + a
		i = i + 1
	}
	→ i == b
	return result
}

Step 3: ループ終了後の証明

// @ requires a >= 0 && b > 0
func Mul(a, b int) int {
	result := 0
	i := 0
	// @ invariant i >= 0 && i <= b
	// @ invariant result == a * i
	for i >= b {
		result = result + a
		i = i + 1
	}
	→ i == b
	→ result == a * b
	return result
}

⋯⋯という証明を
Gobraが自動でやってくれている

trusted

「関数を証明済みと見なす」

// @ ensures res == 2
// @ trusted
func One() (res int) {
	return 1
}

ご清聴ありがとうございました！

Dennis Metzger

2026-02-18

golang.tokyo #43

Dennis(デニス) Metzger(メッツガー)

ソルバーはコードを実行しているわけではない

ソルバーはコードを
実行しているわけではない