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

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

Ada spark - Добавить -# Производное предложение

Я пытаюсь добавить пункт производных к этой процедуре, и это мое решение: - # получает индекс из ключа, данные и находят из данных, а я из данных; Я не уверен в этом, и мне нужна помощь procedure Find (Key: Integer ; Data : in MyArray ; Index : out …
11 янв '19 в 22:20
3 ответа

Значение постусловия

Я могу понять значение и цель предварительных условий в этом коде, но у меня есть проблема в понимании значения и цели постусловий. В Push Я знаю, что эта часть для увеличения указателя после нажатия целого числа ( Pointer = Pointer~ +1). В Pop Я по…
05 дек '18 в 12:57
1 ответ

Сумма квадратов в спарке

Для школьного проекта я должен написать статью о языке программирования SPARK, что я и сделал, однако часть его - написать короткую программу, которая принимает целое число n и выводит сумму квадратов от 1 до n. В C++ программа будет выглядеть приме…
31 май '14 в 12:02
1 ответ

Задачи в SPARK требуют последовательной проработки

В настоящее время я изучаю Аду во время университетского курса по языкам программирования в реальном времени и у меня есть вопрос о SPARK. Я работаю над проектом с задачей, которая контролирует автономный источник питания. Эта задача имеет решающее …
21 янв '18 в 12:46
1 ответ

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

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

СПАРК: gnatprove с опцией -gnato13 до неузнаваемости?

Я очень новичок в Ada/SPARK. Я пытался следовать некоторым урокам отсюда - http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html Предположим, я запускаю приведенный здесь пример ISQRT ( http://docs.adacore.com/spark2014-docs/html/ug/gnatprov…
13 ноя '14 в 01:47
2 ответа

Идентификатор Ada и SPARK `State` либо не объявлен, либо не виден в данный момент

Я делаю автоматическую защиту поезда на Аде с помощью подхода SPARK. Это моя спецификация в SPARK: package Sensors --# own State,Pointer,State1,State2; --# initializes State,Pointer,State1,State2; is type Sensor_Type is (Proceed, Caution, Danger, Un…
14 ноя '11 в 21:46
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 ответ

Контракт с неявной функцией недоступен для подтверждения

У меня есть процедура в пакете SPARK, которая вызывает некоторые функции из пакета none SPARK. procedure do_monitoring is U_C1 : constant Float := Sim.Get_U_C1; I_L1 : constant Float := Sim.Get_I_L1; U_C2 : constant Float := Sim.Get_U_C2; I_L2 : con…
23 янв '18 в 20:50
3 ответа

Нет глобального контракта для процедуры / функции

У меня есть процедура в модуле SPARK, которая вызывает стандарт Ada-Text_IO.Put_Line, Во время проверки я получаю следующее предупреждение warning: no Global contract available for "Put_Line", Я уже знаю, как добавить соответствующий контракт зависи…
23 янв '18 в 22:47
1 ответ

Ада Tasking и Безопасность

Я не люблю кодирование, но мне очень понравилась Ада, и я очень новичок в этом. Не могли бы вы разъяснить мне эти моменты? Если у вас есть компьютер с одним непотоковым процессором, задача по- прежнему будет однопроцессорной. То же самое относится и…
22 июн '15 в 11:03
1 ответ

В SPARK не разрешен вызов изменчивой функции в конфликтующем контексте.

В настоящее время я изучаю Аду во время университетского курса по языкам программирования в реальном времени и у меня есть вопрос о SPARK. Я работаю над проектом с задачей, которая контролирует автономный источник питания. Эта задача имеет решающее …
21 янв '18 в 18:58
0 ответов

Как доказать, что функция возвращается в течение 2 секунд в SPARK Ada?

Если вы посмотрите "SPARK Ada WCET", одним из первых результатов Google будет блог AdaCore, в котором говорится: Вместо проверки WCET с помощью SPARK, мы видим интерес к проверке дискретных временных свойств с помощью SPARK, таких как: "в течение по…
04 май '18 в 19:34
3 ответа

Завершение цикла

Я хочу доказать, что цикл в этой процедуре завершится с помощью варианта (связанная функция) вариант будет I и нижняя граница 0 (I: = 0) на каждом повторении, размер I будет уменьшаться до достижения нижней границы 0Как я могу доказать это I будет у…
24 янв '19 в 12:48
3 ответа

Spark Proof аннотация

Привет, я пытаюсь написать корректные аннотации от этой функции.. это написано с использованием языка программирования Spark function Read_Sensor_Majority return Sensor_Type is count1:Integer:=0; count2:Integer:=0; count3:Integer:=0; overall:Sensor_…
17 ноя '13 в 12:14
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
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