Есть ли способ избавиться от обязательств доказательства альт-эрго, которые создает frama-c?

В настоящее время я играю с frama-c и хочу посмотреть, как frama-c кодирует различные обязательства по доказательству для передачи доказывающему (или помощнику по доказательству). В этом случае alt-ergo.

Мне было интересно, есть ли какой-либо конкретный способ «сбросить» ввод, данный alt-ergo (при условии, что alt-ergo вызывается из frama-c, т.е. не взаимодействует)?

Я хотел бы увидеть, как обязательные свойства C-программ закодированы на «родном» языке ввода alt-ergo. Любая помощь будет принята с благодарностью.


frama-c alt-ergo
person oldjohn1994    schedule 15.11.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Опция -wp-out <dir> позволяет вам выбрать <dir> в качестве каталога, в который будут помещены сгенерированные файлы. Эти файлы отсортированы по подкаталогам в соответствии с используемой моделью памяти (по умолчанию typed). Для Alt-Ergo вы должны найти файлы, заканчивающиеся на .ergo, содержащие только обязательство доказательства, и файлы, заканчивающиеся на _Alt-Ergo.mlw, содержащие полный контекст обязательства доказательства (включая аксиомы, определяющие арифметические модели и модели памяти).

Однако обратите внимание, что в грядущем Frama-C 20.0 Calcium вводится использование API Why3 для связи с проверяющими, и в результате нативные выходы Alt-Ergo (и Coq) постепенно устаревают.

person Virgile    schedule 18.11.2019