仕様駆動開発とは振る舞いに関する仕様を実装に先立って（ときにAIと共同で）書き、その振る舞い仕様をもとに AI に実装を指示する開発スタイルです。ではそのとき AI とともに作り上げる「振る舞い仕様」はどんな形で書くのがよいのでしょうか。この記事で…

最近は本業の自動テストマンより定理証明支援系に力を入れている Kuniwak です（経緯は過去記事参照）。 orgachem.hatenablog.com 定理証明支援系はいいぞ、ということで本記事では 私がよく使う Isabelle の便利機能の紹介とごく個人的に感じている使い所な…

長らく自動テストとテスト容易設計を生業としてきましたが、最近は色々な限界を感じて形式手法に取り組んでいます。 この記事では、既存の自動テストのどこに限界を感じてなぜ形式手法が必要なのかの私見を説明します。なお、私もまだ完全理解には程遠いため…