形式手法を使って、 発見しにくいバグを一網打尽にしようbuilderscon tokyo 2019で話したときに使った資料です。 YouTube: https://www.youtube.com/watch?v=D7GccAn6R94 [2020/04/17追記] この資料をさらにブラッシュアップした資料を公開しました。 この資料よりも次の資料をご覧いただくことをおすすめします。 https://www.slideshare.net/dena_tech/dena-techcon-2020-230372486
OAuth2 のフローを Alloy Analyzer でモデリングする - 詩と創作・思索のひろば
趣味でウェブの認証 API を地力で設計しようとしていたときに、認証フローの仕様を頑張ってこしらえたとして、その正しさをどうやって保証するんだろう？ と疑問に思い、調べていたところ、「形式手法」というのに行き当たった。 形式手法というのはシステムの正しさを上流工程から検証するための方法で、数理論理やロジックに基づいている。その中でも厳密な仕様定義を求める方向と自動検証を求める方向とあるらしいが、Alloy はその後者に位置づけられ、軽量形式手法と呼ばれるもののひとつだということらしい。Alloy はモデリングのための言語および実行環境で、以下のホームページから入手できる。 http://alloy.mit.edu/alloy/ インターネット上にチュートリアルやマニュアルもあるが、作者による教科書の邦訳が出ていて、これで勉強してみた。 抽象によるソフトウェア設計−Alloyではじめる形式手
教えて！アロイ人！
Alloyは、論理学の力で限定的に世界を記述し、その記述された世界を満たすような状態があるかどうか、あるとすればどのような状況か、を示してくれる、一種のプログラム的なものです。このような方法で状態や制約無矛盾性を探る手法を、形式手法と呼びます。 プログラム的なものなので、プログラミングをしたことがない人にとっては少し「とっつきにくい」ところがあるかもしれません。 それではプログラマには簡単なのかと言われると、プログラム的であるにもかかわらず、これまでのプログラミング言語とはかけ離れた考え方をしないといけないところもあって、そのへんが普通のプログラマから見ても「とっつきにくい」印象を与えているように思えます。既存の言語では「SQL」が割と近い、と言えば、分かる人には分かってもらえるかもしれません。SQLはすでに存在するテーブル上のレコードに対して条件を満たすレコードを抜き出してきますが、Al
http://alloy.mit.edu/alloy/documentation/alloy4-grammar.txt
Core Alloy4 Syntax (minus some obscure compatibility syntax retained for Alloy3) ================================================================================ Precendence (from LOW to HIGH) 1) let all a:X|F no a:X|F some a:X|F lone a:X|F one a:x|F sum a:x|F 2) || 3) 4) => => else 5) && 6) ! 7) in = < > = !in != !< !> != 8) no X some X lone X one X set X seq X 9) > >>> 10) + - 11) #X 12) ++ 13)
Alloy入門 - Qiita
Alloyとは Alloyとは、「ソフトウェアのモデル化のためのオープンソースの言語およびアナライザ」であり、「セキュリティホールの発見から電話交換ネットワークまで、幅広く応用」される。 Alloy is an open source language and analyzer for software modeling. It has been used in a wide range of applications, from finding holes in security mechanisms to designing telephone switching networks. - Alloy - Website Alloyは、形式手法の困難さを克服するために、ある種の制約を仮定する代わりに表現力と自動検証能力を両立した「軽量形式手法（Lightweight Formal Met
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Alloy論理データモデル
