このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。
sldv.prove
Stateflow チャートおよび MATLAB Function ブロックの証明オブジェクティブ関数
説明
この関数はなにも出力しないため、expr
を評価する間接的な副作用があるだけで、親関数には影響を与えません。MATLAB® コマンド ラインからこの関数を実行しても、効果はありません。
コード内に sldv.prove
の証明の前提を組み入れるか、前提を分離して検証スクリプトに組み入れます。
例
入力引数
代替方法
関数 sldv.prove
を使用する代わりに、Proof Objective ブロックをモデルに挿入できます。Proof Objective ブロックの代わりに sldv.prove
を使用すると、プロパティ証明とはで説明されているとおり、いくつかの利点が得られます。
関数 sldv.prove
を使用せずに、MATLAB をコード生成に使用して証明オブジェクティブを指定することもできます。コードの生成に MATLAB を直接使用するのではなく、sldv.prove
を使用すると、次の処理が不要になります。
Simulink ブロックを使用したオブジェクティブの表現。
証明の出力の Simulink ブロックへの明示的な接続。