Go to Qiita Advent Calendar Top
LoginSignup
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

Day 19

42Tokyo Advent Calendar 2025

@yuotsuka

C11のプログラムに形式仕様を書いてみる。 CNを触ってみた記録。

Last updated at Posted at 2025-12-18

本記事は 42tokyo のアドベントカレンダー シリーズ2 19日目の記事です。

42tokyoに在籍しているyuotsukaです。
まず本記事を書くにあたっての動機を書こうと思います。動機には興味ないよという方は次節の導入まで飛ばしてください。

モチベーション

42tokyo のカリキュラムの学習の延長線として、個人的に強く関心があり学習を進めている分野にソフトウェア検証があります。

42 のカリキュラムではシステムプログラミングやグラフィック描画についての課題を C 言語で記述していきますが、学習目的のプロジェクトでは書き捨てのようなプログラムが出来上がりがちで、コードの品質には（学ぶ途中として当然かもしれませんが）あまり意識が向かないことも多いです。

一方で、学びが一段落して実装の方針が固まってきたときや、作業途中のコードベースから一度手を離したいときには、「変更してよいもの／いけないもの」や「何を満たすべきだったか」という手がかりが欲しくなります。作成者自身であっても、時間が空けば機能的な前提や意図を部分的に忘れる可能性があるためです。

手がかりとして、型やテストによって「満たしたい条件」を記述しておく、という考え方があります。しかし 42 の基礎カリキュラムで扱うことの多い言語（C / C++ / Python など）では、言語内の型だけでプログラムが満たすべき要求を十分に表現・保証できないケースが多々ありますし、テストも自動化するのは一苦労です（型について、現代的なコンパイラのオプションで補える部分はありますが限界があります）。

そこで、既存の言語処理系に対して外部の型検査器を導入する、というアプローチが知られています。このような言語から見て外部となる型検査を導入する方法を外因的（extrinsic）な方法と呼ぶことにします。

導入

本記事では、外因的な型検査器のひとつとして、C のコードに事前条件・事後条件を記述し、C11 の形式化意味論(Cerberus)と分離論理(Wikipedia)に基づいて検証を行うツール CN を紹介します。CN は Cerberus による C11 意味論の形式化を背景に持ち、仕様から生成される条件を Z3（SMT ソルバ）で自動的に解くことで、ポインタ操作や参照・配列アクセスの安全性まで含めて検査できます。

また補足として、ここで言う「事前条件・事後条件」を手続き（if / else / for / while など）と対応づけて形式的に扱う枠組みとして ホーア論理(Wikipedia)があります。分離論理は、ホーア論理を拡張してポインタや参照（ヒープ上の領域）についての意味を論理的な規則からより直接的に扱えるようにしたもの、と大雑把には捉えられます。

（類似するツールとして RefinedC もあり、こちらも後々比較してみたいです。）

CNについて

　CNは、C11の意味論を Cerberus というプロジェクトで定理証明支援系 Rocq 上に形式化した成果を基盤とするツールです。
C11仕様が定めるルールに基づき、CNのアノテーションを用いて記述されたプログラムについて、CNの記述の範囲でアノテートされた事前条件・事後条件の仕様をCプログラムが満たしているかを検証します。
あわせて、その検証過程において探索できる範囲でC11の仕様違反（未定義動作、未規定動作など）に触れる可能性のある箇所を検出します。
CNの特色の一つとして導入でも軽く言及しましたが、そのプログラムがポインタや参照のような事前/事後条件を書き換えてしまうような可能性のある言語機能についても追跡できる推論規則を持っています（分離論理に基づく）。
その際に、CNで書かれた仕様の条件について、Cerberusの意味論と照らし合わせて大量の条件式を自動的に解決する必要があるため、CNの内部ではZ3というSMTソルバーを利用します。（SMTソルバーは、概要について端的にいうと何重にもなる条件の構造がすべて真になるか、そうでないかをソルバ内部の標準形に落として判定するため計算するソルバになります。）

