ソフトウェア開発において、これから開発するシステムの仕様を作成したとき、その仕様を元に作成されるプログラムはプログラマが作る部分と、既存のライブラリを使用する部分が存在する。したがって、プログラムが仕様に適合しているかを検証するためには、使用するライブラリの仕様が必要となってくる。 本論文では、代数的仕様をC言語で実現する場合に、仕様とプログラムの検証を行うための準備としてC言語の標準ライブラリの代数的仕様の作成法について述べる。また、ポインタのように代数的表現の難しいものの扱いについても述べる。仕様には、対象となるデータの型や関数の集合を示す指標と演算の規則を示す等式の集合との対である等式仕様を用いる。