コマンドキューをもつシステムのAlloyモデル - masateruk’s blog
とあることがきっかけで、コマンドキューをもつシステムをAlloyでモデル化し検証したので、ここで紹介します。 問題 あるシステムのミドルウェアを修正することになりました。このミドルウェアは整数値をやり取りするオブジェクトを複数所有します。インタフェースは以下の通りです。 assign(v) // オブジェクトの値をvに上書きします。 copy(obj) // オブジェクトobjの値をコピーします。 getValue() // オブジェクトの値を取得します。 このミドルウェアを実装するためにライブラリを使用しています。このライブラリはオブジェクトを複数所有しています。各オブジェクトはキューを持ち、コマンドをキューに積んでから実行する必要があります。コマンドは2種類あります。 assign(v)コマンドは、値の上書きする。 copy(obj)コマンドは、オブジェクトobjの値をコピー
レイトン教授で始める�Alloy Analyzer入門 - osiire’s blog
8月15日にギークバーで使った資料をアップします。 レイトン教授で始める�Alloy Analyzer入門 View more presentations from osiire 資料に出てくる３つの問題のAlloyによるチートコードは次の通りです。さぁ、あなたもAlloyでレイトン教授の攻略を始めよう！ //No50 enum Cow { A, B, C, D, E } sig Liar in Cow {} { #Liar = 3 } // ソーウ種は３匹 pred whoIsLiar { not A in Liar iff D in Liar not B in Liar iff C in Liar not C in Liar iff not A in Liar not D in Liar iff E in Liar not E in Liar iff B in Liar } run w
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
形式手法とモデリング - AlloyAnalyzerを中心に | Think IT（シンクイット）
1. 初めに ソフトウエアの欠陥がもたらす影響がクリティカルになるにつれて、より間違いの少ない開発手法に注目が集まっています。 そんな中で注目されている技術の1つが、形式手法です。形式手法とは、数学をベースにしたシステム開発手法の総称です。 ですが、従来の形式手法は、数学の専門知識が必要だったほか、大がかりなシステム開発体制とあわせて語られることがほとんどでした。このため、一般の開発者にとっては、なじみのない技術でした。 こうした状況が、ここ数年で一変しました。PCの性能向上と、より使いやすいツールの提供により、誰でも簡単に試すことがのできる環境が整いつつあります。 本記事では、形式手法ツールの1つ「Alloy Analyzer」を取り上げ、以下の2つのポイントを中心に解説します。 形式手法は、導入の難しさが解消されてきている 形式手法は、ほかの現行の開発手法を補うかたちで利用できる 1.
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
