SPARK 2014 is a programming language derived from Ada. SPARK 2014 has been developed with compile-time proof of absence of run-time errors in mind. It is possible to write programs as a mix of SPARK 2014 and Ada 2012.
Questions tagged [spark-2014]
20 questions
12
votes
3 answers
Proving Floor_Log2 in Spark
New to Spark, and new to Ada, so this question may be overly broad. However, it's asked in good faith, as part of an attempt to understand Spark. Besides direct answers to the questions below, I welcome critique of style, workflow, etc.
As my first…
addaon
- 1,097
- 9
- 25
5
votes
2 answers
How to make Pre and Post conditions for recursive functions in SPARK?
I'm translating an exercise I made in Dafny into SPARK, where one verifies a tail recursive function against a recursive one. The Dafny source (censored, because it might still be used for classes):
function Sum(n:nat):nat
decreases n
{
if…
Andreas
- 5,086
- 3
- 16
- 36
4
votes
2 answers
Failed assert that libsparkcrypto SHA256 results are equal
Summary of my issue
I am using the libsparkcrypto library for my SHA256 function. I am finding that I cannot Assert that x = y implies Sha256(x) = Sha256(y). Any help would be greatly appreciated.
Code
testpackage.adb
package body TestPackage with
…
WhaleDancer
- 83
- 7
4
votes
1 answer
Postcondition on a procedure doesn't prove even though the same condition is asserted and true at the end of procedure
The code looks like this:
spec:
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
…
Dmitry Petukhov
- 53
- 6
4
votes
3 answers
SPARK Integer overflow check
I have the following program:
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;
If I run gnatprove, I get the…
rid
- 61,078
- 31
- 152
- 193
4
votes
2 answers
Spark-Ada postcondition for array total
How does one write a Spark postcondition for a function that sums the elements of an array? (Spark 2014, but if someone shows me how to do it for an earlier Spark I should be able to adapt it.)
So if I have:
type Positive_Array is array (Positive…
digitig
- 1,989
- 3
- 25
- 45
2
votes
1 answer
Making a precondition in SPARK checking array element reports 'array index check might fail'
Continuing my efforts transcribing from Dafny to SPARK I run into problems making a precondition for an array that should be sorted on invoking the function:
type Integer_Array is array (Positive range <>) of Integer;
function BinarySearch(a :…
Andreas
- 5,086
- 3
- 16
- 36
2
votes
1 answer
Can SPARK be used to prove that Quicksort actually sorts?
I'm not a user of SPARK. I'm just trying to understand the capabilities of the language.
Can SPARK be used to prove, for example, that Quicksort actually sorts the array given to it?
(Would love to see an example, assuming this is simple)
MWB
- 11,740
- 6
- 46
- 91
2
votes
2 answers
Find factor of a number
I want to find the smallest factor of a value with below specification
procedure S_Factor (N : in out Positive; Factor : out Positive) with
SPARK_Mode,
Pre => N > 1,
Post => (Factor > 1) and
(N'Old / Factor = N)…
PoliteMan
- 43
- 4
2
votes
1 answer
How to prove a Ada/SPARK precondition on a function embedded in a double loop
I'm trying to prove that the precondition of "prepend" holds during the execution of the program below. The precondition is:
Length (Container) < Container.Capacity
My attempts at proving this are in the code below in the form of pragmas. I can…
LT 'syreal' Jones
- 97
- 1
- 9
1
vote
1 answer
How to use Assert and loop_invariants
Specification:
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 ;
I want to write…
PoliteMan
- 43
- 4
1
vote
2 answers
In need of the lexical and the grammar sheet of the ada programming language spark 2014
In need of the lexical and the grammar sheet of the Ada programming language spark 2014 can anyone help, please.
thanks in advance.
M.Mar
- 91
- 1
- 3
1
vote
2 answers
Instantiating non-library-level package in SPARK Ada
How do I instantiate a non-library-level package in SPARK Ada?
Say I have something like:
subtype Die is Integer range 1..6;
package Random_Die
is
new Ada.Numerics.Discrete_Random(Die);
That gives me the errors:
instantiation error at…
digitig
- 1,989
- 3
- 25
- 45
0
votes
0 answers
Self dependency in Spark 2014
I'm trying to write the flow dependency of a procedure in Ada and Spark 2014 and the compiler give me a medium warning that
medium: missing dependency "null => MyBool"
medium: incorrect dependency "MyBool => MyBool"
Here is my .ads file:
SPARK_Mode…
Architek
- 53
- 5
0
votes
0 answers
GNATprove : "overflow check might fail" in exponentiation function
I can't solve this problem with SPARK 2018, I think I need some invariant to solve the problem of overflow, but I have already tried everything and can not find it. If someone could shed some light on my problem.
I'll try Exponentiation by simple…
Michael Bueno
- 33
- 1
- 1
- 5