Prev: What is your preferred VCS?
Next: GPS 2010 for AVR
From: Henrique on 30 Jul 2010 09:16 Thanks for the help (everyone). By using this concept of intervals, I made the modifications in my code to solve the problem. On 29 jul, 16:15, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > On Thu, 29 Jul 2010 11:21:52 -0700 (PDT), Henrique wrote: > > On Jul 29, 12:35 pm, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> > > wrote: > >> ------------------------ > >> var1 9.99900024414063E+02 > >> var4 9.99900085449219E+02 > > >> When rounded to 6 decimal digits both are same. But the underlying base > >> binary type is longer than 6 digits. > > >> P.S. It is always useful to think of floating point numbers as intervals > >> (which they are) rather than numbers. > > >> -- > >> Regards, > >> Dmitry A. Kazakovhttp://www.dmitry-kazakov.de > > > As I declared the type with 6 digits, I expected that it would make > > the comparison only for these digits (this would gave var4 = var1). > > No, the underlying base type is more or less free compiler choice. There > are certain rules, which in essence guarantee you accuracy of the basic > operations within the precision specified. > > > Do I always need to manually truncate the float number to the number > > of desired digits before making a comparison of them?? > > You should never use equality or inequality for floating-point types. They > do not have "physical" sense. As I said, floating-point numbers are > intervals. Two non-zero length [independent] intervals are *always* > unequal, even if their bounds are equal. > > > So what is the advantage of declaring it as "digits 6"? > > That the compiler guarantees you 6 decimal digits accuracy independently on > whatever hardware you have. The idea behind of Ada numeric types is machine > independence. You specify your requirements on the precision and range and > the compiler either gives you what you wanted or else rejects the program.. > > -- > Regards, > Dmitry A. Kazakovhttp://www.dmitry-kazakov.de- Ocultar texto das mensagens anteriores - > > - Mostrar texto das mensagens anteriores -
From: Dmitry A. Kazakov on 30 Jul 2010 10:34 On Fri, 30 Jul 2010 06:14:49 -0700 (PDT), Phil Clayton wrote: > Certainly ill-advised, but it can be difficult to know when this > difference matters. I think it could when intervals were used as keys in some sorted map. I learnt a couple of quite painful lessons when used keys (not intervals though), which appeared ordered to me, but in reality "<" was not transitive. > This gives me the perfect excuse to wheel out one > of my favourite examples. It's a great example that I keep coming > back to for many reasons. > > We want a 3-way min function (for integers or reals) that gives > > Y = min {A, B, C} > > and we are given > > if A < B and A < C > then > Y := A; > elsif B < C and B < A > then > Y := B; > else > Y := C; > end if; > > The justification given is > > if A is smallest, set Y to A > else if B is smallest, set Y to B > else C is smallest so set Y to C A great example. I think every programmer wrote something like above at least once. [...] > I often bring this example up to motivate the use of formal methods as > it is particularly difficult to find the error through testing, > especially when A, B and C are real types. Absolutely. Same happens when a poor "<" is used for sorting. It is very difficult to detect the problem through blind testing. The thing is so nasty that it can easily pass a branch coverage test. People overestimate the power of testing, because they often have a mental model where the behavior is monotonic. They test for the extremes and consider the rest granted. Your example shows how wrong this presumption is already in apparently "trivial" cases. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Stephen Leake on 31 Jul 2010 11:12 Phil Clayton <phil.clayton(a)lineone.net> writes: > if A < B and A < C > then > Y := A; > elsif B < C and B < A > then > Y := B; > else > Y := C; > end if; > > The justification given is > > if A is smallest, set Y to A > else if B is smallest, set Y to B > else C is smallest so set Y to C > > Unfortunately, the program doesn't work. If you haven't spotted why, > it is well worth trying to work it out, perhaps with a few test cases. > > In fact, this particular error came to various people's attention > because it made its way though all stages of a safety-critical > software development process. (Fortunately the consequences were not > too serious, though intriguing.) The program fails exactly when A = B > < C because it returns C, which is not the minimum. I am _always_ suspicious of 'and' conditions in nested if/then/else; it is easy to leave out a case. If this had been written: if A < B then if A < C then Y := A; else -- A >= C ... The problem would have been clear from the start. > I often bring this example up to motivate the use of formal methods as > it is particularly difficult to find the error through testing, > especially when A, B and C are real types. What are the chances of > having A equal to B? 100%, for a rationally designed test! Clearly to cover all cases, you need A < B, A = B, A > B, A < C, etc. > Where does the original justification go wrong? Well, when talking > about 'the smallest' there is an implicit assumption being made that > it is unique. The justification never considers the case when A or B > is the non-unique smallest. And the same error could be made in a formal specification. "formal" does _not_ mean "complete"! > Of course, the correct program just uses "<=" instead of "<", That would be one way, but it would still require the same detailed analysis and test. I prefer the exhaustive if/then/else style above. -- -- Stephe
From: Phil Clayton on 2 Aug 2010 21:07 On Jul 31, 4:12 pm, Stephen Leake <stephen_le...(a)stephe-leake.org> wrote: > Phil Clayton <phil.clay...(a)lineone.net> writes: > > if A < B and A < C > > then > > Y := A; > > elsif B < C and B < A > > then > > Y := B; > > else > > Y := C; > > end if; > > > The justification given is > > > if A is smallest, set Y to A > > else if B is smallest, set Y to B > > else C is smallest so set Y to C > > > Unfortunately, the program doesn't work. If you haven't spotted why, > > it is well worth trying to work it out, perhaps with a few test cases. > > > In fact, this particular error came to various people's attention > > because it made its way though all stages of a safety-critical > > software development process. (Fortunately the consequences were not > > too serious, though intriguing.) The program fails exactly when A = B > > < C because it returns C, which is not the minimum. > > I am _always_ suspicious of 'and' conditions in nested if/then/else; it > is easy to leave out a case. If this had been written: > > if A < B then > if A < C then > Y := A; > else > -- A >= C > ... > > The problem would have been clear from the start. > > > I often bring this example up to motivate the use of formal methods as > > it is particularly difficult to find the error through testing, > > especially when A, B and C are real types. What are the chances of > > having A equal to B? > > 100%, for a rationally designed test! Justifying that a set of test cases has a 100% chance of finding an error (when not testing all combinations of all input values) will unavoidably involve formal reasoning, similar to that used for formal methods. I was really talking about less formal approaches to testing. > Clearly to cover all cases, you > need A < B, A = B, A > B, A < C, etc. You make it sound easy... Generally, how do you justify that tests 'cover all cases' so giving you a 100% chance of finding an error? Note that even if I had test cases that exercise all possible orderings of A, B and C, I am not guaranteed to find an error in an incorrect implementation of Y = min {A, B, C}. For example, I could have chosen positive values for A in every test but the program could have contained an extra erroneous condition ... and 0 < A that would have gone undetected. So the tests need to take account of the particular implementation too. > > Where does the original justification go wrong? Well, when talking > > about 'the smallest' there is an implicit assumption being made that > > it is unique. The justification never considers the case when A or B > > is the non-unique smallest. > > And the same error could be made in a formal specification. "formal" > does _not_ mean "complete"! Although I said "formal methods", I use this example to motivate formal verification, not formal specification. Any specification, formal or not, can be a load of rubbish! > > Of course, the correct program just uses "<=" instead of "<", > > That would be one way, but it would still require the same detailed > analysis and test. I prefer the exhaustive if/then/else style above. In the absence of any formal verification support, it's probably a good idea to keep things simple like that. Phil
From: Shark8 on 2 Aug 2010 23:31
On Aug 2, 7:07 pm, Phil Clayton <phil.clay...(a)lineone.net> wrote: > On Jul 31, 4:12 pm, Stephen Leake <stephen_le...(a)stephe-leake.org> > wrote: > > > Any specification, > formal or not, can be a load of rubbish! > > Phil You are absolutely right, just look at: Unix, Linux, C, C++, X, Perl, OpenGL's enumeration, etc. |