αRby—An Embedding of Alloy in Ruby
about αRby declarative modeling language embedded in an imperative programming language beneficial to both the modeling community of Alloy and the object-oriented community of Ruby programmers benefits to Alloy users: mixed execution partial instances staged model finding benefits to Ruby users: seamless embedding of a relational constraint solver download & run downloadarby @ github licenseGPLv3
Alloy Analyzer LT
joseph caramagno {lawyer|attorney|legal representative|legal professional|lawyer or attorney|legal counsel}
形式手法勉強会第3回 device tokenの仕様について
形式手法勉強会で使った資料です。 alloyというツールを使っています。 alloy自体の紹介は別の資料で説明しており、 この資料では以下の語を説明無しに使っています ・ドット（結合） ・矢印（積） ・その他各種シグネチャ ・alloyの特徴（全ては関係、全ては論理式、非手続き型言語であることなど） このあたりの理解は原典にあたるのが一番手っ取り早いです http://alloy.mit.edu/alloy/Read less
ボタンの仕様を書いてみよう - Alloy Analyzer で形式仕様記述
まずは簡単な事例で、Alloy で仕様を記述/検査する一通りの流れを説明します。 * 1. 題材 ---- 今回は、単純な「ボタン」の仕様を題材にします。 以下のようなボタンの仕様を考えています。 - ボタン上にカーソルがないときは、ボタンは Normal 状態です。 - マウスカーソルが上に来たら、ボタンは Over 状態になります。 - ボタンが押されたら、ボタンは Press 状態になります。 - ボタンは自身の幅と高さを管理しています。 ボタンは以下のイベントを受け取ります。 これらのイベントはいつでも送られてくる可能性があります。 - mouse_move (x : Int, y : Int) //マウス移動 - mouse_pressL (x : Int, y : Int) //マウス左Press - mouse_releaseL (x : Int, y : Int) //マウ
Kodkod
about kodkod Kodkod is an efficient SAT-based constraint solver for first order logic with relations, transitive closure, and partial models. It provides analyses for both satisfiable and unsatisfiable problems: a finite model finder for the former and a minimal unsatisfiable core extractor for the latter. Recent applications of Kodkod include the Alloy4 analyzer for the Alloy language; the Forge,
Alloy
about alloy Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. An Alloy model is a collection of constraints that describes (implicitly) a set of structures, for example: all the possible security configurations of a web application, or all
Alloy Analyzer のこと
Alloy Analyzer について社内セミナーで発表した資料です。 実際の模様→ http://www.ustream.tv/recorded/17430540Lire moins
Alloyまとめ - 西尾泰和のはてなダイアリー
スライド Alloy Analyzer のこと by @mr_konn Alloyガール Alloyガール1 Alloyガール2 Alloyガール3 Alloyガール4 Alloyガール5 Alloyガール番外編「イラストロジック」 Alloyガール6 Alloyガール完結編 その他 Alloyを勉強する日記(0) Alloyを勉強する日記(1) Alloy本4.2.2 Alloy: 二項関係の性質 Alloyの人間関係をビビッドにするライブラリを作った Alloy日記2: 時系列で変化する状態 Alloyでコンビネータ論理をやろうとしてうまく行かなかった話 Alloy: allの意味がわからない Alloyでコンビネータ論理・続編 Alloy日記3: 結婚と離婚をモデリング イラストロジック Alloyでイラストロジックを解く 解けなかった話 Alloyガール番外編「イラストロジック」
社内セミナーで Alloy Analyzer について発表してきました - これは圏です（はてな使ったら負けだとおもっていた）
PFI の社内セミナーで Alloy Analyzer について発表してきました。 Alloy Analyzer のこと View more presentations from Hiromi Ishii なんか ust でストリーミング放送された上、録画・保存されてしまっているらしいので、観てやろうという酔狂な方は下からご覧になったらいいんじゃないでしょうか。 なんだか台本とか特に考えずに書いたので、早口かつしどろもどろと云うか何か何云ってるのか良くわからない感じになっちゃってますね……反省。 補足 日本語をソースで使うには、4.2RC を使う必要があります。 さて。訳者の一人でいらっしゃる id:bonotake さんやさかいさんから幾つか補足がありましたので紹介します。 発表では「有界モデル検査器」と紹介しましたが、公式には「有界モデル発見器」と呼ぶそうです。 発表では assert
形式手法とモデリング - AlloyAnalyzerを中心に | Think IT（シンクイット）
1. 初めに ソフトウエアの欠陥がもたらす影響がクリティカルになるにつれて、より間違いの少ない開発手法に注目が集まっています。 そんな中で注目されている技術の1つが、形式手法です。形式手法とは、数学をベースにしたシステム開発手法の総称です。 ですが、従来の形式手法は、数学の専門知識が必要だったほか、大がかりなシステム開発体制とあわせて語られることがほとんどでした。このため、一般の開発者にとっては、なじみのない技術でした。 こうした状況が、ここ数年で一変しました。PCの性能向上と、より使いやすいツールの提供により、誰でも簡単に試すことがのできる環境が整いつつあります。 本記事では、形式手法ツールの1つ「Alloy Analyzer」を取り上げ、以下の2つのポイントを中心に解説します。 形式手法は、導入の難しさが解消されてきている 形式手法は、ほかの現行の開発手法を補うかたちで利用できる 1.
Alloy Analyzer で形式仕様記述
仕様を形式的に記述/検査することのできる言語やツールは、VDM, B, Z, Isabelle など他にも色々ありますが、 Alloy はそれらにくらべてより軽いフットワークで記述/検査することができるツールです。 それらのツールと Alloy との比較も、機会があればご紹介したいと思います。 2. Alloy を使った形式仕様記述の特徴 数理論理学＋集合論をベースとした Alloy の言語で仕様を記述します。 書いた仕様を、簡単に検査することができます。 難しい論理式の証明などは必要ありません。 検査結果は図で表示してくれるので、結果を目視で直感的に理解することができます。 仕様で書いた振る舞いをシミュレーションすることができます。 3. このページのスコープ ここでは仕様のうち、概要レベルの仕様や、重要な部分だけを抜き出した仕様といった、抽象度の高い仕様をスコープとしています。 抽象度
Alloy で男の娘を見付けよう - これは圏です（はてな使ったら負けだとおもっていた）
問題 どこかの国の非実在学園での話と思ってちょーだい。 この学園には四種類の人間が通っているそうです。男の子、女の子、男の娘、男装の麗人だそうで。自由な校風なんですね。 自由なのは結構なんですが、時偶あるのが、かわいい女の子だ！と思ったら実は男の娘でしたと云う悲劇で、人によっては美味しいシチュエーションなんでしょうが、少なくともぼくは女の子のほうがいいです。野郎は野郎なので……。ただ、学ラン着てる女の子とか倒錯してていいかんじだなあ、と思うので、男装の麗人はうぇるかむですね！わいわい。 と云う訳で、何とかして性別を判定したいんですが、はて……。 ところで、いかに自由な校風と云えど、一つだけ校則があるそうです。曰く、「嘘吐きは須く嘘を吐き、正直者はみな真実のみを喋るべし」。この法則は受け答えだけでなく、日常の所作や言動にも適用されるそうで、従って男の子や女の子は常に真実を、男の娘や男装の麗人
Alloy 勉強中 - 言語ゲーム
最初に Alloy の事を知ったのは http://d.hatena.ne.jp/keigoi/20090210/p1 を読んで、面白そうだと思った。でも、http://alloy.mit.edu/ のウェブサイトを見てもどこへ行ったら良いのか分からなくて、意味不明すぎて放置していた。しばらくして、同僚が研究で Alloy を使っている事が分かった。これは素晴らしい。というのも、前から私は Coq とか、CafeOBJ とか、論理っぽい事に興味があったんだけど、周りにこういう事を話せる友達がいなかったので寂しい思いをしていたからだ。正直 Alloy の妙にオブジェクト指向風の文法に馴染めなかったけど、同僚に Coq を勧めるより自分で Alloy を勉強する方がはやいと思ってチュートリアルをやる事にした。←いまここ。 ようやく分かった事。Coq と Alloy は一階述語論理を使っていると
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
TestEra: A Tool for Testing Java Programs Using Alloy Specifications
Alloy*: A Higher-Order Relational Constraint Solver
ISO 26262 - Tool Chain Analysis Reduces Tool Qualification Costs
Departamento de Computaci�n
Google Code Archive - Long-term storage for Google Code Project Hosting.
Alloy による Git のコミットグラフのモデリング
AndroidのNFC機能でFeliCaの読み書きをする | −ゆめログ− | ゆめみスタッフブログ