From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,5bc4be576204aa20 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!newsfeed.stanford.edu!headwall.stanford.edu!newshub.sdsu.edu!elnk-nf2-pas!newsfeed.earthlink.net!stamper.news.pas.earthlink.net!newsread3.news.pas.earthlink.net.POSTED!a6202946!not-for-mail From: "Jeffrey R. Carter" Organization: jrcarter at acm dot org User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.7.12) Gecko/20050915 X-Accept-Language: en-us, en MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Buffer overflow Article - CACM References: <3tr6hiFu7jr6U1@individual.net> <1133252164.539307.165050@g49g2000cwa.googlegroups.com> <1133427713.922566.268390@g43g2000cwa.googlegroups.com> In-Reply-To: <1133427713.922566.268390@g43g2000cwa.googlegroups.com> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Message-ID: Date: Thu, 01 Dec 2005 17:58:54 GMT NNTP-Posting-Host: 67.3.216.198 X-Complaints-To: abuse@earthlink.net X-Trace: newsread3.news.pas.earthlink.net 1133459934 67.3.216.198 (Thu, 01 Dec 2005 09:58:54 PST) NNTP-Posting-Date: Thu, 01 Dec 2005 09:58:54 PST Xref: g2news1.google.com comp.lang.ada:6713 Date: 2005-12-01T17:58:54+00:00 List-Id: 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