問題タブ [formal-methods]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
modeling - Rodin Platform Event-B プロジェクトで不明な構成 org.animb.valuation.valBase を修正するにはどうすればよいですか?
最新バージョンの Rodin Platform に完全に洗練されたモデルをインポートしました。このプロジェクトでは、ProB アニメーターで IUMLB を使用しようとしています。しかし、プロジェクトには既に構成済みの AnimB アニメーターがあり、最新の Rodin Software ではサポートされていません。エラーには、「不明な構成 org.animb.valuation.valBase」と記載されています。
この AnimB 構成をプロジェクトから削除または修正するにはどうすればよいですか?
c# - Microsoft コード コントラクトを使用した不変のチェック
コード内の事前条件、事後条件、およびオブジェクトの不変条件をチェックするための Microsoft Code コントラクトにさらされました ( https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts ) 試してみたいと思います。健全性と完全性に関して確認したい質問の 1 つは、チェッカーがエラー メッセージを出力しないと仮定した不変条件が与えられた場合、その不変条件が実際に (証明可能な) 真であることを意味するのか、それとも偽陽性である可能性があるのかということです。
formal-languages - Z notation: How to write operation schema that may add one or more tuples to a relation
I'm writing an operation schema in Z. This operation AssignValue maps a property to one or more values.
One property may be linked to one or more values, and one value may be linked to one or more properties, forming a many-to-many relation, R ⊆ Property × Value.
I'm not sure how to write this operation to indicate that one property could be mapped to one or more values. I have two versions here. Version A seems to map one property to only one value.
Version A:
In Version B, I have added a powerset in the declaration of v? to indicate that v? is a set of values (more than one value).
Version B:
Which version is correct? or there is a better way to represent this? I'm new to z-notation, any help would be greatly appreciated. Thanks!
ocaml - K フレームワークが OCaml バックエンドでエラーを生成する
私はK セマンティクス フレームワークを使用しており、チュートリアルを実行しています。これは私の TEST1.k です。
しかし、コマンド Kompile Test1.k を実行すると、次のエラーが発生します。