PROMELAで記述したモデルから検証器を生成する際にnever claimが2つ以上になると、どれか一つを選択して欲しい旨と-searchオプションを指定する例が出力されます。本などには以下の流れで記載されていますが、何か違いがあったりするのでしょうか。 検証器の…

この文章について このページでは Coqで「Require Import Cpdt.CpdtTactics.」を実行した際に出力されたエラー「Error:Cannot find a physical path bound to logical path matching suffix Cpdt.」を解消する方法について紹介したいと思います。私がCoqの勉…

階乗を計算する関数 和に引き続き積についても同じように関数を定義したいと思います。まずは、階乗を求める関数から定義してみます。ソースは前回からの続きとなっています。 factorial01.c #include "util.h" int factorial(int n) { int acc = 1; int i; …

関数ポインタとは 関数ポインタとは関数を指すポインタのことです。私がC言語を学び始めた頃はポインタについてよく理解していないこともあり、関数ポインタが何の役に立つのかわかりませんでした。 そんな中、関数ポインタを理解するきっかけになったのは、…

プログラミング関する情報を色々書いていきたいと思います。 まずは、別のサイト向けに作成していた内容などを修正しつつ記事にしていこうと考えています。