GNAT packages in Linux distributions
in [ADA]
|
From: Dmitry A. Kazakov on 12 May 2010 17:57 On Wed, 12 May 2010 20:53:45 +0200, Georg Bauhaus wrote: > On 12.05.10 20:33, Dmitry A. Kazakov wrote: > >>> Being better is precisely the point (of DbC). >>> DbC talks about proof obligations, not about provability. >> >> Who is obliged to whom in what? > > By being a programmer subscribing to the principles of DbC, > you are obliged to show that the components of your system > obey the components' contracts. The compiler and run-time > try to help you achieving this goal. A C programmer would tell you same story about merits of pointers, casts and preprocessor. >>> You cannot place an "if" in a specification. >> >> The answer was in my post. You have skipped out. OK, it was that exceptions >> from declarations is not a good idea. And considering it more deeply, >> Eiffel cannot do it either, because specifications are static things. > > Which set of "specifications" has only static things in it? > Why exclude conditionals whose results cannot reasonably > be computed by the compiler but > > (a) can be computed for every single case occuring in the > executing program If they can for *every* case, they are statically checkable, per definition. > (b) can guide the author of a client of a DbC component? I don't know what does it mean technically. Doesn't core dump guide programmers? Blue screens certainly do. > For example, assume that Is_Prime(N) is a precondition of sub P. > Furthermore, TIME(Is_Prime(N)) >> PERMISSIBLE_TIME. > Then, still, PRE: Is_Prime (N) expresses an obligation, > part of a contract: Don't call P unless N is prime, > no matter whether or not assertion checking is in effect. char X [80]; // Don't use X[80], X[81], no matter etc. > (A DbC principle is that assertions are *not* a replacement > for checking input (at the client side).) Exactly. Assertion is not a check. You said this. >>> What is "breach of contract" in your world? >> >> A case for the court. > > What's the court (speaking of programs)? A code revision. > I'm a programmer. If I "design" anything, it is a program whose > parts need to interact in a way that meets some almost entirely > non-mathematical specification. Mathematics has nothing to do with this. It is about a clear distinction between a contract and a condition, how undesirable it could be but nevertheless it is a condition, which you, as a programmer are obliged to consider as *possible*. Eiffel gives you an illusion of safety. This is even worse than C, which openly declares "I am dangerous." Simply consider the following rule: my program shall handle each exception I introduce. Objections? Then consider exceptions from assertions. >>> How would you specify >>> >>> subtype Even is ...; ? >> >> Ada's syntax is: >> >> subtype <name> is <name> <constraint>; > > What will static <name> and static <constraint> be for subtype Even? No, in Ada <constraint> is not required to be static. Example: procedure F (A : String) is subtype Span is Integer range A'Range; -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: stefan-lucks on 12 May 2010 20:37 On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks(a)see-the.signature wrote: > > > In Eiffel, I'll either get an answer, or the program will tell that at > > some point of time when computing, say, the factorial of 100, a certain > > exception has been raised. (I didn't try out Eiffel, but that is what I > > would expect.) But if I get an answer, I can be sure it is the right one. > > That is partial correctness. > > 1. Wrong answer is no more/less incorrect as an exception. We clearly disagree on this point. Consider being new in a town, and asking how to go from, say, the railway station to the market place. If we ask a guy who appears to be a local person in our eyes, but is actually as foreing as we are, most people would prefer an exception "sorry, I don't know the way" over the answer of being directed into the wrong direction. If you think, the "sorry" is as bad as the wrong direction, that is your problem, which I am not interested in discussing any further. Yes, there are some applications where the exception is just as bad as the wrong answer. One such example could be the autopilot of a plane. The plane may crash because the autopilot stops working, or because the autopilot acts on wrong results. Crash is crash. But not all applications have that severe requirments. In fact, event he autopilot may benefit from checks -- if these are performed when the plane is still on the ground, and if any failed test prevents the plane from starting. > 2. It is unrelated to error checks. The programmer did not use any. That > Eiffel possibly checks for integer overflow and C does not is irrelevant to > the issue. The exception may just as well be raised when checking the postcondition. > {Any Precondition} > raise Program_Error; > {Postcondition} Yes, that program is partially correct. Well, Hoare did originally not bother with exceptions, but the following program is partially correct even in the old we-do-not-know-about-exceptions sense: {Any Precondition} while false loop null; end loop; {Postcondition} > The problem is that Program_Error does not satisfy postcondition. > His approach, which I greatly appreciate, is perfectly compatible with > exceptions. Exception propagation is a part of the program behavior to be > checked as anything else. E.g. > > pre : x = 1 > if x = 1 then > raise Foo; > end if; > post : Foo propagating > > This program were be incorrect if it would not raise Foo. Now I see what you mean. You are asking for contracts which include exception propagation. Yes, that would be nice to have. Then you should like Eiffel, because this is what Eiffel actually does. In Eiffel, the formal postcondition require P; is a shortcut notation for the logical Postcondition: P or else (Postcondition_Violation propagating); (whatever the name of the exception is), which is the real postcondition of an Eiffel program. If Eiffel checks P at the end of the program, and raises that exception when the check fails, then Eiffel-programs are always correct! You don't even need to perform any static analysis to ensure their correctness. (But you must not turn of the checks!) Of course the catch is that you would rather want to specify postconditions which exclude exception propagation. I.e., you would need formal postconditions *without* the "or else propagate something" part. In Eiffel, there is no way to enforce such postconditions. And how should that be possible, without static analysis? Perhaps, the difference between SPARK and Eiffel DbC can be summarised as follows: -> Eiffel is a very expressive programming language, while SPARK is less expressive. -> The language for contracts in SPARK is more expressive than the language for contracts in Eiffel. That doesn't mean that the contracts you can express in Eiffel are invalid, however. -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------
From: Yannick Duchêne (Hibou57) on 12 May 2010 20:33 Le Wed, 12 May 2010 10:41:03 +0200, <stefan-lucks(a)see-the.signature> a écrit: > BTW, SPARK also only provides partial correctness, but no total > correctness. While SPARK allows to prove that no exception is raised (*), > it lacks the option to specify (and verify, of course) variants for > WHILE-loops (**). Eiffel supports such > invariants. > > [...] > > (**) I just read that the most recent version of SPARK is able to deal > with generics. Great! Maybe, SPARK has also recently learned how to > specify and prove loop variants? At the end of [Praxis SPARK 95 4.5] you may read the following : > It is also guaranteed that code is âreducibleâ, i.e. that > every loop has a single entry point, simplifying the > generation of verification conditions from loop invariants. So there are some proofs also made on loops at least (still need to learn more). -- pragma Asset ? Is that true ? Waaww... great
From: Georg Bauhaus on 12 May 2010 22:03 On 5/12/10 11:57 PM, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 20:53:45 +0200, Georg Bauhaus wrote: > >> On 12.05.10 20:33, Dmitry A. Kazakov wrote: >> >>>> Being better is precisely the point (of DbC). >>>> DbC talks about proof obligations, not about provability. >>> >>> Who is obliged to whom in what? >> >> By being a programmer subscribing to the principles of DbC, >> you are obliged to show that the components of your system >> obey the components' contracts. The compiler and run-time >> try to help you achieving this goal. > > A C programmer would tell you same story about merits of pointers, casts > and preprocessor. All of these features of C have merits besides what else they may have. But they sure don't warrant dismissing DbC? A C programmer is "right" when he tells an *analogous* story that competent C programmers will avoid typical mistakes by correct use of C features. ... whenever a competent C programmer is defined to be one who avoids these mistakes... A C programmer's tool set is difficult to use for correct, portable programs. For example, ADTs are mostly emulated via style and conventions, by programmers working correctly; there is little direct language support for ADTs in C. Ada seems better here. But before the arrival of preconditions etc. Ada didn't have that much to offer to programmers wanting to state sets of permissible values, for example for subprogram parameters. Or wanting to state relations required to hold between parameters. Ada subtypes, e.g. scalars, are poorly equipped for this style of value set specification, AFAICS. They do establish two implicit preconditions (>= S'First and <= S'Last). And these little things seem to do miracles already, judging by the model train study of McCormick. A Qi style type system could do more via types but is not to be in Ada any time soon, is it? Let alone a statically verifiable one. Hence my insistence on a worked out example of a subtype Even with a static specification of the intended value set, one that can be written by a single programmer. Alternatively, as is, package P is type Number is range 1 .. 10; function Compute (A, B: Number) return Number with Precondition => A >= B; type Number_Too is range 0 .. 10_000_000; function Compute_Too (A, B: Number_Too) return Number_Too with Precondition (A + B = 5_000_000); -- etc., with Precondition's predicate in O(P(N)); end; (Such specifications, if they were to be being static, would exclude a test of A in relation to B at run time, for example to reverse their order in a recursive call as needed. It would also exclude a simple test at run time that A + B = 5_000_000.) A distinguishing property of DbC visible here is that a programmer will *see* the contract (or part thereof). Whatever implementation of Compute will later be provided, he does not need to infer arguments in proper calls of Compute from looking at the code of the body (or its object code). Surely code review can provide results insofar as there will be no doubt about what (current!) preconditions can be inferred from the code. The code of the current implementation! Code review, meant as an alternative to giving preconditions, just seems impractical in the general case. Unlike DbC. >> Which set of "specifications" has only static things in it? >> Why exclude conditionals whose results cannot reasonably >> be computed by the compiler but >> >> (a) can be computed for every single case occuring in the >> executing program > > If they can for *every* case, they are statically checkable, per > definition. "Every case" cannot "reasonably be computed by the compiler". Continuing the examples above. (This argument is also somewhere in OOSC2.) >> (b) can guide the author of a client of a DbC component? > > I don't know what does it mean technically. Contractually, it means "do as the preconditions say." And the preconditions say more than an Ada type can ever say! A subprogram is perfect if there is little else to say than "of this subtype", but that isn't always possible. A responsible programmer will then write calls ensuring that an argument is even. Or that the first argument is greater than the second. The client programmer can arrange for these conditions only because he has clear, formal instructions written as preconditions. The contract guides him, it tells what to do. Why not have a computer language help us express these preconditions? Some can even be checked when we develop our software. A paradoxical consequence of this style of invitation (to please write your client code properly) is this: "Under no circumstances shall the body of a routine ever test for the routine's precondition." -- OOCS2, p.343 IOW, no redundant checks. Note that this is true with assertion checking on or off. And yes, the author does say something about defensive programming at the microscopic (routine) level: it should be avoided in DbC systems in favor of correct software. Have DbC help you write correct software instead. (There is more to say here, e.g. about the "magic" that is needed to program a correct defence...) >> For example, assume that Is_Prime(N) is a precondition of sub P. >> Furthermore, TIME(Is_Prime(N))>> PERMISSIBLE_TIME. >> Then, still, PRE: Is_Prime (N) expresses an obligation, >> part of a contract: Don't call P unless N is prime, >> no matter whether or not assertion checking is in effect. > > char X [80]; // Don't use X[80], X[81], no matter etc. Yes, and don't use X[-200]. But you can. OTOH: function Access_Element (S: String_80; X: Index_80); function Careful (S: String_80; X: Index_80) with Precondition => X rem 2 = 1; How would you write a statically checked version? >> (A DbC principle is that assertions are *not* a replacement >> for checking input (at the client side).) > > Exactly. Assertion is not a check. You said this. What check means, exactly, is important. DbC assertion checking or monitoring can turn assertions into run-time checks; these checks turned can be on or off, like pragma Assert in Ada. Input checking is something completely different. Input to a routine comes from a programmer's call. It is the programmer's obligation to make sure input is valid. It is not the called routine's obligation. Another input is I/O, which by the rules is checked for validity, too. >>>> What is "breach of contract" in your world? >>> >>> A case for the court. >> >> What's the court (speaking of programs)? > > A code revision. How do you become aware of a broken contract? Statically? Dynamically? Typically, I think, you notice a malfunctioning program or an exception occurrence; same with DbC. But DbC is also about specifying what you want before you have an issue and before you have a result of code review. In this sense, DbC extends an Ada spec. I guess you can even use DbC assertions in code review comparing results with your contracts. >> I'm a programmer. If I "design" anything, it is a program whose >> parts need to interact in a way that meets some almost entirely >> non-mathematical specification. > > Mathematics has nothing to do with this. It is about a clear distinction > between a contract and a condition, how undesirable it could be but > nevertheless it is a condition, which you, as a programmer are obliged to > consider as *possible*. Eiffel gives you an illusion of safety. No. Eiffel marketing claims that a fully proven DbC program is 100% bug free. I can't imagine that compiler makers will claim that such a program is guaranteed to automatically produce correct results for each input and presume that every input can be successfully tested for validity. They know about SPARK and TTBOMK they won't claim DbC to effect more than SPARK does. > Simply consider > the following rule: my program shall handle each exception I introduce. > Objections? No objection. > Then consider exceptions from assertions. That is what Eiffel's rescue mechanism is about. Failed assertions are one exception case (defined in $12.1 of OOSC2). BTW, there is a rule in DbC about the correctness of exception handlers of primitive operations. The rule starts from a call of a primitive operation that fails (to terminate its execution in a state satisfying the primitive operation's contract {post(x) and INV}. The primitive operation's exception handler is correct if it establishes its type's INV before propagating the exception to its caller. I am mentioning this to draw attention to the fact that DbC is not just a thin, fluffy wrapper for "raise when" or pragma Assert. If it were the latter, then it would be a bit like C style roll-your-own. >>>> How would you specify >>>> >>>> subtype Even is ...; ? >>> >>> Ada's syntax is: >>> >>> subtype<name> is<name> <constraint>; >> >> What will static<name> and static<constraint> be for subtype Even? > > No, in Ada<constraint> is not required to be static. Example: > > procedure F (A : String) is > subtype Span is Integer range A'Range; > Is the constraint, not to be static, then part of the contractual specification of subtype Even?
From: Phil Thornley on 13 May 2010 04:05
On 12 May, 17:49, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > ... The process was reloading its previous state from > variables each time it was resuming, and as there was obviously no way to > restore the stack pointer (JavaScript is not C or assembly you know), I > had to re-implement the stack this way. > > I suppose this kind of recursivity would be OK. Sure - you can make the data structures as complicated as you like - the recursion rules in SPARK only apply to the code structures. Cheers, Phil |