Re: Processing array subsections, a newbie question.

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Sat, 12 Jun 2010 21:11:33 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> Now suppose I want to write a procedure that performs an operation on a
> subsection of a Buffer_Type object. Ultimately the code needs to be  
> SPARKable
> so I can't use slices (true?). Let's say I do something like
I was pretty sure, however, I still checked.

RavenSPARK language manual, 4.1.2, says
4.1.2 Slices
Slices are not allowed in SPARK.

Confirmed

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.