Float conversion
in [ADA]
|
Prev: What is your preferred VCS?
Next: GPS 2010 for AVR
From: Phil Clayton on 5 Aug 2010 06:20 On Aug 4, 8:26 am, Stephen Leake <stephen_le...(a)stephe-leake.org> wrote: > >> > 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! > > What are you verifying, if not a specification? > > If the specification is rubbish, what is the point of verifying it? Well, in practice, you would hope that if someone knew a specification was wrong/incomplete that they wouldn't go ahead and implement it! What if a specification is clear but - not obviously - contains undesired features? It can be argued that a convincing verification is valuable regardless of the specification quality because, when something goes wrong, you know that it is less likely to be an implementation issue and more likely to be a specification issue. So it helps isolate issues. In practice, any sane person would review the specification first to reduce the likelihood of change and subsequent process iteration. So there are two separate issue here: 1. Is the specification capturing what is wanted (`validation') 2. Does the program implement the specification (`verification') I was only considering 2 in this thread and trying to avoid the other minefield that is 1! Phil
From: Stephen Leake on 5 Aug 2010 08:05 Robert A Duff <bobduff(a)shell01.TheWorld.com> writes: > Stephen Leake <stephen_leake(a)stephe-leake.org> writes: > >> Phil Clayton <phil.clayton(a)lineone.net> writes: >> >>> On Jul 31, 4:12 pm, Stephen Leake <stephen_le...(a)stephe-leake.org> >>> wrote: >>>> Clearly to cover all cases, you >>>> need A < B, A = B, A > B, A < C, etc. >>> >>> You make it sound easy... >> >> It is easy! This is a very small program; exhaustive testing is >> appropriate. > > I wouldn't call that "exhaustive". To me, exhaustive testing means > testing every possible input. There are far more than 9. Yes, that's true. > You seem to be using some sort of coverage metric, not exhaustive > testing. Yes. >> According to the code, there are three important edge cases for each >> pair: A < B, A = B, A > B > > I don't understand that. Phil Clayton's example was: > > if A < B and A < C > then > Y := A; > elsif B < C and B < A > then > Y := B; > else > Y := C; > end if; > > (Interesting example, by the way!) I was talking about my rewrite, which got rid of the 'and' operators to make things clearer. > And why not A=B-epsilon? That's one appropriate test case for A < B, along with A = B - 1.0. > By the way, putting: > > pragma Assert (C < B and C < A); > > after "else" might have made the bug clearer. Or might not. That's a good idea. >> What are you verifying, if not a specification? > > You can't formally verify specifications. You can (sometimes) formally > verify that the code matches a specification. That's what I meant; the verification process is meaningless without a specification. -- -- Stephe
From: Shark8 on 7 Aug 2010 01:54 > I don't understand that. Phil Clayton's example was: > if A < B and A < C > then > Y := A; > elsif B < C and B < A > then > Y := B; > else > Y := C; > end if; > (Interesting example, by the way!) This could be written better as: Function Min( A, B, C : SOME_TYPE ) is begin If A < B AND A < C then return A; -- We know A is the smallest valued var here... elsif B < C then -- and in the ELSE case we know that it is not the smallest value. -- If A is equal to C or B then returning that value is equivalent to returning A's value. return B; else -- We know here that C is the low-valued parameter. return C; end Min; You could also add the Pragma 'inline' if you wanted.
From: Georg Bauhaus on 7 Aug 2010 04:56 On 8/7/10 7:54 AM, Shark8 wrote: > Function Min( A, B, C : SOME_TYPE ) is > begin > If A< B AND A< C then > return A; -- We know A is the smallest valued var > here... > elsif B< C then -- and in the ELSE case we know that it is > not the smallest value. > -- If A is equal to C or B then returning > that value is equivalent to returning A's value. > return B; Generalizing, when Min returns not the values but identities, will the equivalence of A and B work when stable sorting is needed? Another question, are there algorithms that rely on the representation of A, B, and C so that equivalence doesn't establish equality? Georg
From: Shark8 on 7 Aug 2010 09:49
On Aug 7, 2:56 am, Georg Bauhaus <rm-host.bauh...(a)maps.futureapps.de> wrote: > On 8/7/10 7:54 AM, Shark8 wrote: > > > Function Min( A, B, C : SOME_TYPE ) is > > begin > > If A< B AND A< C then > > return A; -- We know A is the smallest valued var > > here... > > elsif B< C then -- and in the ELSE case we know that it is > > not the smallest value. > > -- If A is equal to C or B then returning > > that value is equivalent to returning A's value. > > return B; > > Generalizing, when Min returns not the values but identities, > will the equivalence of A and B work when stable sorting is needed? > > Another question, are there algorithms that rely on > the representation of A, B, and C so that equivalence > doesn't establish equality? > > Georg Good questions. In regard to the stability, I'm under the impression that is a property of the algorithm rather than the comparative-operation. {For example Shell sort is NOT a "stable" sot, but it uses the same operator that merge sort uses; merge sort *is* stable.} For the equivalence/equality question I think it's a matter of the data-type rather than the algorithm that determines it. For example we could define a Set Type with the operation "<" returning true if Left is a proper/strict subset of Right (that is to say fully contained by the superset and NOT equal to it). Now, given a set [Red, Blue, Green, Purple, Yellow, Gray] both [Red,Green,Blue] & [Red, Yellow, Blue] are subsets thereof and return true for "<". However, neither of the subsets are equal or subsets of one another; so we cannot use "<" alone to determine how to 'sort' this group of sets. |