GNAT Compiler Version 3.03 Copyright 1995 Free Software Foundation, Inc. Compiling: ssorting.adb (source file time stamp: 1996-04-30 18:22:29) 1. ------------------------------------------------- 2. -- Maysa-Maria Peterson 3. -- SE 507 Formal Specifications 4. -- 5. -- April 29, 1996 6. -- Shell Sort Assertion Testing 7. ------------------------------------------------- 8. 9. with Sort_Assert_Pak; use Sort_Assert_Pak; 10. 11. with text_io; 12. 13. procedure ssorting is 14. 15. package tio renames text_io; 16. package iio is new text_io.integer_io(integer); 17. function succ(i:integer) return integer renames integer'succ; 18. function pred(i:integer) return integer renames integer'pred; 19. 20. A: Int_Array (1..500); 21. Count : natural; 22. Data_In: tio.File_Type; 23. 24. ---------------------------------------------------------- 25. procedure Get_Data (A: in out Int_Array; Total: out natural) is 26. Amount: constant natural := 40; 27. 28. begin -- Get_Data 29. 30. tio.Open (Data_In, tio.In_File, "random.dat"); 31. for i in 1..Amount loop 32. iio.Get (Data_In, A(i)); 33. tio.Skip_Line (Data_In); 34. end loop; 35. Total := Amount; 36. tio.Close (Data_In); 37. 38. end Get_Data; 39. ------------------------------------------------------- 40. 41. procedure S_Sort (A: in out Int_Array) is 42. Temp, Bub, Dist : integer ; 43. 44. begin 45. 46. --------------------------------------------------------- 47. -- Pre: Dist is 1/2 length of array segment 48. --------------------------------------------------------- 49. ASRT.Precondition(dist = A'last/2, | >>> warning: "dist" may be referenced before it has a value 50. " Shellsort -- While pre: Dist = A'Last/2", 51. " OK", 52. " Failed"); 53. --------------------------------------------------------- 54. 55. Dist := A'last / 2 ; 56. 57. while Dist > 0 loop 58. 59. --------------------------------------------------------- 60. -- Pre: Dist is larger than zero. 61. --------------------------------------------------------- 62. ASRT.Precondition(Dist > 0, 63. " Shellsort -- for index pre: Dist > 0", 64. " OK", 65. " Failed"); 66. --------------------------------------------------------- 67. 68. for Index in 1 .. A'last-Dist loop 69. Bub := Index ; 70. 71. --------------------------------------------------------- 72. -- Pre: array index within subarray length 73. --------------------------------------------------------- 74. ASRT.Precondition( (index in 1..a'last-dist), 75. " Shellsort -- Bub Pre", 76. " OK", 77. " Failed"); 78. --------------------------------------------------------- 79. 80. while (Bub > 0) and then A (Bub) > A (Bub+Dist) loop 81. Temp := A (Bub) ; 82. A (Bub) := A (Bub+Dist) ; 83. A (Bub+Dist) := Temp ; 84. 85. --------------------------------------------------------- 86. -- inv: whether or not a swap occurred, the comparison 87. -- variable to the left of the segment division 88. -- will be a value < that of the variable to the 89. -- right. 90. --------------------------------------------------------- 91. ASRT.Invariant(a(bub) < a(bub+dist), 92. "Shellsort -- Bub Inv: A(Bub) < A(Bub+Dist)", 93. "Ok", 94. "Failed"); 95. --------------------------------------------------------- 96. 97. Bub:= Bub - Dist ; 98. end loop ; 99. 100. --------------------------------------------------------- 101. -- post: after the swap, dist and index+dist in order 102. --------------------------------------------------------- 103. ASRT.Postcondition(All_Dist_Ordered(dist,a(1..bub+dist)), 104. " Shellsort - Bub Post", 105. "Ok", 106. "Failed"); 107. --------------------------------------------------------- 108. 109. --------------------------------------------------------- 110. -- inv: at completion of pass through loop dist and 111. -- dist + index will be in order. 112. --------------------------------------------------------- 113. ASRT.Invariant(All_Dist_Ordered(dist,a(1..bub+dist)), 114. " Shellsort -- For Index Inv", 115. " OK", 116. " Failed"); 117. --------------------------------------------------------- 118. 119. end loop ; 120. 121. --------------------------------------------------------- 122. -- post: at completion of pass through final loop dist and 123. -- dist + index will be in order. 124. --------------------------------------------------------- 125. ASRT.Postcondition(All_Dist_Ordered(dist,a(1..bub+dist)), 126. " Shellsort -- For Index Post", 127. " OK", 128. " Failed"); 129. --------------------------------------------------------- 130. 131. --------------------------------------------------------- 132. -- Inv: all in order 133. --------------------------------------------------------- 134. ASRT.Invariant(Dist_Ordered(dist,a), 135. " Shellsort - While Inv: Dist in order", 136. " OK", 137. " Failed"); 138. --------------------------------------------------------- 139. Dist := Dist / 2 ; 140. 141. end loop ; 142. 143. --------------------------------------------------------- 144. -- Post: all in order 145. --------------------------------------------------------- 146. ASRT.Postcondition(Dist_Ordered(dist,a), 147. " Shellsort -- Post: Complete", 148. " OK", 149. " Failed"); 150. --------------------------------------------------------- 151. 152. end S_Sort ; 153. 154. ------------------------------------------------------- 155. procedure Print_Data (A: in out Int_Array) is 156. Counter: natural := 0; 157. 158. begin -- Print_Data 159. 160. for i in A'First..A'Last loop 161. iio.Put (A(i), 7); 162. Counter := Counter + 1; 163. if (Counter mod 10) = 0 then 164. tio.New_Line; 165. end if; 166. 167. end loop; 168. 169. tio.New_Line; 170. end Print_Data; 171. ------------------------------------------------------- 172. 173. begin -- ssorting 174. 175. ASRT.Silent_Mode ("sorting.out"); 176. Get_Data (A, Count); 177. tio.Put ("Unsorted"); tio.New_Line; 178. Print_Data (A(1..Count)); 179. tio.put("got data"); 180. tio.New_Line(3); 181. S_Sort (A(1..Count)); 182. tio.Put ("Sorted"); tio.New_Line; 183. Print_Data (A(1..Count)); 184. 185. end ssorting; 186. 187. 188. 189. 190. 191. 191 lines: