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-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,463c5796782db6d8 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-04-10 16:27:06 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!news.airnews.net!cabal12.airnews.net!usenet From: "John R. Strohm" Newsgroups: comp.lang.ada Subject: Re: [Spark] Arrays of Strings Date: Thu, 10 Apr 2003 18:21:48 -0500 Organization: Airnews.net! at Internet America Message-ID: <0AF16DC5CF0F5631.90C7740553757FCD.D1A6F4ACFB3596A1@lp.airnews.net> X-Orig-Message-ID: References: <1049891888.75004@master.nyc.kbcfp.com> <1049908902.143649@master.nyc.kbcfp.com> Abuse-Reports-To: abuse at airmail.net to report improper postings NNTP-Proxy-Relay: library1-aux.airnews.net NNTP-Posting-Time: Thu Apr 10 18:24:19 2003 NNTP-Posting-Host: !^)5`1k-VUr58_r (Encoded at Airnews!) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2800.1106 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1106 Xref: archiver1.google.com comp.lang.ada:36068 Date: 2003-04-10T18:21:48-05:00 List-Id: "Hyman Rosen" wrote in message news:1049908902.143649@master.nyc.kbcfp.com... > Vinzent Hoefler wrote: > > The reliability is not in the subset like in MISRA-C, it is in the > > static analysis. I think, it is called *proof*. > > I am starting to be a little disturbed now that I've thought about > this a little more. You seem to be telling me that it's OK to have > variables declared loosely (Natural instead of the array range type) > becuase a program verifier will notice problems regardless. To me, > this seems contrary to to the design of Ada, which emphasizes saying > what you mean using the type system. I've been told here frequently > that Ada's style lends itself to avoiding buffer overflows because > you declare variables that loop over array ranges, and so there is > never an opportunity to go off the end. > > I find that the posted code looks very much like something you would > see in C (except for that awful buffer setting stuff). Disclaimer: This is not a discussion of SPARK as such, but instead of formal verification in the general sense. When you declare an array to be of a given size, you create a proof obligation that the subscript expression will always be in bounds. Satisfying this proof obligation is what you do during verification. Consider procedure main is i:integer; x: array(1..10) of real; begin for i in 2..4 loop x(2*i+1) := 0; end loop; end; The array X is declared to be (1..10). This generates an obligation that for all X(), 1 le and le 10. In this particular case, the verifier must satisfy for all i:integer, i in 2..4 --> (implies) 2*i+1 in 1..10 or for all i:integer, i in 2..4 --> 2*i in 0..9 or i in 2..4 --> i in 0..4 which is trivially true if your verifier knows how to deal with this kind of inequality processing. (That capability has existed since the late 1970s.) And even if your verifier doesn't understand inequality intervals, it can exhaustively enumerate all values of i that satisfy the hypothesis and check that they satisfy the conclusion. (Some model checkers do that kind of thing.) What normally happens is that you will generate a proof obligation that you may not be able to prove. This is normal. Usually, you can't DISPROVE a proof obligation, you can only fail to find a proof for it. (There exist mechanical procedures for finding proofs of theorems, that WILL succeed if a proof does in fact exist. They may take a while.) There are typically two reasons for this: 1) you haven't brought enough information into context, 2) you've uncovered a bug. (There is a third possibility: you've uncovered an instance of Godel's Theorem, but in practice that doesn't seem to happen.) Consider procedure main is i:integer; x: array(1..10) of real; begin for i in 2..4 loop x(2*i+3) := 0; end loop; end; The proof obligation will become i in 2..4 --> 2*i+3 in 1..10 i in 2..4 --> 2*i in -2..7 i in 2..4 --> i in -1..3 *TILT* At this point, your theorem prover will do something roughly analogous to throwing up its hands and saying "Beats me, daddy-O". (With apologies to Maynard G. Krebs...) You are expected to look at the problem, look at the code, and say "DOH!" and fix the obvious error. Yes, it would be a bit more self-documenting if i were declared to be integer(1..10), but it doesn't actually matter for verification. OK, but what if the subscript is coming from somewhere else? Simple. Consider procedure foo(i:integer) is x:array(1..10) of real; begin x(i) := 42; end; Again, a proof obligation is generated, to prove that i is in 1..10. The proof obligation must then be propagated to all of the callers of foo, and proved individually. Whether that obligation is propagated automatically by the verification environment, or manually by the programmer adding an entry specification annotation, is implementation-dependent. Obviously, either way will work. Made-up example: procedure foo(i:integer) is x:array(1..10) of real; entryspec i in 1..10; begin x(i) := 42; end; The use of an entry specification generally simplifies the verification of foo, in that it tells the verifier what it is allowed to assume. At the same time, it explicitly generates a proof obligation on the callers of foo.