Невозможно доказать, присвойте положение - FRAMA-C

Question

Я новичок в Фрам-с, и я хотел бы понять, что проблема с этим простым примером:

/*@ requires \valid(array+(0..length-1)) 
@ ensures \forall integer k; 0 <= k < length ==> array[k] == 0; 
@ assigns array[0..length-1]; 
*/ 
void fill(int array[], int length){ 
    /*@ loop invariant 0 <= i <= length; 
    @ loop invariant \forall integer k; 0 <= k < i ==> array[k] == 0; 
    @ loop assigns i, array[0..i-1]; 
    @ loop variant length - i; 
    */ 
    for(int i = 0; i < length; i++){ 
     array[i] = 0; 
    } 
} 

В этом примере Frama-с (WP + Value) не докажет предложение присваивания в контракте функции, и я не могу понять, почему. Любая помощь будет оценена =)

Answer 1

Это может быть доказано (с помощью alt-ergo 0.95.1), если вы ослабляете свои назначения циклов.

@ loop присваивает i, массив [0..length-1];

Предпосылкой i >= 0 также необходима, потому что это не подразумевается \valid(array+(0..length-1). array+(0..length-1) - действительный набор мест с length <= 0, хотя пустой.

Тот факт, что ваш исходный цикл присваивает, не означает, что ваше предварительное условие является ограничением текущей версии WP-плагина.