CNのリソースやチュートリアル

機能紹介にはWIPな部分も多く含まれていますが、CNにはチュートリアルページがあります。
先に紹介しておきます。(筆者はこのあたりを参考に学習中なので、皆さんもこの辺をさわってみてください。)

CNの使い方

上記リンクのインストール手順に従いながら進みます。CNは仕様の探索時のソルバとしてZ3を要求するので、Z3がすぐに利用できない環境（システムパッケージマネージャやその他の管理ツールで実験的にすぐ導入できない場合など）ではZ3のソースを落としてきてビルドできるならばビルドしましょう。

サブコマンドについて

CNには、事前・事後条件の検証を行う verify 以外にも、テスト生成や実行を行うサブコマンドが用意されています。
ここでは、CNのチュートリアルから引用した基本的な関数群と、Cのバブルソートの実装を用いて試した事項について紹介します。

1. cn verify

CNのメイン機能です。記述された仕様（事前条件・事後条件・不変条件）に基づいて、プログラムがあらゆる入力に対して正しいことをCerberusに照らしあわせて証明します。

  • 実行例: cn verify snippets/case2.c
  • 結果:
    • 証明に成功すると pass と表示されます。
    • 失敗すると、反例となるパスやリソース不足のエラーが表示されます。
    • バブルソートの例では、ループ変数のリソース管理を修正することで pass しました。

2. cn test

Fulminate と呼ばれるコンポーネントを使用し、CNの仕様に基づいてテストケースを自動生成して実行します。
形式検証 (verify) が「すべての入力」を保証するのに対し、test は具体的な入力でスタブテストを行います。形式仕様をちゃんと書くと仕様を書くことが重たくなりがちなので、検証が難しい場合のデバッグや、部分的な仕様の妥当性を確認するのに便利です。

テストレポートの出力様式としては以下のようになります

/tmp/bennet.C975
Testing case1::min3: 100 runs
PASSED
Testing case1::read: 100 runs
PASSED
Testing case1::incr: 100 runs
PASSED
Testing case1::inplace_double: 100 runs
PASSED
Testing case1::read_spec_broken:
FAILED

************************ Failed at *************************
no source location found (try running with --exec-c-locs-mode enabled)********************** Failing input ***********************

void* p0 = malloc(4);
*((unsigned int*)p0) = 4294967295;
unsigned int* p = (unsigned int*)(p0);
read_spec_broken(p);

************************************************************

テストケース生成にかかわるサブコマンドとしてcn seq-testというものがあり、具体例として面白そうな紹介が思いつかなかったのですが、Cソースが2つ自動的に用意(ソース名.exec.c, ソース名.test.c)されCNの意味論を基にモックテストされるみたいです。

CNの文法とケーススタディ

本記事ではCNの紹介のついでに、いくつかのコード例を通じて文法と検証の流れを紹介します。

コード例1: 基本的な関数

