spark-2014

1зной

1ответ

GNATprove: «postcondition может сбой» в простой функции

Я хочу написать простую функцию, которая находит наибольшее число в заданном массиве Integer. Вот спецификация: package Maximum with SPARK_Mode is type Vector is array(Integer range <>) of Integ