Re: Buffer overflow Article - CACM

["Jeffrey R. Carter" <spam@spam.com>]

Harald Korneliussen wrote:
> 
> Thank you, that's very interesting. I'm still a bit sceptical about
> this static-sized internal structures thing, though. Isn't programming
> without dynamic allocation difficult? Last time I did it was in
> Commodore Basic, and that's because I didn't know how to do it then :-)
> 
> I would think that some software (for instance the browser and
> windowing system I'm using now) would be practically impossible to
> write in SPARK or similar languages?

SPARK is primarily for critical SW, where max sizes for things are typically 
known at compile time. But one can use SPARK for only the critical parts of a 
system, hiding the rest of the system from the SPARK tools.

Consider a stack of Integers:

package Integer_Stack
--# own State;
--# initializes State;
is
    function Is_Empty return Boolean;
    --# global State;

    procedure Clear;
    --# global out State;
    --# derives State from ;
    --
    --# post Is_Empty (State);

    procedure Push (Item : in Integer);
    --# global in out State;
    --# derives State from State, Item;
    --
    --# post not Is_Empty (State);

    procedure Pop (Item : out Integer);
    --# global in out State;
    --# derives State, Item from State;
    --
    --# pre not Is_Empty (State);
end Integer_Stack;

Now you can implement Integer_Stack in SPARK. Or you could hide the 
implementation from SPARK. In that case, it could use an instantiation of 
PragmARC.Stack_Bounded, adhering to the spirit of SPARK (static size) but not 
the letter (no generics). Or it could use an instantiation of 
PragmARC.Stack_Unbounded and have a dynamic size. (I deliberately omitted 
Is_Full and pre/post-conditions about fullness to allow such an implementation.)

SPARK puts 2 kinds of restrictions on Ada. There are restrictions that are 
needed to allow the kinds of analysis SPARK does, and there are restrictions to 
ensure everything is sized statically (of course, some fall into both 
categories). When you're writing SW for a PC, you generally can assume lots of 
storage and might be willing to allow dynamic sizing. It would be nice to still 
be able to do the SPARK analysis and be more confident that your SW is correct. 
That would entail an option to the tools that turns off the 2nd kind of 
restriction checking. I'm not even sure that would be possible, but I'd find it 
useful if it were.

-- 
Jeff Carter
"You tiny-brained wipers of other people's bottoms!"
Monty Python & the Holy Grail
18