Описание тега spark-2014

Вопросы с тегом
SPARK 2014 - это язык программирования, унаследованный от Ada. SPARK 2014 был разработан с учетом отсутствия ошибок времени выполнения во время компиляции. Можно писать программы как смесь SPARK 2014 и Ada 2012.
0 ответов

GNATprove: "проверка переполнения может завершиться ошибкой" в функции возведения в степень

Я не могу решить эту проблему с SPARK 2018, думаю, мне нужен какой-то инвариант, чтобы решить проблему переполнения, но я уже все перепробовал и не могу его найти. Если бы кто-то мог пролить свет на мою проблему. Я попробую Экспонирование в простом …
24 окт '18 в 12:59
1 ответ

Испытание Floor_Log2 в Искре

Новичок в Spark и новичок в Ada, поэтому этот вопрос может быть слишком широким. Тем не менее, это спрашивается добросовестно, как часть попытки понять Spark. Помимо прямых ответов на вопросы ниже, я приветствую критику стиля, рабочего процесса и т.…
12 дек '18 в 23:02
2 ответа

SPARK Целочисленная проверка переполнения

У меня есть следующая программа: procedure Main with SPARK_Mode is F : array (0 .. 10) of Integer := (0, 1, others => 0); begin for I in 2 .. F'Last loop F (I) := F (I - 1) + F (I - 2); end loop; end Main; Если я бегу gnatprove, Я получаю следующ…
10 ноя '17 в 17:08
1 ответ

"Утверждение может потерпеть неудачу", и предварительное условие не решает его

У меня есть функция, которая контролирует контролируемый сигнал, применяя простую проверку, находится ли сигнал в заданном диапазоне допуска. Функция называется is_within_limits, У меня есть вторая функция под названием is_within_expanded_limits это…
29 янв '18 в 12:00
1 ответ

Как доказать предусловие Ada/SPARK для функции, встроенной в двойной цикл

Я пытаюсь доказать, что предварительное условие "prepend" выполняется во время выполнения программы ниже. Предварительное условие: Length (Container) < Container.Capacity Мои попытки доказать это приведены в коде ниже в форме прагм. Я могу доказа…
12 ноя '17 в 00:05
1 ответ

Эквивалентность между C/frama-c и Spark-ada

Я изучаю фреймворк Frama-c, и мне интересно, есть ли эквивалентность между C/Frama-c и Spark Ada. Я знаю, что может показаться странным сравнивать такие разные языки, но после прочтения статьи Дэвида А. Уилера, сравнения Йоханнеса Канига и небольшог…
24 май '18 в 13:23
1 ответ

Пост-условие Spark-Ada для итогового массива

Как написать постусловие Spark для функции, которая суммирует элементы массива? (Spark 2014, но если кто-то покажет мне, как это сделать для более ранней версии Spark, я смогу адаптировать ее.) Так что если у меня есть: type Positive_Array is array …
28 июн '17 в 16:51
2 ответа

Создание пакета не на библиотечном уровне в SPARK Ada

Как создать экземпляр не-библиотечного уровня в SPARK Ada? Скажем, у меня есть что-то вроде: subtype Die is Integer range 1..6; package Random_Die is new Ada.Numerics.Discrete_Random(Die); Это дает мне ошибки: instantiation error at a-nudira.ads.45 …
30 июн '17 в 00:42
1 ответ

Выражение для поиска индекса в массиве

Как найти первый символ в строке, который является пробелом, и вернуть его индекс с помощью одного выражения, которое можно использовать как часть Contract_Cases? Например, если строка: Input : constant String := "abc def"; тогда выражение должно ве…
10 ноя '17 в 07:13
1 ответ

Описание типа String в Ada

У меня есть тип, похожий на: type ID is new String (1 .. 7); -- Example: 123-456 Как я могу указать этот формат в коде, либо с Ada или SPARK? Я думал о Static_Predicate, но условие, что строка должна начинаться с 3 положительных целых чисел, за кото…
05 ноя '17 в 15:04
1 ответ

GNATprove: "постусловие может потерпеть неудачу" в простой функции

Я хочу написать простую функцию, которая находит наибольшее число в данном массиве Integer. Вот спецификация: package Maximum with SPARK_Mode is type Vector is array(Integer range <>) of Integer; function Maximum (A : in Vector) return Integer…
22 окт '15 в 20:25
2 ответа

Нуждается в лексическом и грамматическом листе языка программирования ada spark 2014

В случае необходимости лексического и грамматического листа языка программирования Ada spark 2014 каждый может помочь, пожалуйста. заранее спасибо.
29 ноя '18 в 03:08
1 ответ

Как доказать, что предварительное условие процедуры SPARK.Text_IO будет выполнено

Я использую SPARK.Text_IO из примера spark_io в SPARK Discovery 2017. Моя проблема в том, что многие из процедур SPARK.Text_IO имеют предварительное условие, что я не знаю, как начать пытаться доказать именно то, что стандартный ввод читаем, а мы не…
17 ноя '17 в 03:48
1 ответ

Как использовать Assert и loop_invariants

Спецификация: package PolyPack with SPARK_Mode is type Vector is array (Natural range <>) of Integer; function RuleHorner (X: Integer; A : Vector) return Integer with Pre => A'Length > 0 and A'Last < Integer'Last; end PolyPack ; Я хоч…
09 мар '19 в 00:33
2 ответа

Найти множитель числа

Я хочу найти наименьший фактор значения с нижеуказанной спецификацией procedure S_Factor (N : in out Positive; Factor : out Positive) with SPARK_Mode, Pre => N > 1, Post => (Factor > 1) and (N'Old / Factor = N) and (N'Old rem Factor = 0)…
15 мар '19 в 21:39
1 ответ

Постусловие процедуры не подтверждается, даже если в конце процедуры установлено и истинно то же условие.

Код выглядит так: спецификации: type Some_Record_Type is private; procedure Deserialize_Record_Y(Record: in out Some_Record_Type) with Post => ( if Status_OK then ( ... other postconditions ... and then Record_Field_X_Count(Record) = Record_Field…
18 фев '20 в 11:25
2 ответа

Не удалось подтвердить, что результаты libsparkcrypto SHA256 равны

Резюме моей проблемы Я использую библиотеку libsparkcrypto для своей функции SHA256. Я обнаружил, что не могу Assert который x = y подразумевает Sha256(x) = Sha256(y). Любая помощь будет принята с благодарностью. Код testpackage.adb package body Tes…
19 фев '21 в 18:01
1 ответ

Может ли SPARK доказать, что Quicksort действительно сортирует?

Я не пользуюсь СПАРК. Я просто пытаюсь понять возможности языка. Может ли SPARK доказать, например, что Quicksort действительно сортирует переданный ему массив?
22 мар '21 в 22:10
1 ответ

Создание предварительного условия в SPARK, проверяющем элемент массива, сообщает «проверка индекса массива может завершиться неудачно»

Продолжая свои усилия по переводу из Dafny в SPARK, я столкнулся с проблемами, создающими предварительное условие для массива, который должен быть отсортирован при вызове функции: type Integer_Array is array (Positive range <>) of Integer; fun…
10 окт '21 в 09:33
0 ответов

Самостоятельность в Spark 2014

Я пытаюсь написать зависимость потока процедуры в Ada и Spark 2014, и компилятор выдает мне среднее предупреждение, что medium: missing dependency "null => MyBool" medium: incorrect dependency "MyBool => MyBool" Вот мой файл .ads: SPARK_Mode (…
26 сен '22 в 16:32