[Spark2014-discuss] SPARK 2014 strings. Basic I/O

David MENTRÉ dmentre at linux-france.org
Wed Jul 9 21:51:10 CEST 2014

Hello Yannick,

Sorry for the late reply, I don't have the luxury to do a daily exercise 
in SPARK. ;-)

2014-07-07 09:59, Yannick Moy:
> Yes, that's as designed. The mode "Auto" is the automatic mode when
> no other mode is set, but you cannot set it manually. To get what you
> want, you should remove the SPARK_Mode=>On from your configuration
> pragma file, and set it on the units that are in SPARK only.

This is the approach I have taken. Sometimes, it is better to put one's 
principles aside and use tools as designed by their creator. ;-)

I still have warnings but you warned me about some of them in a previous 
email. I'll look at them in more detail.

> An alternative is to define your own wrapper package on
> Bounded_String, and define wrapper subprograms for those subprograms
> you use. Then, mark the body (not the spec) of this wrapper package
> as SPARK_Mode=>Off. This time, the instantiation is inside the body
> marked SPARK_Mode=>Off, but the type and subprogram declarations that
> you call from SPARK code are in the SPARK spec.
> Or use your own SPARK unit for bounded strings. This is ultimately
> what we'll propose: a library of basic data structures and algorithms
> in SPARK.

Yes, the SPARK library of basic data structures is the way to go on the 
long term.

Best regards,

More information about the Spark2014-discuss mailing list