コマンドキューをもつシステムのAlloyモデル - masateruk’s blog
とあることがきっかけで、コマンドキューをもつシステムをAlloyでモデル化し検証したので、ここで紹介します。 問題 あるシステムのミドルウェアを修正することになりました。このミドルウェアは整数値をやり取りするオブジェクトを複数所有します。インタフェースは以下の通りです。 assign(v) // オブジェクトの値をvに上書きします。 copy(obj) // オブジェクトobjの値をコピーします。 getValue() // オブジェクトの値を取得します。 このミドルウェアを実装するためにライブラリを使用しています。このライブラリはオブジェクトを複数所有しています。各オブジェクトはキューを持ち、コマンドをキューに積んでから実行する必要があります。コマンドは2種類あります。 assign(v)コマンドは、値の上書きする。 copy(obj)コマンドは、オブジェクトobjの値をコピー
Alloy Analyzer のこと
Alloy Analyzer について社内セミナーで発表した資料です。 実際の模様→ http://www.ustream.tv/recorded/17430540Lire moins
形式手法をプログラミング言語に統合せよ | XCrossOver
この記事の所要時間： 約 2分48秒 Haskell界隈なのかどうかはちょっと微妙ですが、一部で形式手法に注目が集まっています。 形式手法自体はBメソッドやVDMなど昔からあるのですが、最近注目されているのは、CoqとAlloyです。 Coqは熱狂的な盛り上がりを見せているようですが、如何せん書物が追いついていないようです。 Alloyは日本語訳された書籍が販売されています。 Amazon.co.jp： 抽象によるソフトウェア設計－Alloyではじめる形式手法－: Daniel Jackson, 中島 震, 今井 健男, 酒井 政裕, 遠藤 侑介, 片岡 欣夫: 本 これを読んでいてふと思ったのが、形式手法は形式手法、プログラムはプログラムと棲み分ける時代はもう終わったのではないか、ということです。 特にCoqでは、証明駆動開発などというものも考えられていて、 Coqによる証明駆動開発
Alloy Community
Welcome to the new Alloy community website! This site is intended as a way for Alloy users to connect and discuss the Alloy modeling language, as well as a place to post papers, software, events or courses related to Alloy. The Alloy Analyzer can be downloaded HERE! If you are a new user to Alloy, please browse the Tutorial and the main Alloy Analyzer web page. If you are a researcher or user of
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
