部分関数の置き換えを認めると矛盾が発生する 部分関数の例はこれ (defun partial (x) (if (partial x) 'nil 't)) こうじゃないのはなぜか (defun partial (x) (partial x)) いちおう値を返しそうな雰囲気はかもし出しておきたい、くらいかな であれば、こうじゃないのはなぜか (defun partial (x) (if (partial x) 't 'nil)) 評価してみて返ってくるかどうかで部分関数かどうかを判定するっていう意味合い？ いやちょっと無理があるか さてpartialは部分関数なのでこういうの書いても'tになることはないでしょうから 証明なしで定義する必要があります (J-Bob/prove (my/prelude) '(((defun partial (x) (if (partial x) 'nil 't))
プログラムの正しさは証明できる。定理証明へ踏み出すための最高のガイドブック Daniel P. Friedman, Carl Eastlund 著、中野圭介 監訳 240ページ A5判 ISBN：978-4-908686-02-3 2017年10月23日 第1版第1刷 発売 あるプログラムが、考えられるあらゆる入力に対して誤った動作を引き起さないことは、テストを書いても確かめられません。それを確かめるには、公理と式の等価な書き換えだけで恒真を導いたり、再帰的なプログラムの構造に照した帰納法による証明が必要です。 なんだか難しそうに聞こえるかもしれませんが、その世界観を丁寧にときほぐして解説したのが、本書の原書にあたる "The Little Prover" です。
All slide content and descriptions are owned by their creators.
AWSがFormal Methodsを使っているというので、見てみる。分散アルゴリズムの検証に、形式手法が有効だったという話である。調べてみると、ACMの記事になる4年も前から、発表されていたらしい。 論文によると How Amazon Web Services Uses Formal Methods | April 2015 | Communications of the ACM AWSでは、2011年からFormal Methodsを使って、重要な分散システムのアルゴリズム設計を行っている。また、外部公開I/Fを単純化して提供することで、大規模な分散システムでサービスを提供できる秘訣となっている。AWSでは、顧客のデータを保護するために、フォールトトレラントな分散アルゴリズムを使っている。また、分散アルゴリズムはたくさんあるが、それらを組み合わせるのは難しい。 TLA+は、プログラマが
LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour. A system in LTSA is modelled as a set of interacting finite state machines. The properties required of the system are
1.はじめに 私は主に組み込み分野における開発に携わってきました。近年、組み込み分野では、品質に対する要求はどんどん厳しくなっています。現在、品質向上のための様々なアプローチが行われています。今回は、人間にわかりやすいモデルを、抜け漏れなく検証するという観点で、UMLとモデル検証の組み合わせの可能性を探ってみました。 本記事では、UMLの状態マシン図で記載したモデルに、モデル検証ツールspinを適用していきます。 spinとは、ベル研究所で開発されたオープンソースのモデル検証ツールです。検証対象のモデルの取りうる全ての状態において、検証条件を満たしているか確認することができます。また、複数のタスクで動作するシステムにおけるデッドロックの発生なども検出することができます。デッドロックの検出例は、書籍やWebサイトでも多く紹介されています。 組み込みシステムにおいては、現在でもRTOS（リアル
The information in the patterns can be presented in a variety of ways. One organization, illustrated below, is based on classifying the patterns in terms of the kinds of system behaviors they describe. Occurrence Patterns talk about the occurrence of a given event/state during system execution. Order Patterns talk about relative order in which multiple events/states occur during system execution.
IoT（モノのインターネット）市場が拡大する中で、エッジ側の機器制御で重要な役割を果たすことが期待されているリアルタイムOS（RTOS）について解説する本連載。第50回は、イタリア発のRTOS「BeRTOS」を紹介する。
UtbildningForskningSamarbeta med ossOm ChalmersAktuelltInstitutioner InstitutionenData- och informationsteknikVi bedriver forskning och utbildning inom AI, cybersäkerhet, interaktionsdesign, software engineering, computing science och datateknik - från grundforskning till direkta tillämpningar. Vi utbildar för framtiden och bedriver forskning nära näringslivet, organisationer och akademin för att
PVS is a mechanized environment for formal specification and verification. PVS consists of a specification language, a large number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples
形式的手法の発祥の地，欧州では 「同手法についてよくある誤解」とのテーマが学会などで語られる。 一方，日本ではその存在すらほとんど認知されておらず よくある誤解などが発生する以前の状態だ。 こうした中，国内でも先駆的に形式的手法を活用し成果を上げた企業がある。 研究者の興味の対象でしかなかった形式的手法が，いよいよ日本でも現場に広がり始めた。 仕様記述と形式検証（モデル検査）。 形式的手法を構成するぞれぞれの分野での最新事例を紹介する。 形式的手法は，主に2つに大別される。1つは，ソフトウエアの仕様を「形式的な仕様記述言語」を使って論理的に記述したり，検査したりすることで，少しでも早い段階でバグを洗い出す「仕様記述」。もう1つは，形式的な仕様記述言語とは別の専用言語で記述したシステムの状態遷移をコンピュータに入力することで，振る舞いにバグがないかどうかを高速かつ自動的に探索する「形式検証（
This is the The wiki about formal methods set up by Jonathan Bowen that anyone can edit. See announcement. Tip: If you register with this website you will receive less advertisements. 133 articles since February 2009 Helping out Not sure where to start? Find out more about the wiki on the About page. If you are new to wikis, check out the tutorial, and see Help:Contents. Check out Help:Starting th
Spécialiste en systèmes sécuritaires Specialist in safety critical systems CLEARSY a été fondée le 1er Janvier 2001 par l’équipe d’ingénieurs auteurs de l’industrialisation de l’outil de modélisation formelle nommé Atelier B, utilisé dans le secteur du ferroviaire pour réaliser les logiciels de sécurité. CLEARSY, INGENIERIE DE SYSTEMES SECURITAIRESNous sommes une PME française, spécialisée dans la
「Coqで定理を記述してみる、型クラスとか使って」に次のような断り書きを入れました。 ミート半束のような代数構造をどう定義するのが良いのか、あんまり分かってないのですが、まーまー使える方法を紹介します。この方法には課題があることを注意しておきます。今回の目的ではうまくいきますが、より大規模な記述にはもっと効率的な方法が必要かも知れません。 代数構造を定義する別な方法である、スピターズ／ファンデル・ウィーゲンの方式をかいつまんで紹介します。 内容： Bundling is bad 追記： 方式の呼び名 オールインワン方式 バンドル方式 アンバンドル方式 何が違うの？ ソースコード Bundling is bad 「Coqで定理を記述してみる、型クラスとか使って」では、ミート半束と（最大元付き）順序集合を定義するために、「マグマのクラス」と「法則（公理系）を書いたクラス」を使いました。スピター
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Amazon.co.jp: ＳＰＩＮ モデル検査: 検証モデリング技法: 中島震: 本
Obsolete URL
