Цель доказательства функции для диаграмм Stateflow и блоков MATLAB Function
Эта функция не имеет выхода и никакого влияния на ее родительскую функцию, кроме любых косвенных побочных эффектов оценки expr
. Если вы выпускаете эту функцию из MATLAB® командная строка, функция не имеет эффекта.
Интерсперсные sldv.prove
доказательство допущений в коде или разделение допущений на скрипты верификации.
Вместо использования sldv.prove
функция, можно вставить Proof Objective блок в модель. Использование sldv.prove
вместо блока Цель Доказательства предлагает несколько преимуществ, описанных в разделе «Что такое Property Proving?».
Можно также задать цель доказательства при помощи MATLAB для генерации кода без использования sldv.prove
функция. Использование sldv.prove
вместо непосредственного использования MATLAB для генерации кода устраняет необходимость:
Выразите цель при помощи блока Simulink.
Явным образом соедините выход с блоком Simulink.
Proof Assumption | Proof Objective | sldv.condition
| sldv.prove
| sldv.test
| Test Condition | Test Objective