Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. Spec# is a research vehicle that has bee
モデル検査の「モデル」とは
論理学とか数学とか計算機科学とか哲学とか。ひたすら個人の見解を述べます。うろ覚えで書いたりするのであまり信用しないでください。間違いの指摘等歓迎いたします。でもきつい言い方はやめてください。 モデル検査の「モデル」とは何かを少し考えてみたい。というか考えるも何もモデル検査の開発者の一人Clarkeの文章を発見したので、それを報告するだけなのだけど。 まず、最近の一般的な理解は、どうもソフトウェアやハードウェアを単純化した「モデル」、ということであるらしい。例えば、Wikipediaには モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。 とある。またPrinciple of Model Checking
PFI の社内セミナーで Alloy Analyzer について発表してきました。 Alloy Analyzer のこと View more presentations from Hiromi Ishii なんか ust でストリーミング放送された上、録画・保存されてしまっているらしいので、観てやろうという酔狂な方は下からご覧になったらいいんじゃないでしょうか。 なんだか台本とか特に考えずに書いたので、早口かつしどろもどろと云うか何か何云ってるのか良くわからない感じになっちゃってますね……反省。 補足 日本語をソースで使うには、4.2RC を使う必要があります。 さて。訳者の一人でいらっしゃる id:bonotake さんやさかいさんから幾つか補足がありましたので紹介します。 発表では「有界モデル検査器」と紹介しましたが、公式には「有界モデル発見器」と呼ぶそうです。 発表では assert
Not your computer? Use a private browsing window to sign in. Learn more about using Guest mode
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