まずは、CNのチュートリアルにもあるベーシックな関数の仕様記述例です。(出典: https://rems-project.github.io/cn-tutorial/getting-started/tutorials/first-taste/)

純粋な関数: min3

ポインタを扱わない純粋な関数の仕様は、外部での書き換え状態などを意識せずに比較的直感的に記述できます。

unsigned int	min3(unsigned int x, unsigned int y, unsigned int z)
/*@ ensures return <= x
			&& return <= y
			&& return <= z;
@*/
{
	if (x <= y && x <= z)
		return (x);
	else if (y <= x && y <= z)
		return (y);
	else
		return (z);
}
  • ensures: 関数の戻り値（return）が満たすべき条件を記述します。ここでは、戻り値が引数 x, y, z のいずれよりも小さいか等しいこと（最小値であること）を保証しています

こういう単純なヘルパを書いたら仕様を書いていく癖をつけていきたいです。

ポインタ操作: incr

ポインタを扱う場合、リソースの概念が登場します。

void incr (unsigned int *p)
/*@ requires take P = RW<unsigned int>(p);
    ensures take P_post = RW<unsigned int>(p);
            P_post == P + 1u32;
@*/
{
  unsigned int n = *p;
  unsigned int m = n+1;
  *p = m;
}
  • requires take P = ...: 関数呼び出し時に、ポインタ p への読み書き権限（RW）を受け取ります。その時点での値を P という論理変数にバインドします
  • ensures take P_post = ...: 関数終了時に、ポインタ p への権限を返却します。その時点での値を P_post とします
  • P_post == P + 1u32: 終了時の値が、開始時の値 P に 32bit unsigned int型の 1 を足したものになっていることを保証します

コード例2: Bubble Sort

次に、少し複雑な例として、C言語のバブルソートアルゴリズムにおいて、配列の参照についての安全性（i, jのインデックスの配列外参照がないこと）を検証する例を紹介します。

以下は、CNのアノテーションを付与し、配列のアクセス範囲と終了ステータスを形式仕様で記述し、検証に成功したCのバブルソートアルゴリズムのコードです。(本当はadventなのでもっと賢いソートアルゴリズムの検証をしたかったのですが、惰性で一番poorなソートアルゴリズムの検証(しかもソート対象の配列の中身のソート結果には触れていない)になってしまいました。)

void swap(unsigned int *p, unsigned int *q)
/*@
  requires
    take Pv = RW<unsigned int>(p);
    take Qv = RW<unsigned int>(q);
  ensures
    take Pv_ = RW<unsigned int>(p);
    take Qv_ = RW<unsigned int>(q);
    Pv_ == Qv;
    Qv_ == Pv;
@*/
{
  unsigned int tmp = *p;
  *p = *q;
  *q = tmp;
}

int bubble_sort(unsigned int *arr, unsigned int size)
/*@
  requires
    take A = each (u64 k; 0u64 <= k && k < (u64)size)
      { RW<unsigned int>(array_shift<unsigned int>(arr, k)) };
  ensures
    take A_post = each (u64 k; 0u64 <= k && k < (u64)size)
      { RW<unsigned int>(array_shift<unsigned int>(arr, k)) };
    return == 0i32;
 @*/
{
  if (size == 0u) return 0;


  unsigned int i = 0u;
  for (; i < size - 1u; i++)
  /*@
    inv
      take Ai = each (u64 k; 0u64 <= k && k < (u64)size)
        { RW<unsigned int>(array_shift<unsigned int>(arr, k)) };
      {arr} unchanged;
      {size} unchanged;

      (u64)i < (u64)size;
  @*/
  {
    unsigned int j = 0u;
    while (j < size - 1u - i)
    /*@
      inv
        take Aj = each (u64 k; 0u64 <= k && k < (u64)size)
          { RW<unsigned int>(array_shift<unsigned int>(arr, k)) };
        {arr} unchanged;
        {size} unchanged;
        (u64)j < (u64)size;
        (u64)j + (u64)i + 1u64 <= (u64)size;
        (u64)i + 1u64 < (u64)size;
    @*/
    {
      /*@ assert (j < size); @*/
      /*@ assert (j + 1u32 < size); @*/
      /*@ focus RW<unsigned int>, (u64)j; @*/
      /*@ focus RW<unsigned int>, (u64)j + 1u64; @*/
      if (arr[j] > arr[j + 1u]) {
        swap(&arr[j], &arr[j + 1u]);
      }
      j++;
    }
  }
  return 0;
}

cn verify

[1/2]: swap -- pass
[2/2]: bubble_sort -- pass

cn test

Testing case2::swap: 100 runs
PASSED
Testing case2::bubble_sort: 100 runs
PASSED

Testing Summary:
cases: 2, passed: 2, failed: 0, errored: 0, skipped: 0

Bubble sort内のCNのアノテーション

このコードで使われている主なCNの構文について解説します。

  • /*@ ... @*/:
    CNのアノテーションは、C言語のコメントとして記述します。既存のCコンパイラからはただのコメントとして無視されるため、コードのポータビリティをほぼ損ないません。(ただコメントの文法がC11にベースなので、古い規格を指定したCか準拠が甘い実装ではコメント部分をコンパイル時に互換する形へ差し替える等しないとコンパイルできないかもしれません。)

  • requires / ensures:
    関数の事前条件（Pre-condition）と事後条件（Post-condition）を定義します

    • take A = ...: take はリソース（メモリの所有権など）を取得することを意味します。CNは分離論理（Separation Logic）に基づいており、ポインタへのアクセスには所有権を条件として明示する必要があります
    • RW<unsigned int>(ptr): ptr が指すメモリ領域に対して、読み書き（Read/Write）の権限があることを示します
    • each (u64 k; ...): 配列全体のような、反復的なリソースを記述します。ここでは arr の 0 から size-1 までの各要素へのアクセス権をまとめて定義しています
    • array_shift<T>(ptr, k): ポインタ ptr から k 個分（型 T のサイズ単位で）ずらした位置のアドレスを計算するCNの組み込み述語です。C言語の ptr + k に相当します

  • inv (Loop Invariant):
    ループ不変条件です。ループの各反復の開始時に常に成り立つ条件を記述します。ループ内の検証には必須です

    • {arr} unchanged: フレーム条件（Framing condition）と呼ばれ、arr ポインタ自体がループ内で変更されないことを明示します

  • assert:
    その地点で必ず真であるべき条件を記述します。C言語の assert マクロと似ていますが、CNの assert は実行時でなく検証時に証明されます。証明のステップを細かく刻むことで、検証器（SMTソルバ）の助けになったり、検証エラーの原因特定に役立ちます

  • focus:
    each で定義された配列全体のリソースから、特定のインデックス（j や j+1）のリソースを一時的に「フォーカス」して取り出します。これにより、arr[j] のような個別の要素へのアクセスが可能になります

検証のポイントと苦労した点

この検証を通すにあたって、特に以下の躓いたポイントがありました。

配列要素へのアクセス (focus):
CNでは、each で配列全体のリソースを持っていても、そのままでは個々の要素 arr[j] にアクセスできません。focus コマンドを使って、必要なインデックスのリソースを明示的に切り出す必要がありました

現在は配列のサイズに対するインデックスのアクセスが収まるかの検証まで完了しています。ソートが正しく行われているか（ソートアルゴリズム機能的正当性）の検証は、さらに別途仕様記述と検証が必要になります。今回は入力の配列の情報がソースコードから与えられないので、入力のより具体的な例(Cコード)とその仕様が用意できれば、機能的正当性の検証に進めると思います。

終わりに

2026年はこの辺りの仕様記述言語とかフレームワークを触りつつ(あと導入でちょこっと触れたRefinedCについても)、Cerberusに接続するためのRocq(Software Foundations完走したい)とか、界隈で流行っているLeanについてキャッチアップしていきたい気持ちがあります（達成できるかはさておき、表明しておくことで意識を...ね...）
この辺さわっていてふつふつと思っているのですが、ドナルド・クヌースが提唱した文芸的プログラミングの一環として仕様記述して検証するの事が当たり前ような世界が来たりとか、自然言語の翻訳まわりは翻訳先の言語が十分に学習されていればLLMのようなTransformerで形式仕様と自然言語を結びつけることができるという話があるので検証系が発達していけば、保証の弱い処理系でも現代的に実用的なユーザビリティが獲得できるかもとか、色々と想像できて夢がありますね。

最後に、これは完全に42tokyoの在校生にむけての宣伝文句なのですが、CNのアノテーション方法は42norminetteのlinterもたまたまパスするようになっています。コメントに何を記述するかは42 normに言及があると思いますが、何はともあれ興味ある人はぜひこういう道具を通して学習してみましょう。(そんで教えてください)

本記事は以上となります。ここまで記事をお読みいただき、ありがとうございました。

1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?