************************************************************************ ** Maysa-Maria Peterson SE507 March 16, 1996 ** ** Quick Sort Assertion Testing ** ** Log File ** ************************************************************************ GNAT Compiler Version 3.01 Copyright 1995 Free Software Foundation, Inc. Compiling: assert.ads (source file time stamp: 1996-03-16 01:04:10) No code generated for file assert.ads (package spec) 1. package Assert is 2. -- Copyright (c) 1995,1996 John Beidler 3. -- Computing Sciences Dept. 4. -- Univ. of Scranton, Scranton, PA 18510 5. -- 6. -- (717) 941-7446 voice 7. -- (717) 941-4250 FAX 8. -- beidler@cs.uofs.edu 9. -- 10. -- For use by non-profit educational institutions only. 11. -- This software is GUARANTEED. Please report any errors. All 12. -- corrections will be made as soon as possible (normally within 13. -- one working day). 14. ------------------------------------------------------------------ 15. 16. procedure Precondition (Condition : boolean ; 17. Prefix : String ; 18. True_Message : String ; 19. False_Message: String ) ; 20. -------------------------------------------------------------------- 21. -- Pre-cond : None 22. -- Post-cond : if Condition then display True_Message 23. -- else display False_Message ; 24. -- depending upon the operating mode 25. -------------------------------------------------------------------- 26. 27. procedure Postcondition (Condition : boolean ; 28. Prefix : String ; 29. True_Message : String ; 30. False_Message: String ) ; 31. -------------------------------------------------------------------- 32. -- Pre-cond : None 33. -- Post-cond : if Condition then display True_Message 34. -- else display False_Message ; 35. -- depending upon the operating mode 36. -------------------------------------------------------------------- 37. 38. procedure Invariant (Condition : boolean ; 39. Prefix : String ; 40. True_Message : String ; 41. False_Message: String ) ; 42. -------------------------------------------------------------------- 43. -- Pre-cond : None 44. -- Post-cond : if Condition then display True_Message 45. -- else display False_Message ; 46. -- depending upon the operating mode 47. -------------------------------------------------------------------- 48. 49. procedure Assertion (Condition : boolean ; 50. Prefix : String ; 51. True_Message : String ; 52. False_Message: String ) ; 53. -------------------------------------------------------------------- 54. -- Pre-cond : None 55. -- Post-cond : if Condition then display True_Message 56. -- else display False_Message ; 57. -- depending upon the operating mode 58. -------------------------------------------------------------------- 59. 60. Procedure Beta_Mode; 61. -------------------------------------------------------------------- 62. -- Pre-cond : None 63. -- Post-cond : Place package in Beta_Mode 64. -- Comment : In Beta_Mode the package only displays the False_Message 65. -------------------------------------------------------------------- 66. 67. Procedure Alpha_Mode; 68. -------------------------------------------------------------------- 69. -- Pre-cond : None 70. -- Post-cond : Place package in Alpha_Mode (default) 71. -- Comment : In Alpha_Mode all messages are displayed 72. -------------------------------------------------------------------- 73. 74. Procedure Silent_Mode (File_Name: string); 75. -------------------------------------------------------------------- 76. -- Pre-cond : None 77. -- Post-cond : All messages displayed to a file. 78. -- If Silent_Mode is not used, all messages are 79. -- displayed on the system output device 80. -- NOTE : In silent mode, all messages are preceeded by the year 81. -- month, day, and time of the message. 82. -------------------------------------------------------------------- 83. 84. Procedure Off; 85. -------------------------------------------------------------------- 86. -- Pre-cond : None 87. -- Post-cond : Displaying of assertions is suspended 88. -------------------------------------------------------------------- 89. 90. Procedure On; 91. -------------------------------------------------------------------- 92. -- Pre-cond : None 93. -- Post-cond : Displaying of assertions is turned on (default) 94. -------------------------------------------------------------------- 95. 96. procedure Pause; 97. -------------------------------------------------------------------- 98. -- Pre-cond : None 99. -- Post-cond : May be used to temporarily suspend the program while 100. -- you read the assertions when not in Silent_Mode. 101. -------------------------------------------------------------------- 102. 103. generic 104. type Univ_Range is (<>); 105. type Array_Object is limited private; 106. type Array_Type is array (Univ_Range range <>) of Array_Object; 107. with function Condition (i: Univ_Range; A: Array_Type) return boolean; 108. function A_For_All (Left, 109. Right: Univ_Range; 110. A : Array_Type) return boolean; 111. -------------------------------------------------------------------- 112. -- Pre-cond: None 113. -- Returns : true iff {Condition (i,A) is true for all i in (Left,Right)} 114. -------------------------------------------------------------------- 115. 116. generic 117. type Univ_Range is (<>); 118. type Array_Object is limited private; 119. type Array_Type is array (Univ_Range range <>) of Array_Object; 120. with function Condition (i: Univ_Range; A: Array_Type) return boolean; 121. function A_There_Exists (Left, 122. Right: Univ_Range; 123. A : Array_Type) return boolean; 124. -------------------------------------------------------------------- 125. -- Pre-cond: None 126. -- Returns : true iff {Condition (i,A) is true for at least one i in (Left,Right)} 127. -------------------------------------------------------------------- 128. 129. generic 130. type Univ_Range is (<>); 131. with function Condition (i: Univ_Range) return boolean; 132. function R_For_All (Left, Right: Univ_Range) return boolean; 133. -------------------------------------------------------------------- 134. -- Pre-cond: None 135. -- Returns : true iff {Condition (i,A) is true for all i in (Left,Right)} 136. -------------------------------------------------------------------- 137. 138. generic 139. type Univ_Range is (<>); 140. with function Condition (i: Univ_Range) return boolean; 141. function R_There_Exists (Left, Right: Univ_Range) return boolean; 142. -------------------------------------------------------------------- 143. -- Pre-cond: None 144. -- Returns : true iff {Condition (i,A) is true for at least one i in (Left,Right)} 145. -------------------------------------------------------------------- 146. 147. generic 148. type Univ_Range is (<>); 149. type Key_Type is limited private; 150. type Array_Object is limited private; 151. type Array_Type is array (Univ_Range range <>) of Array_Object; 152. with function Condition (i: Univ_Range; Key: Key_Type; 153. A: Array_Type) return boolean; 154. function Key_Compare(Left, Right: Univ_Range; 155. Key : Key_Type; 156. A : Array_Type) return boolean; 157. -------------------------------------------------------------------- 158. -- Pre-cond: None 159. -- Returns : true iff {Condition (i,key,A) is true for all i in (Left,Right)} 160. -------------------------------------------------------------------- 161. 162. end Assert ; 162 lines: No errors GNAT Compiler Version 3.01 Copyright 1995 Free Software Foundation, Inc. Compiling: assert.adb (source file time stamp: 1996-03-16 00:47:36) 1. with Text_IO, Calendar; 2. use Calendar; 3. 4. package body Assert is 5. 6. package tio renames text_io; 7. package iio is new text_io.integer_io(integer); 8. 9. type Main_Switch_Type is (on, off); 10. type Package_Mode_Type is (Alpha, Beta); 11. type Str_Ptr is access string; 12. subtype Month_Name is string (1..4); 13. type Month_Array_Type is array (1..12) of Month_Name; 14. 15. Main : Main_Switch_Type := on; 16. Package_Mode: Package_Mode_Type:= Alpha; 17. 18. Time_Of_Day : Time; 19. Year, Month, Day: natural; 20. Seconds: Day_Duration; 21. MON : Month_Array_Type := (" jan", " feb", " mar", " apr", " may", " jun", 22. " jul", " aug", " sep", " oct", " nov", " dec"); 23. 24. Display_File : tio.File_Type; 25. File_Name_Ptr: Str_Ptr := null; 26. 27. procedure Sec_To_Str (Second: in Day_Duration; 28. Str: in out string) is 29. Time : integer := integer (Second); 30. Hrs, Min, Sec: integer; 31. begin -- Sec_To_Str 32. Hrs := Time / 3600; 33. Time := Time - 3600*Hrs; 34. Min := Time / 60; 35. Sec := Time - 60*Min; 36. if Hrs < 10 then 37. Str (2..3) := integer'image (Hrs); 38. Str (1..2) := " 0"; 39. else 40. Str (1..3) := integer'image (Hrs); 41. end if; 42. if Min < 10 then 43. Str (5..6) := integer'image (Min); 44. Str (4..5) := ":0"; 45. else 46. Str (4..6) := integer'image (Min); 47. Str (4..4) := ":"; 48. end if; 49. if Sec < 10 then 50. Str (8..9) := integer'image (Sec); 51. Str (7..8) := ":0"; 52. else 53. Str (7..9) := integer'image (Sec); 54. Str (7..7) := ":"; 55. end if; 56. 57. end Sec_To_Str; 58. ----------------------------------------------------- 59. procedure Assertion_Test (Condition : boolean; 60. Type_Message : string; 61. Prefix : String; 62. True_Message : String; 63. False_Message: String) is 64. procedure Display_Msg (Msg: string) is 65. Tod : string (1..9); 66. begin -- Display_Msg 67. if File_Name_Ptr = null then 68. tio.Put (Msg); tio.New_Line; 69. else 70. begin 71. tio.Open (Display_File, tio.Append_File, File_Name_Ptr.all); 72. --\\tio.Put_Line ("Append"); 73. exception 74. when others => tio.Create (Display_File, tio.Out_File, File_Name_Ptr.all); 75. tio.Put_Line ("Create"); 76. 77. end; 78. Time_of_Day := Clock; 79. Split (Time_of_Day, Year, Month, Day, Seconds); 80. Sec_To_Str (Seconds, ToD); 81. iio.Put (Display_File, Year, 0); 82. tio.Put (Display_File, MON(Month) & " "); 83. iio.Put (Display_File, Day, 0); 84. tio.Put (Display_File, ToD); 85. tio.Put (Display_File, " " & Msg); 86. --| tio.Put_Line (Display_File, 87. --| integer'image(Year) & integer'image(Month) 88. --| & integer'image(Day) & Day_Duration'image(Seconds) 89. --| & Msg); 90. tio.New_Line (Display_File); 91. tio.Close (Display_File); 92. end if; 93. end Display_Msg; 94. -------------------------------------------------- 95. begin -- Assertion_Test 96. if Main = on then 97. if not Condition then 98. Display_Msg (Type_Message & ":[F] " & Prefix & False_Message); 99. elsif Package_Mode = Alpha then 100. Display_Msg (Type_Message & ":[T] " & Prefix & True_Message); 101. end if ; 102. end if ; 103. exception 104. when others => Display_Msg (Type_Message & ":[X] " & Prefix & False_Message); 105. end Assertion_Test; 106. ----------------------------------------------------- 107. procedure Precondition (Condition : boolean; 108. Prefix : String; 109. True_Message : String; 110. False_Message: String) is 111. begin -- Precondition 112. Assertion_Test (Condition, "PRE ", Prefix, True_Message, False_Message); 113. end Precondition; 114. ----------------------------------------------------- 115. procedure Invariant (Condition : boolean; 116. Prefix : String; 117. True_Message : String; 118. False_Message: String) is 119. 120. begin -- Invariant 121. Assertion_Test (Condition, "INV ", Prefix, True_Message, False_Message); 122. end Invariant; 123. ----------------------------------------------------- 124. procedure Postcondition (Condition : boolean; 125. Prefix : String; 126. True_Message : String; 127. False_Message: String) is 128. begin -- Postcondition 129. Assertion_Test (Condition, "POST", Prefix, True_Message, False_Message); 130. end Postcondition; 131. ----------------------------------------------------- 132. procedure Assertion (Condition : boolean; 133. Prefix : String; 134. True_Message : String; 135. False_Message: String) is 136. begin -- Assertion 137. Assertion_Test (Condition, "ASRT", Prefix, True_Message, False_Message); 138. end Assertion; 139. ----------------------------------------------------- 140. Procedure Beta_Mode is 141. begin -- Beta_Mode 142. Package_Mode := Beta; 143. end Beta_Mode; 144. ----------------------------------------------------- 145. Procedure Alpha_Mode is 146. begin -- Alpha_Mode 147. Package_Mode := Alpha; 148. end Alpha_Mode; 149. ----------------------------------------------------- 150. Procedure Silent_Mode (File_Name: string) is 151. begin -- Silent_Mode 152. if File_Name_Ptr = null then 153. --File_Name_Ptr := new string(string'length(File_Name)); 154. --File_Name_Ptr.all := File_Name; 155. File_Name_Ptr := new string'(File_Name); 156. end if; 157. end Silent_Mode; 158. ----------------------------------------------------- 159. Procedure Off is 160. begin -- Off 161. Main := off; 162. end Off; 163. ----------------------------------------------------- 164. Procedure On is 165. begin -- On 166. Main := on; 167. end On; 168. ----------------------------------------------------- 169. procedure Pause is 170. begin -- Pause 171. if File_Name_Ptr = null then 172. tio.Put (" to continue"); tio.Skip_Line; 173. end if; 174. end Pause; 175. 176. function A_For_All(Left, 177. Right: Univ_Range; 178. A : Array_Type) return boolean is 179. begin -- A_For_All 180. for i in left..Right loop 181. if not Condition (i, A) then 182. return false; 183. end if; 184. end loop; 185. return true; 186. end A_For_All; 187. 188. function A_There_Exists (Left, 189. Right: Univ_Range; 190. A : Array_Type ) return boolean is 191. begin -- A_There_Exists 192. for i in left..Right loop 193. if Condition (i, A) then 194. return true; 195. end if; 196. end loop; 197. return false; 198. end A_There_Exists; 199. 200. function R_For_All(Left, Right: Univ_Range) return boolean is 201. begin -- R_For_All 202. for i in left..Right loop 203. if not Condition (i) then 204. return false; 205. end if; 206. end loop; 207. return true; 208. end R_For_All; 209. 210. function R_There_Exists (Left, Right: Univ_Range) return boolean is 211. begin -- R_There_Exists 212. for i in left..Right loop 213. if Condition (i) then 214. return true; 215. end if; 216. end loop; 217. return false; 218. end R_There_Exists; 219. 220. function Key_Compare (Left, Right: Univ_Range; Key: Key_type; 221. A: Array_Type) return boolean is 222. begin -- Key_Compare 223. for i in Left..Right loop 224. if Condition (i, Key, A) then 225. return true; 226. end if; 227. end loop; 228. return false; 229. end Key_Compare; 230. 231. end Assert; 231 lines: No errors GNAT Compiler Version 3.01 Copyright 1995 Free Software Foundation, Inc. Compiling: qsort_assert_pak.ads (source file time stamp: 1996-03-16 02:46:30) No code generated for file qsort_assert_pak.ads (package spec) 1. with Assert; 2. package QSort_Assert_Pak is 3. 4. package ASRT renames Assert; 5. 6. type Int_Array is array (Natural range <>) of integer; 7. 8. 9. function Less (i: natural; Key: integer; A: Int_Array) return boolean; 10. function Greater (i : natural; Key: integer; A: Int_Array) return boolean; 11. function Ordered (i: natural; A: Int_Array) return boolean; 12. 13. ------------------------------------------------------- 14. -- returns A(i) < A(i+1) ? 15. ------------------------------------------------------- 16. 17. function For_All_Ordered is new ASRT.A_For_All 18. (Univ_Range => natural, 19. Array_Object => integer, 20. Array_Type => Int_Array, 21. Condition => Ordered); 22. ------------------------------------------------------- 23. -- For_All_Ordered is now an instance of the generic A_For_All 24. ------------------------------------------------------- 25. 26. 27. function Key_Compare_Less is new ASRT.Key_Compare 28. (Univ_Range => Natural, -- range of array 29. Array_Object => integer, -- array object 30. Key_Type => integer, -- key object 31. Array_Type => Int_Array,-- the array 32. Condition => Less); -- the loop assertion condition 33. ------------------------------------------------------- 34. -- Key_Compare_Less is now an instance of the generic Key_Compare 35. ------------------------------------------------------- 36. 37. function Key_Compare_Greater is new ASRT.Key_Compare 38. (Univ_Range => Natural, -- range of array 39. Array_Object => integer, -- array object 40. Key_Type => integer, -- key object 41. Array_Type => Int_Array,-- the array 42. Condition => Greater); -- the loop assertion condition 43. ------------------------------------------------------- 44. -- Key_Compare_Greater is now an instance of the generic Key_Compare 45. ------------------------------------------------------- 46. 47. end QSort_Assert_Pak; 47 lines: No errors GNAT Compiler Version 3.01 Copyright 1995 Free Software Foundation, Inc. Compiling: qsort_assert_pak.adb (source file time stamp: 1996-03-16 02:22:32) 1. package body QSort_Assert_Pak is 2. 3. function Ordered (i: natural; A: Int_Array) return boolean is 4. begin -- Ordered 5. return A(i) < A(i+1); 6. end Ordered; 7. 8. function Less(i: natural; Key: integer; A: Int_Array) 9. return boolean is 10. begin -- Less 11. return A(i) > Key ; 12. end Less; 13. 14. function Greater(i: natural; Key: integer; A: Int_Array) 15. return boolean is 16. begin -- Greater 17. return A(i) < Key ; 18. end Greater; 19. 20. end QSort_Assert_Pak; 20 lines: No errors GNAT Compiler Version 3.01 Copyright 1995 Free Software Foundation, Inc. Compiling: qsorting.adb (source file time stamp: 1996-03-17 03:20:28) 1. with QSort_Assert_Pak; use QSort_Assert_Pak; 2. with text_io; 3. 4. ------------------------------------------------------------------ 5. -- This procedure must be "with"ed with Random 6. ------------------------------------------------------------------ 7. procedure qsorting is 8. package tio renames text_io; 9. package iio is new text_io.integer_io(integer); 10. 11. function succ(i:integer) return integer renames integer'succ; 12. function pred(i:integer) return integer renames integer'pred; 13. 14. -- type Int_Array is array (Natural range <>) of integer; 15. A: Int_Array (1..500); 16. Count : natural; 17. Data_In: tio.File_Type; 18. First: natural; 19. Last: natural; 20. 21. 22. procedure Get_Data (A: in out Int_Array; Total: out natural) is 23. 24. Amount: constant natural := 40; 25. begin -- Get_Data 26. tio.Open (Data_In, tio.In_File, "random.dat"); 27. for i in 1..Amount loop 28. iio.Get (Data_In, A(i)); tio.Skip_Line (Data_In); 29. end loop; 30. Total := Amount; 31. tio.Close (Data_In); 32. end Get_Data; 33. 34. --------------------------------------------------------------- 35. 36. procedure Q_Sort (A: in out Int_Array) is 37. 38. Left, First : natural := A'first; 39. Right, Last : natural := A'last; 40. Key_Index : natural := 1; 41. Key : integer := 1; 42. 43. begin -- Q_Sort 44. 45. if Left < Right then 46. Key_Index := ((Right - Left)/2 )+ Left; -- select a random location 47. Key := A (Key_Index); -- Place the value in Key 48. A (Key_Index) := A (Left); -- Fill that position and vacate A(Left) 49. ------------------------------------------------------- 50. -- pre condition: Left < Right (and Array[Left..Right] in no particular 51. -- order.) 52. ------------------------------------------------------- 53. 54. ASRT.Precondition(left < right, 55. "Q_Sort - 1. main while loop Left < Right pre ", 56. " OK", 57. " Failed"); 58. ------------------------------------------------------ 59. 60. 61. While Left < Right loop 62. 63. ------------------------------------------------------ 64. -- Find a smaller number to the right 65. ------------------------------------------------------ 66. 67. 68. ------------------------------------------------------- 69. -- Pre Condition: everything to the right of key is > Key 70. ------------------------------------------------------- 71. -- sub-arrays A(Right+1) .. A'last > key 72. ------------------------------------------------------- 73. If Right /= Last then -- if right = last then nothing exists to the right 74. ASRT.PreCondition(Key_Compare_Less (Succ(Right), Last, Key, A), 75. "-- 2 first internal while loop pre", 76. " OK", 77. " Failed"); 78. End if; 79. 80. 81. While Left < Right and then Key < A (Right) loop 82. Right := Right - 1; 83. 84. 85. ------------------------------------------------------- 86. -- Invariant: Left <= Right AND Key < A(Succ(Right)) 87. ASRT.Invariant(Key_Compare_Less(Succ(Right), Last, Key, A), 88. "--- 2 first while loop invariant ", 89. " OK", 90. " Failed"); 91. ------------------------------------------------------- 92. 93. end loop; 94. 95. ------------------------------------------------------ 96. -- Post Condition: Left = Right OR Key >= A(Right) 97. -- ForAll i in A(A'first) to (A(Right)) 98. -- A(i) < Key; 99. ASRT.Postcondition(Left = Right OR Key >= A(Right), 100. "-- 2 first while Left=Right or Key > post ", 101. "OK", 102. "Failed"); 103. 104. -------------------------------------------------------- 105. 106. if Left /= Right then 107. 108. ------------------------------------------------------ 109. -- Move the smaller number to A(Left) 110. ------------------------------------------------------ 111. A (Left) := A (Right); 112. Left := Left + 1; 113. end if; 114. 115. ------------------------------------------------------ 116. -- Find a bigger number to the left 117. ------------------------------------------------------ 118. 119. 120. ------------------------------------------------------ 121. -- Pre: Left < Right CAND Key > A(Left) 122. -- ForAll i in A(A'first) to (A(Pred(Left))) 123. -- Key > A(i) ; 124. If First /= Left then -- if first=left then nothing exists to the left 125. ASRT.Precondition(Key_Compare_Greater (First, (Pred(Left)), Key, A), 126. "-- 3 second while Left < Right or Key > pre ", 127. "OK", 128. "Failed"); 129. end if; 130. 131. ------------------------------------------------------ 132. 133. 134. While Left < Right and then A (Left) < Key loop 135. 136. 137. Left := Left + 1; 138. ---------------------------------------------------- 139. -- Invariant: Left <= Right OR Key > Pred(A(Left)) 140. ASRT.Invariant(Key_Compare_Greater(First, Pred(Left), Key, A), 141. "--- 3 second while loop invariant ", 142. " OK", 143. " Failed"); 144. 145. ------------------------------------------------------ 146. end loop ; 147. 148. ------------------------------------------------------ 149. -- Post: Left = Right OR Key <= A(Left) 150. ASRT.Postcondition (Left=Right OR Key <= A(Left), 151. "-- 3 second while Left = Right or Key < post ", 152. "OK", 153. "Failed"); 154. ------------------------------------------------------ 155. 156. 157. if Left /= Right then 158. 159. --------------------------------------------------- 160. -- Move the larger number to A(Right) 161. --------------------------------------------------- 162. A (Right) := A (Left); 163. Right := Right - 1; 164. end if; 165. ----------------------------------------------------- 166. -- Invariant: Left <= Right 167. ASRT.Invariant (Left <= Right , 168. "Q_Sort - 1 main while invariant ", 169. "OK", 170. "Failed"); 171. 172. ----------------------------------------------------- 173. 174. end loop ; 175. 176. ------------------------------------------------------- 177. -- Post: Left = Right 178. ASRT.Postcondition(left = right, 179. "Q_Sort - 1 main while loop Left = Right post ", 180. " OK", 181. " Failed"); 182. ------------------------------------------------------- 183. 184. ------------------------------------------------------- 185. -- Since Left = Right, return the key to its final position 186. -- in the array 187. ------------------------------------------------------- 188. 189. A (Left) := Key; 190. 191. ------------------------------------------------------- 192. -- The following if structure forces the smaller of the 193. -- two pieces is recursively processed first to keep 194. -- the number of pending levels of recursion at a minimum 195. -- 196. -- It provides a sub-range of items within the array 197. -- that have yet to be sorted, anything outside that range 198. -- is assumed to be sorted 199. ------------------------------------------------------- 200. if (A'last - Left) < (Left - A'first) then 201. if A'first < Left then 202. Q_Sort ( A (A'first..Left-1) ) ; 203. end if ; 204. if Right < a'last then 205. Q_Sort (A (Right+1 .. A'Last) ) ; 206. end if ; 207. else 209. Q_Sort (A (Right+1 .. A'Last) ) ; 210. end if ; 211. if a'first < left then 212. Q_Sort ( A (A'first..Left-1) ) ; 213. end if ; 214. end if ; 215. end if ; 216. -- ASRT.PostCondition(For_All_Ordered (A'First, A'Last, A), 217. -- "Q_Sort - Complete", 218. -- " OK", 219. -- " Failed"); -- in [A'First, A'Last) 220. 221. end Q_Sort ; 222. 223. ------------------------------------------------------- 224. procedure Print_Data (A: in out Int_Array) is 225. Counter: natural := 0; 226. begin -- Print_Data 227. for i in A'First..A'Last loop 228. iio.Put (A(i), 7); 229. Counter := Counter + 1; 230. if (Counter mod 10) = 0 then 231. tio.New_Line; 232. end if; 233. end loop; 234. tio.New_Line; 235. end Print_Data; 236. ------------------------------------------------------- 237. begin -- qsorting 238. ASRT.Silent_Mode ("sorting.out"); 239. Get_Data (A, Count); 240. tio.Put ("Unsorted"); tio.New_Line; 241. Print_Data (A(1..Count)); 242. tio.put("got data"); 243. tio.New_Line(3); 244. Q_Sort (A(1..Count)); 245. tio.Put ("Sorted"); tio.New_Line; 246. Print_Data (A(1..Count)); 247. end qsorting; 247 lines: No errors ***** qsort runs without assertion testing ***** canary% c9x qsorting.adb canary% l9x qsorting canary% qsorting Unsorted 566 388 981 1060 -488 -2276 -1063 4538 -1489 755 -2511 -2134 -3384 4382 -4108 1046 -4683 -2141 4892 4822 3870 1188 2997 -1552 2273 -4888 1698 1926 527 -1112 250 -4746 -623 1770 -1347 -1566 -1922 -4753 -3093 2210 got data Sorted -4888 -4753 -4746 -4683 -4108 -3384 -3093 -2511 -2276 -2141 -2134 -1922 -1566 -1552 -1489 -1347 -1112 -1063 -623 -488 250 388 527 566 755 981 1046 1060 1188 1698 1770 1926 2210 2273 2997 3870 4382 4538 4822 4892 canary% ***** qsort runs with assertion testing ***** canary% c9x qsorting.adb canary% l9x qsorting canary% qsorting Unsorted 566 388 981 1060 -488 -2276 -1063 4538 -1489 755 -2511 -2134 -3384 4382 -4108 1046 -4683 -2141 4892 4822 3870 1188 2997 -1552 2273 -4888 1698 1926 527 -1112 250 -4746 -623 1770 -1347 -1566 -1922 -4753 -3093 2210 got data Sorted -4888 -4753 -4746 -4683 -4108 -3384 -3093 -2511 -2276 -2141 -2134 -1922 -1566 -1552 -1489 -1347 -1112 -1063 -623 -488 250 388 527 566 755 981 1046 1060 1188 1698 1770 1926 2210 2273 2997 3870 4382 4538 4822 4892 canary% canary%vi sorting.out 1996 mar 16 22:24:09 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:09 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:09 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:09 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:09 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:09 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:10 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:10 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:10 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:10 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:10 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:11 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:11 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:11 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:11 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:11 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:11 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:11 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:11 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:11 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:11 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:11 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:11 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:11 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:12 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:12 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:12 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:12 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:12 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:12 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:12 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:12 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:12 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:12 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:12 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:12 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:12 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:13 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:13 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:13 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:13 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:13 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:13 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:13 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:13 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:13 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:13 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:13 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:13 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:13 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:13 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:13 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:13 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:13 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:13 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:13 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:13 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:13 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:13 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:13 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:13 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:14 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:14 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:14 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:14 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:14 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:14 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:14 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:14 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:14 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:14 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:14 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:14 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:14 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:15 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:15 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:15 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:15 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:15 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:15 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:16 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:16 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:16 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:16 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:16 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:16 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:16 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:16 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:16 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:17 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:17 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:17 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:17 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:17 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:17 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:17 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:17 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:18 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:18 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:18 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:18 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:18 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:18 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:18 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:18 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:18 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:19 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:19 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:19 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:19 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:19 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:19 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:19 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:19 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:19 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:19 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:19 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:19 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:19 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:19 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:19 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:19 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:19 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:19 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:19 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:19 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:19 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:19 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:19 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:19 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:19 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:20 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:20 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:20 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:20 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:20 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:20 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:20 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:20 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:20 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:20 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:20 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:20 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:20 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:20 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:20 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:20 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:20 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:20 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:20 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:20 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:20 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:20 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:20 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:20 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:21 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:21 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:21 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:21 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:21 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:21 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:21 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:21 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:21 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:21 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:21 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:21 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:21 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:21 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:21 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:21 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:21 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:21 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:21 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:21 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:21 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:21 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:21 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:22 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:22 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:22 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:22 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:22 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:22 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:22 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:22 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:22 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:22 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:22 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:22 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:22 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:22 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:22 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:22 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:22 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:22 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:22 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:22 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:22 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:22 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:22 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:22 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:23 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:23 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:23 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:23 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:23 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:23 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:23 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:23 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:23 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:23 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:23 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:23 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:23 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:23 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:23 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:23 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:23 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:23 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:23 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:23 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:23 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:23 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:23 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:24 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:24 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:24 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:24 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:24 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:24 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:24 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:24 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:24 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:24 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:24 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:24 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:24 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:24 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:24 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:24 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:24 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:24 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:24 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:24 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:24 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:24 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:24 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:24 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:24 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:25 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:25 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:25 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:25 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:25 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:25 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:25 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:25 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:25 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:25 PRE :[T] -- 2 first internal while loop pre OK 1996 mar 16 22:24:25 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:25 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:25 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:25 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:25 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:25 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:25 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:25 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:25 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:25 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:25 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:25 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:25 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:26 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:26 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:26 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:26 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:26 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:26 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:26 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:26 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:26 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:26 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:26 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:26 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:26 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:26 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:26 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:26 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:26 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:26 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:26 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:26 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:26 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:26 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:26 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:26 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:27 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:27 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:27 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:27 INV :[T] --- 3 second while loop invariant OK 1996 mar 16 22:24:27 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:27 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:27 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:27 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:27 INV :[T] --- 2 first while loop invariant OK 1996 mar 16 22:24:27 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:27 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:27 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:27 POST:[T] Q_Sort - 1 main while loop Left = Right post OK 1996 mar 16 22:24:27 PRE :[T] Q_Sort - 1. main while loop Left < Right pre OK 1996 mar 16 22:24:27 POST:[T] -- 2 first while Left=Right or Key > post OK 1996 mar 16 22:24:27 PRE :[T] -- 3 second while Left < Right or Key > pre OK 1996 mar 16 22:24:27 POST:[T] -- 3 second while Left = Right or Key < post OK 1996 mar 16 22:24:27 INV :[T] Q_Sort - 1 main while invariant OK 1996 mar 16 22:24:27 POST:[T] Q_Sort - 1 main while loop Left = Right post OK