Windows10をクリーンインストールし、その後Office2010のWordにて年賀状の宛名印刷をしようとしたところWordの「はがき印刷」がグレーアウトされ、印刷ウィザードが起動できない状態となってハマった。解決方法がわかったのでメモしておく。以下のサイトが参…

形式手法における検証法は2通りある。 仕様を「定理」とみなし、「公理」と「推論規則」を使って証明する方法。 仕様を「モデル」として構築し、要求として与えられる条件を満たす可能性を計算機上で探索する方法。 1つめの方法に用いるツールは「定理証明系…

Who killed Aunt Agatha? Event-Bのハンドブックを読み進めているのだが、アガサパズルというチュートリアルが2.6章にある。 Someone in Dreadsbury Mansion killed Aunt Agatha. Agatha, the butler, and Charles live in Dreadsbury Mansion and are the o…

数学記号をEvent-Bで入力するためのASCII表記一覧表。 記号論理における記号 記号 LaTex 英語 ASCII表記 意味 補足 \top False true 真 \bot True false 偽 \wedge Conjunction & 論理積または連言 (PかつQ) \vee Disjunction or 論理和または選言 (PまたはQ…

Pythonの使い方メモ。csvファイルを読み込んでディクショナリを作成する方法。 以下のような中身のcsvファイル(Month.csv)があり、キーと値がペアで並んでいるとする。 1,january 2,february 3,march 4,april 5,may 6,june 7,july 8,august 9,september 10,o…

2月にEvent-Bを解説した書籍が出ると以前書きましたが、 アマゾンを覗いたら登録されていました。 Event-B: リファインメント・モデリングに基づく形式手法作者: 中島震,來間啓伸出版社/メーカー: 近代科学社発売日: 2015/02/26メディア: ムックこの商品を含…

EclipseベースのRodinという開発環境を使って検証をする定理証明系のツールである。 日本語で詳しい解説があるのは以下のサイトだが、この記事を書いた時点では更新が止まっている。 Event-B - 形式手法 Event-B 形式手法そのものについては以下のサイトに形…

形式手法を理解するためのよい資料を見つけたので自分用にブックマーク。 数理的に組み込みソフトを開発する方法入門 from Toshiyuki Fujikura しかし、リンク先URLを入れるだけでスライドが埋め込みで表示されるなんてすごいな。 Embedded-Note lagavulin19…

Event-Bとは形式手法の１つ。Bメソッドと呼ばれるものがベースになっている。 Event-Bの本が出版 仕事がら形式手法について興味があるのだが、Event-Bは今まで日本語で書籍が出ていない。これはちょっと気になる。 Event-Bについて日本語で比較的まとまった…

うちは賃貸アパートに嫁さんと二人で住んでいるのだが、お風呂が風呂釜がなく、追い炊きできないタイプ。 二人とも共働きで、帰ってくる時間が嫁さんはほぼ定時帰り、自分は遅くなりがち。だが、嫁さんは帰ってきてすぐに風呂に入りたいタイプで帰宅後すぐに…