ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentationソフトウェアの基礎(beta)¶ 本ドキュメントは実験中のものです。 安定板は http://proofcafe.org/sf/ を参照してください。 epub版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.epub mobi版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.mobi Contents:
プログラムに証明が付く日 | RANDMAX
この記事は「Theorem Prover Advent Calendar 2013」6日目の記事です。 http://qiita.com/advent-calendar/2013/theorem_prover 神田「野らぼー」にて、地下の薄暗い店内で… 「そう言えばこないだ隣で起こってたポインタオーバーラン、対応大変そうだったですけどちゃんと家に帰れてたんでしょうかね、新婚なのに…」 「ヌルポとかポインタオーバーランとか、どうして無くならないんだろうね。その時はみんな手を抜いてるつもりなんて毛頭なくて、一生懸命考えて大丈夫だと思ってるはずなんだけどね。レビューもして、それでも起こった後でみんなでソース見てみると、なんで気づかなかったんだよ！ってことになる。」 「人間って、そういうの苦手なんでしょうねきっと。ほら、『何かほかにありませんか』って聞かれても出てこないじゃないですか。静的な解析っ
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
バグのないプログラムを作るための技術 - eomole blog 4 くらい
2015/12/10 追記: バグを本気で無くしたい方はこんな良く辺鄙なブログなんて見ずにソフトウェアエンジニアリング系の国際学会に行くなり、そこの論文を読むなりするといいと思います。ICSEなんかは日本語の勉強会資料もあってとっつきやすいでしょう。 バグのないプログラムを作る方法について色々聞きかじったことを, 脈絡なく訳の分からない説明でつらつらと書きならべます. テスト 割と古典的な方法ですね. プログラミングコンテストでもお馴染みの方式です. Java だと JUnit (4) みたいなのを使います. 手作りケース とりあえず試してみるケース コーナーケース ミスの発生しやすそうなところを突くためのケース ランダムケース ランダムに爆撃するためのケース みたいなものを作って, 仕様とマッチするか確認します. 当たり前ですが, 基本的には下手な鉄砲も数撃ちゃ当たる方式なので, 運が悪
Getting started
The Coq Proof Assistant A Tutorial Version 1 Gérard Huet, Gilles Kahn and Christine Paulin-Mohring LogiCal Project 1This research was partly supported by IST working group “Types” Getting started Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs
Coq for POPL folk
Using Proof Assistants for Programming Language Research or, How to write your next POPL paper in Coq San Francisco, CA January 8th, 2008 A tutorial on the use of the Coq proof assistant in formalizing programming language metatheory. This tutorial will be tailored to people who are familiar with syntactic proofs of programming language metatheory, such as type soundness, but have never used a pro
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ソフトウェアの基礎
Software Foundations 日本語版Wiki