Re: "Ravenscar-like" profile for C/C++

[aek@vib.usr.pu.ru (Alexander Kopilovitch)]

Peter Amey wrote:

> > if they had plans for a C++ version and they told they had spent
> > plenty time thinking about how one could achieve something
> > worthwhile for C++ and similar to SPARK but they just couldn't
> > think of anything!
>
> Your memory serves you well!  I don't think things have changed that 
> much.  My personal view is that any such subset, if it did exist, would 
> be so restrictive and unnatural to typical C++ users that they would 
> find it unacceptable.  Persuading a potential Ada user of the merits of 
> SPARK is a much easier proposition because they have already taken 
> several steps down the early error detection route.

How about SPARK-classes for C++? I mean regular C++ classes, but with attribute
SPARK (in GCC you can relatively easily define such additional attributes for
classes, it will look something like __SPARK__), which tells that the class
conforms with SPARK-imposed restrictions. In other words, SPARK in C++ can be
applied for individual classes, which can be mixed in a program (and even in
an individual source file) with other (non-SPARK) classes.

Perhaps many C++ programmers will find this approach acceptable, they may
perceive it as reasonable and useful compromise. (And there will be nothing
heretic in that - even in SPARK applications for Ada it may happen that some
packages are for SPARK examination, while others bypass SPARK for some reasons).



Alexander Kopilovich                      aek@vib.usr.pu.ru
Saint-Petersburg
Russia