news@cs.yale.edu (Usenet News) (03/01/90)
In article <1880@clyde.concordia.ca> marcap@hercule.CS.Concordia.CA (PAWLOWSKY marc) writes: >consuming. For example I just wrote a class to perform quick_sort. The >properly check that the procedure has worked it is necessay to check >that the cardinality is still the same, all objects that entered the array >exit the array, the output is sorted. When an object is "put" into a >structure it should also be checked that the object is in the structure. I would expect that the postconditions for the standard Eiffel library would include assertions to perform the checking you describe (such assertions do seem like a good idea), but upon examination I see they don't. I wonder why not? They wouldn't be compiled into the libraries as distributed, and they would provide good examples of correct assertion writing. On another note, would it be possible for you to post your quicksort class? At what level of the library does it operate? I for one hope that such classes become more common. I like the Eiffel implementations of standard computer science data structures, but classes implementing standard CS _algorithms_ seem a bit further behind. They could be every bit as helpful, though.... >Marc Pawlowsky Grad Student Concodia University Rob Jellinghaus | "Next time you see a lie being spread or a jellinghaus-robert@CS.Yale.EDU | bad decision being made out of sheer ignor- ROBERTJ@{yalecs,yalevm}.BITNET | ance, pause, and think of hypertext." {everyone}!decvax!yale!robertj | -- K. Eric Drexler, _Engines of Creation_
marcap@hercule.cs.concordia.ca (PAWLOWSKY marc) (03/02/90)
In article <17412@cs.yale.edu> jellinghaus-robert@yale.UUCP writes: > >On another note, would it be possible for you to post your quicksort class? Ok, here it is. It is kinda messy and I will post a better version later on (cleaned up removing debug statements, plus probably adding heap sort). class ARRAY_COMPAR[T -> COMPARABLE] -- Marc Pawlowsky -- Graduate Student -- Concordia University -- Montreal, Quebec, Canada -- This file is placed in the public domain. It may be used -- freely as long as no charge is made for this file alone, -- or as part of a library package. Programs using this -- file may be charged for. -- Copyright 1990 Marc Pawlowsky export repeat ARRAY, is_sorted, is_sorted_range, quick_sort, merge, min_value, max_value, min_value_range, max_value_range, print_range inherit ARRAY[T] rename Create as array_create; STD_FILES feature Create(low, up: INTEGER) is do array_create(low, up); end; -- Create is_sorted: BOOLEAN is -- is the array sorted do debug output.putstring("is_sorted range is "); output.putint(lower); output.putstring(" .. "); output.putint(upper); output.new_line; end; -- debug Result := is_sorted_range(lower, upper); end; -- is_sorted is_sorted_range(low: INTEGER, up: INTEGER): BOOLEAN is -- the objects in low .. up in nondecreasing order require low_large_enough: low >= lower; up_small_enough: up <= upper; low_small_enough: low <= up; local i: INTEGER; k,l: T; do from i := up - 1; Result := True; invariant -- records greater than i are in nondecreasing order variant i until (not Result) or (i < low) loop k := item(i); l := item(i + 1); Result := (k <= l); debug k.print; output.putstring(" <= "); l.print; if Result then output.putstring(" True\n"); else output.putstring(" False\n"); end; -- if end; -- debug i := i - 1; end; -- loop end; -- is_sorted_range quick_sort is -- sort the array in nondescending order do qsort(lower, upper); ensure sorted: Current.is_sorted; end; -- quick_sort qsort(m,n:INTEGER) is -- sort records m..n into nondescending order local i,j: INTEGER; k, temp, t2: T; stop, stop2: BOOLEAN; do debug output.putstring("Entering qsort("); output.putint(m); output.putchar(','); output.putint(n); output.putstring(")\n"); end; -- debug -- QUICK SORT ALGORITHM if m < n then debug print_range(m, n); end; -- debug k := Current.item(m); from i := m + 1; j := n; invariant left_low: max_value_range(m, i - 1) <= k; right_high: (j < n) implies (min_value_range(j + 1, n) > k) variant ends_converging: j - i + 2 until i > j loop debug output.putstring("i="); output.putint(i); output.putstring(" j="); output.putint(j); output.new_line; print_range(i, j); end; -- debug if item(i) <= k then i := i + 1; elsif item(j) > k then j := j - 1 else -- swap item(i) and item(j) temp := item(i); t2 := item(j); put(temp, j); put(t2, i); i := i + 1; j := j - 1; end; -- if end; -- loop debug output.putstring("start recursion i="); output.putint(i); output.putstring(" j="); output.putint(j); output.new_line; print_range(m, n); end; -- debug temp := item(j); put(temp, m); put(k, j); debug print_range(m,n); end; -- debug check new_up_smaller: (j - 1) < n; new_low_larger: (j + 1) > m; end; qsort(m, j - 1); qsort(j + 1, n); debug output.putstring("Exiting qsort("); output.putint(m); output.putchar(','); output.putint(n); output.putstring(")\n"); print_range(m,n); end; -- debug end; -- if ensure (m < n) implies is_sorted_range(m, n); end; -- qsort merge(other: like Current): like Current is -- Give the sorted array after merging Current and Other require Current_sorted: Current.is_sorted; other_sorted: other.is_sorted; local i, j, k: INTEGER; do Result.Create(1, (other.count + Current.count)); from i:= 1; j := Current.lower; k := other.lower; invariant -- (Result.item(1 .. (i-1)) are sorted -- (old j < j) or (old k < k) variant (Result.count - i + 1) until (j > Current.upper) or (k > other.upper) loop if Current.item(j) <= other.item(k) then Result.put(Current.item(j), i); j := j + 1; else Result.put(other.item(k), i); k := k + 1; end; -- if i := i + 1; end; -- loop -- transfer the remaining records if j <= Current.upper then from invariant variant Current.count - j + 1 until j > Current.upper loop Result.put(Current.item(j), i); i := i + 1; j := j + 1; end; -- loop else from invariant variant other.count - k + 1 until k > other.upper loop Result.put(other.item(k), i); i := i + 1; k := k + 1; end; -- loop end; -- if end; -- merge print_range(low, up:INTEGER) is -- print low..up to output require low_large_enough: low >= lower; up_small_enough: up <= upper; low_small_enough: low <= up; local i: INTEGER; do from i:= low; variant up - i + 1 until i > up loop output.putint(i); output.putchar(' '); item(i).print; output.new_line; i := i + 1; end; -- loop end; -- print_range min_value: T is -- the minimum value in teh array do Result := min_value_range(lower, upper); end; -- min_value max_value: T is -- the maximum value in the array. do Result := max_value_range(lower, upper); end; -- max_value min_value_range(low, up: INTEGER): T is -- the lowest element in the array for the range low .. up require low >= lower; up <= upper; low <= up; local i: INTEGER; do from i:= up; Result := item(i); i := i - 1; invariant -- Result is the lowest for all j > i, Current.item(j) variant i - low + 1 until i < low loop if item(i) < Result then Result := item(i); end; -- if i := i - 1; end; -- loop end; -- min_value_range max_value_range(low, up: INTEGER): T is -- the highest element in the array for range low .. up require low >= lower; up <= upper; low <= up; local i: INTEGER; do from i:= up; Result := item(i); i := i - 1; invariant -- Result is the highest for all j > i, Current.item(j) variant i - low + 1 until i < low loop if item(i) > Result then Result := item(i); end; -- if i := i - 1; end; -- loop end; -- max_value_range end -- class ARRAY_COMPAR --------------------------------------------------------------------------- testing classes --------------------------------------------------------------------------- class COUNTER -- An integer counter export item, increment, decrement, add, set, out, repeat COMPARABLE inherit ANY redefine out; COMPARABLE redefine out feature item: INTEGER; out: STRING is -- print string do Result := item.out; end; -- out Create(i: INTEGER) is do item := i; end; -- Create set(i: INTEGER) is do item := i; ensure item = i; end; -- set increment is do item := item + 1; ensure (old item) + 1 = item; end; -- increment decrement is do item := item - 1; ensure (old item) - 1 = item; end; -- decrement add(x: INTEGER) is do item := item + x; ensure (old item) + x = item end; -- add infix "<" (other: like Current): BOOLEAN is -- Is current element less than `other` do Result := item < other.item; end; -- "<" end; -- class COUNTER class TEST_ARRAY_COMPAR inherit ANY; RANDOM_NUMBERS; STD_FILES feature amount: INTEGER is 20; Create is local a: ARRAY_COMPAR[COUNTER]; i,j,mini,maxi: INTEGER; k: COUNTER; do a.Create(1,amount); from i := amount; variant i until i < 1 loop j := random_int(1,9999); k.Create(j); a.put(k, i); i := i - 1; end; -- loop putstring("BEFORE:\n"); putstring("is sorted: "); if a.is_sorted then putstring("TRUE\n"); else putstring("FALSE\n"); end; -- if mini := a.min_value.item; maxi := a.max_value.item; putint(mini); putchar(' '); putint(maxi); new_line; from i := amount; variant i until i < 1 loop putint(a.item(i).item); new_line; i := i - 1; end; -- loop a.quick_sort; putstring("AFTER:\n"); putstring("is sorted: "); if a.is_sorted then putstring("TRUE\n"); else putstring("FALSE\n"); end; -- if mini := a.min_value.item; maxi := a.max_value.item; putint(mini); putchar(' '); putint(maxi); new_line; from i := amount; variant i until i < 1 loop putint(a.item(i).item); new_line; i := i - 1; end; -- loop end; -- Create end -- class TEST_ARRAY_COMPAR