{"id":252135,"date":"2015-03-01T17:02:02","date_gmt":"2015-03-01T13:02:02","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=252135"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=252135","title":{"rendered":"\u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u0430 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 Android, Java \u0438 Python"},"content":{"rendered":"

\u0422\u0438\u043c \u041f\u0435\u0442\u0435\u0440\u0441 \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043b \u0433\u0438\u0431\u0440\u0438\u0434\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 Timsort \u0432 2002 \u0433\u043e\u0434\u0443. \u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0438\u0441\u043a\u0443\u0441\u043d\u0443\u044e \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u044e \u0438\u0434\u0435\u0439 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u0441\u043b\u0438\u044f\u043d\u0438\u0435\u043c \u0438 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u0432\u0441\u0442\u0430\u0432\u043a\u0430\u043c\u0438 \u0438 \u0437\u0430\u0442\u043e\u0447\u0435\u043d \u043d\u0430 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u0443\u044e \u0440\u0430\u0431\u043e\u0442\u0443 \u0441 \u0440\u0435\u0430\u043b\u044c\u043d\u044b\u043c\u0438 \u0434\u0430\u043d\u043d\u044b\u043c\u0438. \u0412\u043f\u0435\u0440\u0432\u044b\u0435 Timsort \u0431\u044b\u043b \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d \u0434\u043b\u044f Python, \u043d\u043e \u0437\u0430\u0442\u0435\u043c \u0414\u0436\u043e\u0448\u0443\u0430 \u0411\u043b\u043e\u0445 (\u0441\u043e\u0437\u0434\u0430\u0442\u0435\u043b\u044c \u043a\u043e\u043b\u043b\u0435\u043a\u0446\u0438\u0439 Java, \u0438\u043c\u0435\u043d\u043d\u043e \u043e\u043d, \u043a\u0441\u0442\u0430\u0442\u0438, \u043e\u0442\u043c\u0435\u0442\u0438\u043b, \u0447\u0442\u043e \u0431\u043e\u043b\u044c\u0448\u0438\u043d\u0441\u0442\u0432\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 \u0434\u0432\u043e\u0438\u0447\u043d\u043e\u0433\u043e \u043f\u043e\u0438\u0441\u043a\u0430 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043e\u0448\u0438\u0431\u043a\u0443) \u043f\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043b \u0435\u0433\u043e \u043d\u0430 Java (\u043c\u0435\u0442\u043e\u0434\u044b java.util.Collections.sort \u0438 java.util.Arrays.sort). \u0421\u0435\u0433\u043e\u0434\u043d\u044f Timsort \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u044b\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u043c \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u0432 Android SDK, Oracle JDK \u0438 OpenJDK. \u0423\u0447\u0438\u0442\u044b\u0432\u0430\u044f \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u043e\u0441\u0442\u044c \u044d\u0442\u0438\u0445 \u043f\u043b\u0430\u0442\u0444\u043e\u0440\u043c, \u043c\u043e\u0436\u043d\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u0432\u044b\u0432\u043e\u0434, \u0447\u0442\u043e \u0441\u0447\u0451\u0442 \u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440\u043e\u0432, \u043e\u0431\u043b\u0430\u0447\u043d\u044b\u0445 \u0441\u0435\u0440\u0432\u0438\u0441\u043e\u0432 \u0438 \u043c\u043e\u0431\u0438\u043b\u044c\u043d\u044b\u0445 \u0443\u0441\u0442\u0440\u043e\u0439\u0441\u0442\u0432, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0449\u0438\u0445 Timsort \u0434\u043b\u044f \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438, \u0438\u0434\u0451\u0442 \u043d\u0430 \u043c\u0438\u043b\u043b\u0438\u0430\u0440\u0434\u044b.<\/p>\n

\u041d\u043e \u0432\u0435\u0440\u043d\u0451\u043c\u0441\u044f \u0432 2015-\u0439 \u0433\u043e\u0434. \u041f\u043e\u0441\u043b\u0435 \u0442\u043e\u0433\u043e \u043a\u0430\u043a \u043c\u044b \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043b\u0438 Java-\u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u043f\u043e\u0434\u0441\u0447\u0451\u0442\u043e\u043c \u0438 \u043f\u043e\u0440\u0430\u0437\u0440\u044f\u0434\u043d\u043e\u0439 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 (J. Autom. Reasoning 53(2), 129-139) \u043d\u0430\u0448\u0438\u043c \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u043e\u0434 \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u0435\u043c KeY, \u043c\u044b \u0438\u0441\u043a\u0430\u043b\u0438 \u043d\u043e\u0432\u044b\u0439 \u043e\u0431\u044a\u0435\u043a\u0442 \u0434\u043b\u044f \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f. Timsort \u043a\u0430\u0437\u0430\u043b\u0441\u044f \u043f\u043e\u0434\u0445\u043e\u0434\u044f\u0449\u0435\u0439 \u043a\u0430\u043d\u0434\u0438\u0434\u0430\u0442\u0443\u0440\u043e\u0439, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u043e\u043d \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u0441\u043b\u043e\u0436\u043d\u044b\u0439 \u0438 \u0448\u0438\u0440\u043e\u043a\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f. \u041a \u0441\u043e\u0436\u0430\u043b\u0435\u043d\u0438\u044e, \u043c\u044b \u043d\u0435 \u0441\u043c\u043e\u0433\u043b\u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u0435\u0433\u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c. \u041f\u0440\u0438\u0447\u0438\u043d\u0430 \u044d\u0442\u043e\u0433\u043e \u043f\u0440\u0438 \u0434\u0435\u0442\u0430\u043b\u044c\u043d\u043e\u043c \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0435\u043d\u0438\u0438 \u043e\u043a\u0430\u0437\u0430\u043b\u0430\u0441\u044c \u043f\u0440\u043e\u0441\u0442\u0430: \u0432 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 Timsort \u0435\u0441\u0442\u044c \u0431\u0430\u0433. \u041d\u0430\u0448\u0438 \u0442\u0435\u043e\u0440\u0435\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0438\u0441\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u043d\u0438\u044f \u0443\u043a\u0430\u0437\u0430\u043b\u0438 \u043d\u0430\u043c, \u0433\u0434\u0435 \u0438\u0441\u043a\u0430\u0442\u044c \u043e\u0448\u0438\u0431\u043a\u0443 (\u043b\u044e\u0431\u043e\u043f\u044b\u0442\u043d\u043e, \u0447\u0442\u043e \u043e\u0448\u0438\u0431\u043a\u0430 \u0431\u044b\u043b\u0430 \u0443\u0436\u0435 \u0432 \u043f\u0438\u0442\u043e\u043d\u043e\u0432\u0441\u043a\u043e\u0439 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438). \u0412 \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f, \u043a\u0430\u043a \u043c\u044b \u044d\u0442\u043e\u0433\u043e \u0434\u043e\u0431\u0438\u043b\u0438\u0441\u044c.<\/p>\n

\u0421\u0442\u0430\u0442\u044c\u044f \u0441 \u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u043b\u043d\u044b\u043c \u0430\u043d\u0430\u043b\u0438\u0437\u043e\u043c, \u0430 \u0442\u0430\u043a\u0436\u0435 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0442\u0435\u0441\u0442\u043e\u0432\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b \u043d\u0430 \u043d\u0430\u0448\u0435\u043c \u0441\u0430\u0439\u0442\u0435.<\/p>\n

\u0421\u043e\u0434\u0435\u0440\u0436\u0430\u043d\u0438\u0435
\n \u0411\u0430\u0433 \u0432 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 Timsort \u043d\u0430 Android, Java \u0438 Python
\n 1.1 \u0412\u043e\u0441\u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u043c \u0431\u0430\u0433 Timsort \u043d\u0430 Java
\n 1.2 \u041a\u0430\u043a \u0432 \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u0435 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 Timsort?
\n 1.3 \u0411\u0430\u0433 Timsort \u0448\u0430\u0433 \u0437\u0430 \u0448\u0430\u0433\u043e\u043c \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e (\u043d\u0435)\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 Timsort
\n 2.1 \u0421\u0438\u0441\u0442\u0435\u043c\u0430 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 KeY
\n 2.2 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0438 \u0435\u0433\u043e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f
\n 2.3 \u0410\u043d\u0430\u043b\u0438\u0437 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u043e\u0432 \u0440\u0430\u0431\u043e\u0442\u044b KeY \u041f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043d\u044b\u0435 \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u0431\u0430\u0433\u0430 \u043a \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f\u043c Timsort \u043d\u0430 Python \u0438 Android\/Java
\n 3.1 \u041d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f merge_collapse (Python)
\n 3.2 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f merge_collapse (Python)
\n 3.3 \u041d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f mergeCollapse (Java\/Android)
\n 3.4 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f mergeCollapse (Java\/Android) \u0417\u0430\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435: \u043a\u0430\u043a\u0438\u0435 \u0438\u0437 \u044d\u0442\u043e\u0433\u043e \u0441\u043b\u0435\u0434\u0443\u044e\u0442 \u0432\u044b\u0432\u043e\u0434\u044b?
\n 1. \u0411\u0430\u0433 \u0432 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 Timsort \u043d\u0430 Android, Java \u0438 Python
\n \u0422\u0430\u043a \u0432 \u0447\u0451\u043c \u0436\u0435 \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0431\u0430\u0433? \u0418 \u043f\u043e\u0447\u0435\u043c\u0443 \u0431\u044b \u0432\u0430\u043c \u043d\u0435 \u043f\u043e\u043f\u0440\u043e\u0431\u043e\u0432\u0430\u0442\u044c \u0432\u043e\u0441\u043f\u0440\u043e\u0438\u0437\u0432\u0435\u0441\u0442\u0438 \u0435\u0433\u043e \u0441\u0430\u043c\u0438\u043c?<\/p>\n

1.1 \u0412\u043e\u0441\u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u043c \u0431\u0430\u0433 Timsort \u043d\u0430 Java
\n git clone https:\/\/github.com\/abstools\/java-timsort-bug.git cd java-timsort-bug javac *.java java TestTimSort 67108864
\n \u0415\u0441\u043b\u0438 \u0431\u0430\u0433 \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442, \u0432\u044b \u0443\u0432\u0438\u0434\u0438\u0442\u0435 \u0442\u0430\u043a\u043e\u0439 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442
\n Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: 40 at java.util.TimSort.pushRun(TimSort.java:413) at java.util.TimSort.sort(TimSort.java:240) at java.util.Arrays.sort(Arrays.java:1438) at TestTimSort.main(TestTimSort.java:18)
\n \u0412\u0438\u0434\u0435\u043e\u0437\u0430\u043f\u0438\u0441\u044c \u0432\u043e\u0441\u043f\u0440\u043e\u0438\u0437\u0432\u0435\u0434\u0435\u043d\u0438\u044f \u043e\u0448\u0438\u0431\u043a\u0438<\/p>\n

1.2 \u041a\u0430\u043a \u0432 \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u0435 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 Timsort?
\n \u0422imsort \u2014 \u044d\u0442\u043e \u0433\u0438\u0431\u0440\u0438\u0434\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0443 \u0432\u0441\u0442\u0430\u0432\u043a\u043e\u0439 \u0438 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0443 \u0441\u043b\u0438\u044f\u043d\u0438\u0435\u043c.<\/p>\n

\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0435\u0440\u0435\u0443\u043f\u043e\u0440\u044f\u0434\u043e\u0447\u0438\u0432\u0430\u0435\u0442 \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432 \u0441\u043b\u0435\u0432\u0430 \u043d\u0430\u043f\u0440\u0430\u0432\u043e, \u043d\u0430\u0445\u043e\u0434\u044f \u0432 \u043d\u0451\u043c \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u0435 (\u043d\u0435\u043f\u0435\u0440\u0435\u043a\u0440\u044b\u0432\u0430\u044e\u0449\u0438\u0435\u0441\u044f) \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0435 \u0441\u0435\u0433\u043c\u0435\u043d\u0442\u044b (\u00ab\u0441\u0435\u0440\u0438\u0438\u00bb, \u0438\u043b\u0438 runs). \u0415\u0441\u043b\u0438 \u0441\u0435\u0440\u0438\u044f \u043a\u043e\u0440\u043e\u0447\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0451\u043d\u043d\u043e\u0439 \u043c\u0438\u043d\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0434\u043b\u0438\u043d\u044b, \u043e\u043d\u0430 \u0434\u043e\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c\u0438 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u0430\u043c\u0438 \u0438 \u0441\u043e\u0440\u0442\u0438\u0440\u0443\u0435\u0442\u0441\u044f \u0432\u0441\u0442\u0430\u0432\u043a\u043e\u0439. \u0414\u043b\u0438\u043d\u044b \u0441\u043e\u0437\u0434\u0430\u043d\u043d\u044b\u0445 \u0441\u0435\u0440\u0438\u0439 \u0434\u043e\u0431\u0430\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0432 \u043a\u043e\u043d\u0435\u0446 \u043c\u0430\u0441\u0441\u0438\u0432\u0430 runLen. \u041a\u043e\u0433\u0434\u0430 \u043d\u043e\u0432\u0430\u044f \u0441\u0435\u0440\u0438\u044f \u0434\u043e\u0431\u0430\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0432 runLen, \u043c\u0435\u0442\u043e\u0434 mergeCollapse \u0441\u043b\u0438\u0432\u0430\u0435\u0442 \u0441\u0435\u0440\u0438\u0438, \u043f\u043e\u043a\u0430 \u0442\u0440\u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u0430 \u0432 runLen \u043d\u0435 \u0431\u0443\u0434\u0443\u0442 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u0442\u044c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0439 \u043f\u0430\u0440\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u00ab\u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u043c\u00bb:<\/p>\n

runLen [n-2] > runLen [n-1] + runLen [n] runLen [n-1] > runLen [n]
\n \u0417\u0434\u0435\u0441\u044c n \u2014 \u044d\u0442\u043e \u0438\u043d\u0434\u0435\u043a\u0441 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0435\u0439 \u0441\u0435\u0440\u0438\u0438 \u0432 runLen. \u0418\u0434\u0435\u044f \u0431\u044b\u043b\u0430 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u044d\u0442\u043e\u0433\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0430 \u0434\u043b\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0442\u0440\u0451\u0445 \u0441\u0435\u0440\u0438\u0439 \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u0435\u0442, \u0447\u0442\u043e \u0432\u0441\u0435 \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u0442\u0440\u043e\u0439\u043a\u0438 \u0441\u0435\u0440\u0438\u0439 \u0431\u0443\u0434\u0443\u0442 \u0435\u043c\u0443 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u0442\u044c. \u0412 \u043a\u043e\u043d\u0446\u0435 \u0441\u043b\u0438\u0432\u0430\u044e\u0442\u0441\u044f \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438, \u0447\u0442\u043e \u0434\u0430\u0451\u0442 \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u043e\u0442\u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432.<\/p>\n

\u0418\u0437 \u0441\u043e\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u0439 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0441\u0442\u0438 \u0436\u0435\u043b\u0430\u0442\u0435\u043b\u044c\u043d\u043e \u0432\u044b\u0434\u0435\u043b\u0438\u0442\u044c \u043a\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u043c\u0435\u043d\u044c\u0448\u0435 \u043f\u0430\u043c\u044f\u0442\u0438 \u043f\u043e\u0434 runLen, \u043d\u043e \u0435\u0451 \u0434\u043e\u043b\u0436\u043d\u043e \u0431\u044b\u0442\u044c \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u0447\u0442\u043e\u0431\u044b \u0442\u0443\u0434\u0430 \u0437\u0430\u0432\u0435\u0434\u043e\u043c\u043e \u043f\u043e\u043c\u0435\u0441\u0442\u0438\u043b\u0438\u0441\u044c \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438. \u0415\u0441\u043b\u0438 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u0432\u0441\u0435\u0445 \u0441\u0435\u0440\u0438\u0439, \u0434\u043b\u0438\u043d\u0430 \u0441\u0435\u0440\u0438\u0439 \u0431\u0443\u0434\u0435\u0442 \u0440\u0430\u0441\u0442\u0438 \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e (\u0434\u0430\u0436\u0435 \u0431\u044b\u0441\u0442\u0440\u0435\u0435, \u0447\u0435\u043c \u0447\u0438\u0441\u043b\u0430 \u0424\u0438\u0431\u043e\u043d\u0430\u0447\u0447\u0438: \u0434\u043b\u0438\u043d\u0430 \u043a\u0430\u0436\u0434\u043e\u0439 \u0441\u0435\u0440\u0438\u0438 \u0441\u0442\u0440\u043e\u0433\u043e \u0431\u043e\u043b\u044c\u0448\u0435 \u0441\u0443\u043c\u043c\u044b \u0434\u043b\u0438\u043d \u0434\u0432\u0443\u0445 \u043f\u043e\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0445). \u0422\u0430\u043a \u043a\u0430\u043a \u0441\u0435\u0440\u0438\u0438 \u043d\u0435 \u043f\u0435\u0440\u0435\u043a\u0440\u044b\u0432\u0430\u044e\u0442\u0441\u044f, \u0438\u0445 \u043f\u043e\u0442\u0440\u0435\u0431\u0443\u0435\u0442\u0441\u044f \u043d\u0435 \u0442\u0430\u043a \u043c\u043d\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u043e\u0442\u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0434\u0430\u0436\u0435 \u043e\u0433\u0440\u043e\u043c\u043d\u044b\u0439 \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432.<\/p>\n

1.3 \u0411\u0430\u0433 Timsort \u0448\u0430\u0433 \u0437\u0430 \u0448\u0430\u0433\u043e\u043c
\n \u0418\u0437 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u0444\u0440\u0430\u0433\u043c\u0435\u043d\u0442\u0430 \u043a\u043e\u0434\u0430 \u0432\u0438\u0434\u043d\u043e, \u0447\u0442\u043e \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f mergeCollapse \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0434\u043b\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0442\u0440\u0451\u0445 \u0441\u0435\u0440\u0438\u0439 \u0432 runLen:
\n private void mergeCollapse() { while (stackSize > 1) { int n = stackSize — 2; if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) { if (runLen[n — 1] < runLen[n + 1]) n—; mergeAt(n); } else if (runLen[n] <= runLen[n + 1]) { mergeAt(n); } else { break; \/\/ \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d } } }
\n \u041a \u0441\u043e\u0436\u0430\u043b\u0435\u043d\u0438\u044e, \u044d\u0442\u043e\u0433\u043e \u043d\u0435 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u0447\u0442\u043e\u0431\u044b \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u043b\u0438 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443. \u041f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0438\u043c, \u0447\u0442\u043e runLen \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0442\u0430\u043a\u043e\u0439 \u043d\u0430\u0431\u043e\u0440 \u0434\u043b\u0438\u043d \u043f\u0435\u0440\u0435\u0434 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435\u043c mergeCollapse (n=4):
\n 120, 80, 25, 20, 30
\n \u041d\u0430 \u043f\u0435\u0440\u0432\u043e\u043c \u043f\u0440\u043e\u0445\u043e\u0434\u0435 \u0446\u0438\u043a\u043b\u0430 while \u0431\u0443\u0434\u0443\u0442 \u043e\u0431\u044a\u0435\u0434\u0438\u043d\u0435\u043d\u044b \u0441\u0435\u0440\u0438\u0438 \u0434\u043b\u0438\u043d\u043e\u0439 25 \u0438 20 (\u0442\u0430\u043a \u043a\u0430\u043a 25 < 20 + 30 \u0438 25 < 30):
\n 120, 80, 45, 30
\n \u041d\u0430 \u0432\u0442\u043e\u0440\u043e\u043c \u043f\u0440\u043e\u0445\u043e\u0434\u0435 \u0446\u0438\u043a\u043b\u0430 (\u0442\u0435\u043f\u0435\u0440\u044c n=3), \u043c\u044b \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u043c, \u0447\u0442\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d \u0434\u043b\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0442\u0440\u0451\u0445 \u0441\u0435\u0440\u0438\u0439, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e 80 > 45 + 30 \u0438 45 > 30, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 mergeCollapse \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u0442 \u0440\u0430\u0431\u043e\u0442\u0443. \u041d\u043e mergeCollapse \u043d\u0435 \u0432\u043e\u0441\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u043b \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0434\u043b\u044f \u0432\u0441\u0435\u0433\u043e \u043c\u0430\u0441\u0441\u0438\u0432\u0430: \u043e\u043d \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f \u0432 \u043f\u0435\u0440\u0432\u043e\u0439 \u0442\u0440\u043e\u0439\u043a\u0435, \u0442\u0430\u043a \u043a\u0430\u043a 120 < 80 + 45.<\/p>\n

\u0413\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440 \u0442\u0435\u0441\u0442\u043e\u0432 \u043d\u0430 \u043d\u0430\u0448\u0435\u043c \u0441\u0430\u0439\u0442\u0435 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0432\u044b\u044f\u0432\u0438\u0442\u044c \u044d\u0442\u0443 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0443. \u041e\u043d \u0441\u043e\u0437\u0434\u0430\u0451\u0442 \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432 \u0441 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e\u043c \u043a\u043e\u0440\u043e\u0442\u043a\u0438\u0445 \u0441\u0435\u0440\u0438\u0439, \u043f\u0440\u0438 \u044d\u0442\u043e\u043c \u0438\u0445 \u0434\u043b\u0438\u043d\u044b \u043d\u0435 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443, \u0447\u0442\u043e \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 \u043a \u043f\u0430\u0434\u0435\u043d\u0438\u044e Timsort. \u0418\u0441\u0442\u0438\u043d\u043d\u0430\u044f \u043f\u0440\u0438\u0447\u0438\u043d\u0430 \u043e\u0448\u0438\u0431\u043a\u0438 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0438\u0437-\u0437\u0430 \u043d\u0430\u0440\u0443\u0448\u0435\u043d\u0438\u044f \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0430 \u0434\u043b\u0438\u043d\u044b \u0441\u0435\u0440\u0438\u0439 \u0440\u0430\u0441\u0442\u0443\u0442 \u043c\u0435\u0434\u043b\u0435\u043d\u043d\u0435\u0435, \u0447\u0435\u043c \u043e\u0436\u0438\u0434\u0430\u043b\u043e\u0441\u044c, \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u0447\u0435\u0433\u043e \u0438\u0445 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u043f\u0440\u0435\u0432\u044b\u0448\u0430\u0435\u0442 runLen.length \u0438 \u044d\u0442\u043e \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 \u043a ArrayOutOfBoundsException.<\/p>\n

2. \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e (\u043d\u0435)\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 Timsort
\n \u041c\u044b \u043e\u0431\u043d\u0430\u0440\u0443\u0436\u0438\u043b\u0438, \u0447\u0442\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 mergeCollapse \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f, \u043a\u043e\u0433\u0434\u0430 \u043f\u044b\u0442\u0430\u043b\u0438\u0441\u044c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c Timsort. \u041a \u0441\u0447\u0430\u0441\u0442\u044c\u044e, \u043c\u044b \u0442\u0430\u043a\u0436\u0435 \u043f\u043e\u043d\u044f\u043b\u0438, \u043a\u0430\u043a \u0435\u0433\u043e \u0438\u0441\u043f\u0440\u0430\u0432\u0438\u0442\u044c. \u0412 \u0438\u0442\u043e\u0433\u0435 \u043d\u0430\u043c \u0434\u0430\u0436\u0435 \u0443\u0434\u0430\u043b\u043e\u0441\u044c \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0443\u044e \u0432\u0435\u0440\u0441\u0438\u044e, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0441\u043e\u0431\u043b\u044e\u0434\u0430\u0435\u0442\u0441\u044f. \u041d\u043e \u043d\u0435 \u0431\u0443\u0434\u0435\u043c \u0441\u043f\u0435\u0448\u0438\u0442\u044c. \u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u0440\u0430\u0437\u0431\u0435\u0440\u0451\u043c\u0441\u044f, \u0447\u0442\u043e \u0442\u0430\u043a\u043e\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438 \u043a\u0430\u043a \u043e\u043d\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f.<\/p>\n

2.1 \u0421\u0438\u0441\u0442\u0435\u043c\u0430 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 KeY
\n KeY \u2014 \u044d\u0442\u043e \u043f\u043b\u0430\u0442\u0444\u043e\u0440\u043c\u0430 \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043e\u0434\u043d\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043d\u0430 Java \u0438 JavaCard. \u041e\u043d\u0430 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043f\u043e \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438. \u0413\u0440\u0443\u0431\u043e \u0433\u043e\u0432\u043e\u0440\u044f, \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0441\u043e\u0441\u0442\u043e\u0438\u0442 \u0438\u0437 \u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u0439 (\u0432 \u0442\u0435\u0440\u043c\u0438\u043d\u0430\u0445 KeY \u2014 requires) \u0438 \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0439 (\u0432 \u0442\u0435\u0440\u043c\u0438\u043d\u0430\u0445 KeY \u2014 ensures). \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0437\u0430\u0434\u0430\u044e\u0442\u0441\u044f \u043f\u0435\u0440\u0435\u0434 \u043c\u0435\u0442\u043e\u0434\u0430\u043c\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0438\u0445 \u0440\u0435\u0430\u043b\u0438\u0437\u0443\u044e\u0442 (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u043f\u0435\u0440\u0435\u0434 \u0443\u043f\u043e\u043c\u044f\u043d\u0443\u0442\u044b\u043c \u0432\u044b\u0448\u0435 mergeCollapse()). \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043c\u0435\u0442\u043e\u0434\u0430 \u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u0435\u0433\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u043c.<\/p>\n

\u0412 \u0441\u043b\u0443\u0447\u0430\u0435 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u043f\u0440\u043e\u0441\u0442\u043e \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u0435\u0442, \u0447\u0442\u043e \u043d\u0430 \u0432\u0445\u043e\u0434 \u043f\u043e\u0434\u0430\u0451\u0442\u0441\u044f \u043d\u0435\u043f\u0443\u0441\u0442\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432, \u0430 \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u0442\u0440\u0435\u0431\u0443\u0435\u0442, \u0447\u0442\u043e\u0431\u044b \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0438\u0440\u0443\u044e\u0449\u0438\u0439 \u043c\u0430\u0441\u0441\u0438\u0432 \u0431\u044b\u043b \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043d \u0438 \u044f\u0432\u043b\u044f\u043b\u0441\u044f \u043f\u0435\u0440\u0435\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u043e\u0439 \u0432\u0445\u043e\u0434\u043d\u043e\u0433\u043e. \u0421\u0438\u0441\u0442\u0435\u043c\u0430 KeY \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u0432\u044b\u0437\u0432\u0430\u0442\u044c \u0441 \u0432\u0445\u043e\u0434\u043d\u044b\u043c\u0438 \u0434\u0430\u043d\u043d\u044b\u043c\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u044f\u043c, \u0442\u043e \u043c\u0435\u0442\u043e\u0434 \u0437\u0430\u0432\u0435\u0440\u0448\u0438\u0442\u0441\u044f \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0438 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0438\u0440\u0443\u044e\u0449\u0435\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0431\u0443\u0434\u0435\u0442 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u0442\u044c \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u044e. \u042d\u0442\u043e \u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u043f\u043e\u043b\u043d\u043e\u0439 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c\u044e, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u0438 \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0435 \u0437\u0430\u0432\u0435\u0440\u0448\u0435\u043d\u0438\u0435 \u043c\u0435\u0442\u043e\u0434\u0430. \u041a\u0430\u043a \u043c\u044b \u0443\u0432\u0438\u0434\u0435\u043b\u0438, \u043c\u0435\u0442\u043e\u0434 java.utils.Array.sort() \u0438\u0437 OpenJDK \u043d\u0435 \u0441\u043e\u0431\u043b\u044e\u0434\u0430\u0435\u0442 \u044d\u0442\u043e\u0442 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0434\u043b\u044f \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0451\u043d\u043d\u044b\u0445 \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u0434\u0430\u043d\u043d\u044b\u0445 \u043e\u043d \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u0442\u0441\u044f \u0438\u0441\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435\u043c.<\/p>\n

\u0414\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u043a\u043b\u0430\u0441\u0441\u043e\u0432 \u0438 \u043e\u0431\u044a\u0435\u043a\u0442\u043e\u0432, \u0447\u0442\u043e\u0431\u044b \u0443\u043a\u0430\u0437\u0430\u0442\u044c \u043e\u0431\u0449\u0438\u0435 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u044f \u043d\u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u043f\u043e\u043b\u0435\u0439. \u041e\u0431\u044b\u0447\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442\u0441\u044f \u0441\u043e\u0433\u043b\u0430\u0441\u043e\u0432\u0430\u043d\u043d\u043e\u0441\u0442\u044c \u0434\u0430\u043d\u043d\u044b\u0445 \u0438\u043b\u0438 \u0433\u0440\u0430\u043d\u0438\u0447\u043d\u044b\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u044f:
\n \/*@ private invariant @ runBase.length == runLen.length && runBase != runLen; @*\/
\n \u042d\u0442\u043e\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0433\u043e\u0432\u043e\u0440\u0438\u0442, \u0447\u0442\u043e \u0434\u043b\u0438\u043d\u044b \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432 runBase \u0438 runLen \u0434\u043e\u043b\u0436\u043d\u044b \u0441\u043e\u0432\u043f\u0430\u0434\u0430\u0442\u044c, \u043d\u043e \u0432 \u0442\u043e \u0436\u0435 \u0432\u0440\u0435\u043c\u044f \u044d\u0442\u043e \u0434\u043e\u043b\u0436\u043d\u044b \u0431\u044b\u0442\u044c \u0434\u0432\u0430 \u0440\u0430\u0437\u043d\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u0430. \u0421\u0435\u043c\u0430\u043d\u0442\u0438\u043a\u0430 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u0432 \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u0435\u0442, \u0447\u0442\u043e \u043a\u0430\u0436\u0434\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u043d\u0430 \u0432\u044b\u0445\u043e\u0434\u0435 \u0434\u043e\u043b\u0436\u0435\u043d \u043d\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u0442\u044c \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u044f \u0441\u0432\u043e\u0435\u0433\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430, \u043d\u043e \u0438 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u0435\u0433\u043e \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0433\u043e \u043e\u0431\u044a\u0435\u043a\u0442\u0430 \u201cthis\u201d.<\/p>\n

\u0412 \u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u044f\u0437\u044b\u043a\u0430 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0439 KeY \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442 Java Modeling Language (JML). \u0412\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u043d\u0430 \u043d\u0451\u043c \u043f\u0438\u0448\u0443\u0442\u0441\u044f \u043a\u0430\u043a \u043d\u0430 \u043e\u0431\u044b\u0447\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 Java, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 Java-\u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0441\u0442\u044b \u0435\u0433\u043e \u043b\u0435\u0433\u043a\u043e \u043e\u0441\u0432\u043e\u044f\u0442. \u0413\u043b\u0430\u0432\u043d\u043e\u0435 \u0440\u0430\u0441\u0448\u0438\u0440\u0435\u043d\u0438\u0435 JML \u2014 \u044d\u0442\u043e \u043a\u0432\u0430\u043d\u0442\u043e\u0440\u044b (\\forall T x \u2014 \u0434\u043b\u044f \u043b\u044e\u0431\u043e\u0433\u043e T, \\exists T x \u2014 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 T) \u0438, \u043a\u043e\u043d\u0435\u0447\u043d\u043e, \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u0435 \u043a\u043b\u044e\u0447\u0435\u0432\u044b\u0435 \u0441\u043b\u043e\u0432\u0430 \u0434\u043b\u044f \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 JML \u043f\u0440\u0438\u0432\u043e\u0434\u044f\u0442\u0441\u044f \u0432 \u043a\u043e\u043c\u043c\u0435\u043d\u0442\u0430\u0440\u0438\u044f\u0445 java-\u0444\u0430\u0439\u043b\u043e\u0432 \u043f\u0435\u0440\u0435\u0434 \u043a\u043e\u0434\u043e\u043c, \u043a \u043a\u043e\u0442\u043e\u0440\u043e\u043c\u0443 \u043e\u043d\u0438 \u043e\u0442\u043d\u043e\u0441\u044f\u0442\u0441\u044f. \u041d\u0438\u0436\u0435 \u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u043f\u0440\u0438\u043c\u0435\u0440 Java-\u043c\u0435\u0442\u043e\u0434\u0430 \u0441 JML-\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0435\u0439:<\/p>\n

\/*@ private normal_behavior @ requires @ n >= MIN_MERGE; @ ensures @ \\result >= MIN_MERGE\/2; @*\/ private static int \/*@ pure @*\/ minRunLength(int n) { assert n >= 0; int r = 0; \/\/ \u0421\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u0441\u044f 1 \u0435\u0441\u043b\u0438 \u0445\u043e\u0442\u044f \u0431\u044b \u043e\u0434\u0438\u043d \u0435\u0434\u0438\u043d\u0438\u0447\u043d\u044b\u0439 \u0431\u0438\u0442 \u0431\u044b\u043b \u0443\u0434\u0430\u043b\u0451\u043d \u0441\u0434\u0432\u0438\u0433\u043e\u043c \/*@ loop_invariant n >= MIN_MERGE\/2 && r >=0 && r<=1; @ decreases n; @ assignable \\nothing; @*\/ while (n >= MIN_MERGE) { r |= (n & 1); n >>= 1; } return n + r; }
\n \u041a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 minRunLength() \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043e\u0434\u043d\u043e \u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u0435: \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440 \u0434\u043e\u043b\u0436\u0435\u043d \u0431\u044b\u0442\u044c \u043d\u0435 \u043c\u0435\u043d\u044c\u0448\u0435, \u0447\u0435\u043c MIN_MERGE. \u0412 \u044d\u0442\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 (\u0438 \u0442\u043e\u043b\u044c\u043a\u043e \u0432 \u044d\u0442\u043e\u043c) \u043c\u0435\u0442\u043e\u0434 \u043e\u0431\u0435\u0449\u0430\u0435\u0442 \u0437\u0430\u0432\u0435\u0440\u0448\u0438\u0442\u044c\u0441\u044f \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e (\u043d\u0435 \u0437\u0430\u0446\u0438\u043a\u043b\u0438\u0442\u044c\u0441\u044f \u0438 \u043d\u0435 \u0432\u044b\u0431\u0440\u043e\u0441\u0438\u0442\u044c \u0438\u0441\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435) \u0438 \u0432\u0435\u0440\u043d\u0443\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0431\u043e\u043b\u044c\u0448\u0435 \u0438\u043b\u0438 \u0440\u0430\u0432\u043d\u043e MIN_MERGE\/2. \u0414\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u043c\u0435\u0442\u043e\u0434 \u043f\u043e\u043c\u0435\u0447\u0435\u043d \u043a\u0430\u043a pure (\u0447\u0438\u0441\u0442\u044b\u0439). \u042d\u0442\u043e \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u043c\u0435\u0442\u043e\u0434 \u043d\u0435 \u043c\u043e\u0434\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u0442 \u043a\u0443\u0447\u0443.<\/p>\n

\u041a\u043b\u044e\u0447\u0435\u0432\u043e\u0439 \u043c\u043e\u043c\u0435\u043d\u0442 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0441\u0438\u0441\u0442\u0435\u043c\u0430 KeY \u0441\u043f\u043e\u0441\u043e\u0431\u043d\u0430 \u0441\u0442\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u044b \u043f\u043e\u0434\u043e\u0431\u043d\u044b\u0445 \u043c\u0435\u0442\u043e\u0434\u043e\u0432 \u0434\u043b\u044f \u043b\u044e\u0431\u044b\u0445 \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u043e\u0432. \u041a\u0430\u043a \u044d\u0442\u043e \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e? KeY \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442 \u0441\u0438\u043c\u0432\u043e\u043b\u044c\u043d\u043e\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430, \u0442\u043e \u0435\u0441\u0442\u044c, \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442 \u0435\u0433\u043e, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u0441\u0438\u043c\u0432\u043e\u043b\u044c\u043d\u044b\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f, \u0442\u0430\u043a \u0447\u0442\u043e \u0443\u0447\u0438\u0442\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u0432\u0441\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0435 \u043f\u0443\u0442\u0438 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f. \u041d\u043e \u044d\u0442\u043e\u0433\u043e \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0441\u0438\u043c\u0432\u043e\u043b\u044c\u043d\u043e\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0446\u0438\u043a\u043b\u043e\u0432 \u0441 \u043d\u0435\u0444\u0438\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u043c \u0447\u0438\u0441\u043b\u043e\u043c \u0438\u0442\u0435\u0440\u0430\u0446\u0438\u0439 (\u0442\u0430\u043a\u0438\u0445 \u043a\u0430\u043a \u0446\u0438\u043a\u043b \u0432 mergeCollapse(), \u0433\u0434\u0435 \u043c\u044b \u043d\u0435 \u0437\u043d\u0430\u0435\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 stackSize) \u043d\u0438\u043a\u043e\u0433\u0434\u0430 \u043d\u0435 \u0437\u0430\u0432\u0435\u0440\u0448\u0438\u0442\u0441\u044f. \u0427\u0442\u043e\u0431\u044b \u0441\u0438\u043c\u0432\u043e\u043b\u044c\u043d\u043e\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0446\u0438\u043a\u043b\u043e\u0432 \u0441\u0442\u0430\u043b\u043e \u043a\u043e\u043d\u0435\u0447\u043d\u044b\u043c, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043b\u043e\u0433\u0438\u043a\u0430 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u0432. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0432\u044b\u0448\u0435\u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d\u043d\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 minRunLength() \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0446\u0438\u043a\u043b, \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0430 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u043c \u0446\u0438\u043a\u043b\u0430. \u0418\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u0435\u0442, \u0447\u0442\u043e \u043f\u043e\u0441\u043b\u0435 \u043a\u0430\u0436\u0434\u043e\u0439 \u0438\u0442\u0435\u0440\u0430\u0446\u0438\u0438 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u0443\u0441\u043b\u043e\u0432\u0438\u0435 n >= MIN_MERGE\/2 && r >= 0 && r <= 1, \u0438 \u0438\u0437 \u044d\u0442\u043e\u0433\u043e \u043c\u043e\u0436\u043d\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u0432\u0441\u0435\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430. \u0410\u043d\u043d\u043e\u0442\u0430\u0446\u0438\u044f decreases (\u0443\u043c\u0435\u043d\u044c\u0448\u0430\u0435\u0442\u0441\u044f) \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f, \u0447\u0442\u043e\u0431\u044b \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u0437\u0430\u0432\u0435\u0440\u0448\u0435\u043d\u0438\u0435 \u0446\u0438\u043a\u043b\u0430. \u0412 \u043d\u0435\u0439 \u0443\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0435, \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u043d\u0435\u043e\u0442\u0440\u0438\u0446\u0430\u0442\u0435\u043b\u044c\u043d\u043e \u0438 \u0441\u0442\u0440\u043e\u0433\u043e \u0443\u043c\u0435\u043d\u044c\u0448\u0430\u0435\u0442\u0441\u044f. \u041a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f assignable \u043f\u0435\u0440\u0435\u0447\u0438\u0441\u043b\u044f\u0435\u0442 \u043e\u0431\u044a\u0435\u043a\u0442\u044b \u043a\u0443\u0447\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u0438\u0437\u043c\u0435\u043d\u0435\u043d\u044b \u0432 \u0446\u0438\u043a\u043b\u0435. \u041a\u043b\u044e\u0447\u0435\u0432\u043e\u0435 \u0441\u043b\u043e\u0432\u043e \\nothing \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u043a\u0443\u0447\u0430 \u043d\u0435 \u043c\u043e\u0434\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u0442\u0441\u044f. \u0418 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e: \u0446\u0438\u043a\u043b \u0438\u0437\u043c\u0435\u043d\u044f\u0435\u0442 \u0442\u043e\u043b\u044c\u043a\u043e \u043b\u043e\u043a\u0430\u043b\u044c\u043d\u0443\u044e \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0443\u044e r \u0438 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442 n.<\/p>\n

\u0412 \u043e\u0431\u0449\u0435\u043c, \u0434\u043b\u044f \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u043c\u0435\u0442\u043e\u0434\u043e\u0432. \u041d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0442\u0430\u043a\u0436\u0435 \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442\u044c \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u0446\u0438\u043a\u043b\u043e\u0432. \u0418\u043d\u043e\u0433\u0434\u0430 \u043e\u0447\u0435\u043d\u044c \u043d\u0435\u043f\u0440\u043e\u0441\u0442\u043e \u043f\u0440\u0438\u0434\u0443\u043c\u0430\u0442\u044c \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0441\u043e\u0431\u043b\u044e\u0434\u0430\u0435\u0442\u0441\u044f \u0432 \u0446\u0438\u043a\u043b\u0435 \u0438 \u043f\u0440\u0438 \u044d\u0442\u043e\u043c \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0441\u0438\u043b\u0451\u043d, \u0447\u0442\u043e\u0431\u044b \u0438\u0437 \u043d\u0435\u0433\u043e \u0432\u044b\u0432\u0435\u0441\u0442\u0438 \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u043c\u0435\u0442\u043e\u0434\u0430. \u0411\u0435\u0437 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u0430\u043b\u044c\u043d\u043e\u0439 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u043a\u0438 \u0438 \u0442\u0435\u0445\u043d\u043e\u043b\u043e\u0433\u0438\u0438 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c \u0432\u0440\u044f\u0434 \u043b\u0438 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e \u0441\u043e\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u044b\u0435 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u0446\u0438\u043a\u043b\u043e\u0432 \u0432 \u043d\u0435\u0442\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0430\u0445. \u041d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435 \u0438\u043c\u0435\u043d\u043d\u043e \u0437\u0434\u0435\u0441\u044c \u0438 \u043a\u0440\u043e\u0435\u0442\u0441\u044f \u043e\u0448\u0438\u0431\u043a\u0430 \u0441\u043e\u0437\u0434\u0430\u0442\u0435\u043b\u0435\u0439 Timsort. \u041f\u0440\u0438 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0451\u043d\u043d\u044b\u0445 \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u0445 \u0446\u0438\u043a\u043b \u0432 mergeCollapse \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u043a\u043b\u0430\u0441\u0441\u0430 Timsort (\u0441\u043c\u043e\u0442\u0440\u0438\u0442\u0435 \u0440\u0430\u0437\u0434\u0435\u043b 1.3 \u0411\u0430\u0433 Timsort \u0448\u0430\u0433 \u0437\u0430 \u0448\u0430\u0433\u043e\u043c):<\/p>\n

\/*@ private invariant @ (\\forall int i; 0<=i && i<stackSize-4; @ runLen[i] > runLen[i+1] + runLen[i+2])) @*\/
\n \u042d\u0442\u043e\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u0435\u0442, \u0447\u0442\u043e runLen[i] \u0434\u043e\u043b\u0436\u043d\u043e \u0431\u044b\u0442\u044c \u0431\u043e\u043b\u044c\u0448\u0435, \u0447\u0435\u043c \u0441\u0443\u043c\u043c\u0430 \u0434\u0432\u0443\u0445 \u043f\u043e\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0445 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u0432, \u0434\u043b\u044f \u043b\u044e\u0431\u044b\u0445 \u043d\u0435\u043e\u0442\u0440\u0438\u0446\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u0445 i, \u043c\u0435\u043d\u044c\u0448\u0438\u0445 stackSize-4. \u0418\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u043d\u0435 \u0432\u043e\u0441\u0441\u0442\u0430\u043d\u0430\u0432\u043b\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u0438 \u043f\u043e\u0441\u043b\u0435 \u0446\u0438\u043a\u043b\u0430, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0432\u0435\u0441\u044c \u043c\u0435\u0442\u043e\u0434 mergeCollapse \u043d\u0435 \u0441\u043e\u0445\u0440\u0430\u043d\u044f\u0435\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u043a\u043b\u0430\u0441\u0441\u0430. \u0421\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e, \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0446\u0438\u043a\u043b\u0430 \u043d\u0435 \u0442\u0430\u043a\u043e\u0439 \u0441\u0442\u0440\u043e\u0433\u0438\u0439, \u043a\u0430\u043a \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u043b\u0438 \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a\u0438. \u042d\u0442\u043e \u043c\u044b \u0438 \u043e\u0431\u043d\u0430\u0440\u0443\u0436\u0438\u043b\u0438 \u0432 \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u0435 \u043d\u0430\u0448\u0435\u0439 \u043f\u043e\u043f\u044b\u0442\u043a\u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c Timsort \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e KeY. \u0411\u0435\u0437 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u0430 \u043e\u0431\u043d\u0430\u0440\u0443\u0436\u0438\u0442\u044c \u044d\u0442\u043e \u0431\u044b\u043b\u043e \u0431\u044b \u043f\u043e\u0447\u0442\u0438 \u043d\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e.<\/p>\n

\u0425\u043e\u0442\u044f JML \u0438 \u043e\u0447\u0435\u043d\u044c \u043f\u043e\u0445\u043e\u0436 \u043d\u0430 Java, \u044d\u0442\u043e \u043f\u043e\u043b\u043d\u043e\u0446\u0435\u043d\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u043f\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0443, \u043f\u043e\u0434\u0445\u043e\u0434\u044f\u0449\u0438\u0439 \u0434\u043b\u044f \u043f\u043e\u043b\u043d\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 Java-\u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c.<\/p>\n

2.2 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0438 \u0435\u0433\u043e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f
\n \u0423\u043f\u0440\u043e\u0449\u0451\u043d\u043d\u0430\u044f \u0432\u0435\u0440\u0441\u0438\u044f \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043f\u043e \u0437\u0430\u0434\u0443\u043c\u043a\u0435 \u0430\u0432\u0442\u043e\u0440\u043e\u0432 \u0434\u043e\u043b\u0436\u0435\u043d \u0441\u043e\u0431\u043b\u044e\u0434\u0430\u0442\u044c\u0441\u044f \u0432 mergeCollapse, \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u043d\u0430 \u043d\u0438\u0436\u0435.
\n \/*@ requires @ stackSize > 0 && @ runLen[stackSize-4] > runLen[stackSize-3]+runLen[stackSize-2] @ && runLen[stackSize-3] > runLen[stackSize-2]; @ ensures @ (\\forall int i; 0<=i && i<stackSize-2; @ runLen[i] > runLen[i+1] + runLen[i+2]) @ && runLen[stackSize-2] > runLen[stackSize-1] @*\/ private void mergeCollapse()
\n \u0414\u0432\u0435 \u0444\u043e\u0440\u043c\u0443\u043b\u044b \u0432 ensures \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u044e\u0442, \u0447\u0442\u043e \u043a\u043e\u0433\u0434\u0430 mergeCollapse \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u0442\u0441\u044f, \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443, \u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d\u043d\u043e\u043c\u0443 \u0432 \u0440\u0430\u0437\u0434\u0435\u043b\u0435 1.2. \u041c\u044b \u0443\u0436\u0435 \u0432\u0438\u0434\u0435\u043b\u0438, \u0447\u0442\u043e \u044d\u0442\u043e\u0442 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 \u043d\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u0432 \u0442\u0435\u043a\u0443\u0449\u0435\u0439 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 mergeCollapse (\u0440\u0430\u0437\u0434\u0435\u043b 1.3). \u0422\u0435\u043f\u0435\u0440\u044c \u043c\u044b \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u043c \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0443\u044e \u0432\u0435\u0440\u0441\u0438\u044e, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0441\u043e\u0431\u043b\u044e\u0434\u0430\u0435\u0442 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442:<\/p>\n

private void newMergeCollapse() { while (stackSize > 1) { int n = stackSize — 2; if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1] || n-1 > 0 && runLen[n-2] <= runLen[n] + runLen[n-1]) { if (runLen[n — 1] < runLen[n + 1]) n—; } else if (n<0 || runLen[n] > runLen[n + 1]) { break; \/\/ \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d } mergeAt(n); } }
\n \u041e\u0441\u043d\u043e\u0432\u043d\u0430\u044f \u0438\u0434\u0435\u044f \u044d\u0442\u043e\u0439 \u0432\u0435\u0440\u0441\u0438\u0438 \u2014 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0442\u044c, \u0447\u0442\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0441\u043e\u0431\u043b\u044e\u0434\u0430\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u0447\u0435\u0442\u044b\u0440\u0451\u0445 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0441\u0435\u0440\u0438\u0439 \u0432 runLen \u0432\u043c\u0435\u0441\u0442\u043e \u0442\u0440\u0451\u0445. \u041a\u0430\u043a \u043c\u044b \u0443\u0432\u0438\u0434\u0438\u043c \u043d\u0438\u0436\u0435, \u044d\u0442\u043e\u0433\u043e \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u0447\u0442\u043e\u0431\u044b \u0434\u043b\u0438\u043d\u044b \u0432\u0441\u0435\u0445 \u0441\u0435\u0440\u0438\u0439 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u043b\u0438 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443 \u043f\u043e\u0441\u043b\u0435 \u0437\u0430\u0432\u0435\u0440\u0448\u0435\u043d\u0438\u044f mergeCollapse.<\/p>\n

\u041f\u0435\u0440\u0432\u044b\u0439 \u0448\u0430\u0433 \u0432 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0435 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0434\u043b\u044f \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u043e\u0439 \u0432\u0435\u0440\u0441\u0438\u0438 mergeCollapse \u2014 \u044d\u0442\u043e \u043d\u0430\u0439\u0442\u0438 \u043f\u043e\u0434\u0445\u043e\u0434\u044f\u0449\u0438\u0439 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0446\u0438\u043a\u043b\u0430. \u0412\u043e\u0442 \u0435\u0433\u043e \u0443\u043f\u0440\u043e\u0449\u0451\u043d\u043d\u0430\u044f \u0432\u0435\u0440\u0441\u0438\u044f:<\/p>\n

\/*@ loop_invariant @ (\\forall int i; 0<=i && i<stackSize-4; @ runLen[i] > runLen[i+1] + runLen[i+2]) @ && runLen[stackSize-4] > runLen[stackSize-3]) @*\/
\n \u0418\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0446\u0438\u043a\u043b\u0430 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u0435\u0442, \u0447\u0442\u043e \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438 \u043a\u0440\u043e\u043c\u0435, \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e, \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0447\u0435\u0442\u044b\u0440\u0451\u0445, \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u0443\u0441\u043b\u043e\u0432\u0438\u044e. \u041f\u0440\u0438 \u044d\u0442\u043e\u043c \u0437\u0430\u043c\u0435\u0442\u0438\u043c, \u0447\u0442\u043e \u0446\u0438\u043a\u043b \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u0442\u0441\u044f (\u043f\u043e \u043e\u043f\u0435\u0440\u0430\u0442\u043e\u0440\u0443 break), \u0442\u043e\u043b\u044c\u043a\u043e \u0435\u0441\u043b\u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0435 \u0447\u0435\u0442\u044b\u0440\u0435 \u0441\u0435\u0440\u0438\u0438 \u0442\u043e\u0436\u0435 \u0435\u043c\u0443 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442. \u0422\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c, \u043c\u043e\u0436\u043d\u043e \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c, \u0447\u0442\u043e \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443.<\/p>\n

2.3 \u0410\u043d\u0430\u043b\u0438\u0437 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u043e\u0432 \u0440\u0430\u0431\u043e\u0442\u044b KeY
\n \u041a\u043e\u0433\u0434\u0430 \u043c\u044b \u043f\u043e\u0434\u0430\u0451\u043c \u043d\u0430 \u0432\u0445\u043e\u0434 KeY \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0443\u044e \u0432\u0435\u0440\u0441\u0438\u044e mergeCollapse \u0432\u043c\u0435\u0441\u0442\u0435 \u0441 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u043c \u0438 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u043c \u0446\u0438\u043a\u043b\u0430, \u0441\u0438\u0441\u0442\u0435\u043c\u0430 \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442 \u0441\u0438\u043c\u0432\u043e\u043b\u044c\u043d\u043e\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0446\u0438\u043a\u043b\u0430 \u0438 \u0433\u0435\u043d\u0435\u0440\u0438\u0440\u0443\u0435\u0442 \u0443\u0441\u043b\u043e\u0432\u0438\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438: \u0444\u043e\u0440\u043c\u0443\u043b\u044b, \u0438\u0437 \u0438\u0441\u0442\u0438\u043d\u043d\u043e\u0441\u0442\u0438 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0441\u043b\u0435\u0434\u0443\u0435\u0442, \u0447\u0442\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 mergeCollapse \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f. \u0421\u043b\u0435\u0434\u0443\u044e\u0449\u0430\u044f (\u0443\u043f\u0440\u043e\u0449\u0451\u043d\u043d\u0430\u044f) \u0444\u043e\u0440\u043c\u0443\u043b\u0430 \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442 \u0433\u043b\u0430\u0432\u043d\u043e\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 mergeCollapse, \u0441\u0433\u0435\u043d\u0435\u0440\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0435 KeY:<\/p>\n

\u0424\u043e\u0440\u043c\u0443\u043b\u0430 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u0435\u0442, \u0447\u0442\u043e \u0438\u0437 \u0443\u0441\u043b\u043e\u0432\u0438\u0439 \u0432 \u0441\u043a\u043e\u0431\u043a\u0430\u0445, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0438\u0441\u0442\u0438\u043d\u043d\u044b \u043f\u043e\u0441\u043b\u0435 \u0437\u0430\u0432\u0435\u0440\u0448\u0435\u043d\u0438\u044f \u0446\u0438\u043a\u043b\u0430, \u0434\u043e\u043b\u0436\u043d\u043e \u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u044c \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0435 mergeCollapse. \u041f\u043e\u043d\u044f\u0442\u043d\u043e, \u043e\u0442\u043a\u0443\u0434\u0430 \u0432\u0437\u044f\u043b\u0438\u0441\u044c \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u0432 \u0441\u043a\u043e\u0431\u043a\u0430\u0445: \u043e\u043f\u0435\u0440\u0430\u0442\u043e\u0440 break, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u0442 \u0446\u0438\u043a\u043b, \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u0442\u043e\u043b\u044c\u043a\u043e \u043a\u043e\u0433\u0434\u0430 \u043e\u043d\u0438 \u0432\u0441\u0435 \u0438\u0441\u0442\u0438\u043d\u043d\u044b. \u041c\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u043b\u0438 \u044d\u0442\u0443 \u0444\u043e\u0440\u043c\u0443\u043b\u0443 (\u0438 \u0432\u0441\u0435 \u043f\u0440\u043e\u0447\u0438\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438) \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e KeY \u0432 \u043f\u043e\u043b\u0443\u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u043c \u0440\u0435\u0436\u0438\u043c\u0435. \u041d\u0438\u0436\u0435 \u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d \u043d\u0430\u0431\u0440\u043e\u0441\u043e\u043a \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430:<\/p>\n

\u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e. \u0424\u043e\u0440\u043c\u0443\u043b\u0430 runLen[stackSize-2] > runLen[stackSize-1] \u0438\u0437 \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u044f mergeCollapse \u043f\u0440\u044f\u043c\u043e \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0438\u0437 n >= 0 ==> runLen[n] > runLen[n+1].<\/p>\n

\u0414\u043e\u043a\u0430\u0436\u0435\u043c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0443\u044e \u0444\u043e\u0440\u043c\u0443\u043b\u0443:<\/p>\n

\\forall int i; 0<=i && i<stackSize-2; runLen[i] > runLen[i+1] + runLen[i+2].<\/p>\n

\u0412\u043e\u0437\u043c\u043e\u0436\u043d\u044b \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0435 \u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f i:<\/p>\n

i < stackSize-4: \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443 \u0446\u0438\u043a\u043b\u0430 i = stackSize-4: \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0438\u0437 n>1 ==> runLen[n-2] > runLen[n-1] + runLen[n] i = stackSize-3: \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u0438\u0437 n>0 ==> runLen[n-1] > runLen[n] + runLen[n+1]
\n \u042d\u0442\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442, \u0447\u0442\u043e \u043d\u043e\u0432\u0430\u044f \u0432\u0435\u0440\u0441\u0438\u044f mergeCollapse \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u0442\u0441\u044f \u0442\u043e\u043b\u044c\u043a\u043e \u043a\u043e\u0433\u0434\u0430 \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443.<\/p>\n

3. \u041f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043d\u044b\u0435 \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u0431\u0430\u0433\u0430 \u043a \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f\u043c Timsort \u043d\u0430 Python \u0438 Android\/Java
\n \u041d\u0430\u0448 \u0430\u043d\u0430\u043b\u0438\u0437 \u043e\u0448\u0438\u0431\u043a\u0438 (\u0432\u043a\u043b\u044e\u0447\u0430\u044f \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 mergeCollapse) \u0431\u044b\u043b \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u0435\u043d, \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0435\u043d \u0438 \u043f\u0440\u0438\u043d\u044f\u0442 \u0432 \u0431\u0430\u0433\u0442\u0440\u0435\u043a\u0435\u0440 Java.<\/p>\n

\u0411\u0430\u0433 \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u043a\u0430\u043a \u043c\u0438\u043d\u0438\u043c\u0443\u043c \u0432 \u0432\u0435\u0440\u0441\u0438\u0438 Java \u0434\u043b\u044f Android, OpenJDK \u0438 OracleJDK: \u0432\u043e \u0432\u0441\u0435\u0445 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u0439 \u043a\u043e\u0434 Timsort. \u0422\u0430\u043a\u0436\u0435 \u0431\u0430\u0433 \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0432 Python. \u0412 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0445 \u0440\u0430\u0437\u0434\u0435\u043b\u0430\u0445 \u043f\u0440\u0438\u0432\u043e\u0434\u044f\u0442\u0441\u044f \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b\u044c\u043d\u0430\u044f \u0438 \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0430\u044f \u0432\u0435\u0440\u0441\u0438\u0438.<\/p>\n

\u041a\u0430\u043a \u0431\u044b\u043b\u043e \u0441\u043a\u0430\u0437\u0430\u043d\u043e \u0432\u044b\u0448\u0435, \u0438\u0434\u0435\u044f \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u043e\u0447\u0435\u043d\u044c \u043f\u0440\u043e\u0441\u0442\u0430: \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0442\u044c, \u0447\u0442\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0447\u0435\u0442\u044b\u0440\u0451\u0445 \u0441\u0435\u0440\u0438\u0439 \u0432 runLen, \u0430 \u043d\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u0434\u043b\u044f \u0442\u0440\u0451\u0445.<\/p>\n

3.1 \u041d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f merge_collapse (Python)
\n Timsort \u0434\u043b\u044f Python (\u043d\u0430\u043f\u0438\u0441\u0430\u043d \u043d\u0430 C \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c Python API) \u0434\u043e\u0441\u0442\u0443\u043f\u0435\u043d \u0432 \u0440\u0435\u043f\u043e\u0437\u0438\u0442\u043e\u0440\u0438\u0438 subversion \u2013 \u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0442\u0430\u043a\u0436\u0435 \u043e\u043f\u0438\u0441\u0430\u043d \u0437\u0434\u0435\u0441\u044c.<\/p>\n

\u0412\u0435\u0440\u0441\u0438\u044f Timsort \u0434\u043b\u044f Java \u0431\u044b\u043b\u0430 \u043f\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0430 \u0441 CPython. \u0412\u0435\u0440\u0441\u0438\u044f \u043d\u0430 CPython \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043e\u0448\u0438\u0431\u043a\u0443, \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d\u043d\u0430\u044f \u0434\u043b\u044f \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u043a\u0438 \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432 \u0432\u043f\u043b\u043e\u0442\u044c \u0434\u043e 264 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u0432, \u0442\u0430\u043a\u0436\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043e\u0448\u0438\u0431\u043a\u0443. \u041e\u0434\u043d\u0430\u043a\u043e \u043d\u0430 \u0441\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u043c\u0430\u0448\u0438\u043d\u0430\u0445 \u0432\u044b\u0437\u0432\u0430\u0442\u044c \u043e\u0448\u0438\u0431\u043a\u0443 \u043f\u0435\u0440\u0435\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u043c\u0430\u0441\u0441\u0438\u0432\u0430 \u043d\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e: \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0432\u044b\u0434\u0435\u043b\u044f\u0435\u0442 85 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u0432 \u0434\u043b\u044f runLen, \u0438 \u044d\u0442\u043e\u0433\u043e \u0445\u0432\u0430\u0442\u0430\u0435\u0442 (\u043a\u0430\u043a \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442 \u043d\u0430\u0448 \u0430\u043d\u0430\u043b\u0438\u0437 \u0432 \u043f\u043e\u043b\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435) \u0434\u043b\u044f \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432, \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u0449\u0438\u0445 \u043d\u0435 \u0431\u043e\u043b\u0435\u0435 249 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u0432. \u0414\u043b\u044f \u0441\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044f, \u043c\u043e\u0449\u043d\u0435\u0439\u0448\u0438\u0439 \u043d\u0430 \u0441\u0435\u0433\u043e\u0434\u043d\u044f\u0448\u043d\u0438\u0439 \u0434\u0435\u043d\u044c \u0441\u0443\u043f\u0435\u0440\u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440 Tianhe-2 \u043e\u0431\u043b\u0430\u0434\u0430\u0435\u0442 250 \u0431\u0430\u0439\u0442\u0430\u043c\u0438 \u043f\u0430\u043c\u044f\u0442\u0438.<\/p>\n

\/* The maximum number of entries in a MergeState’s * pending-runs stack. * This is enough to sort arrays of size up to about * 32 * phi ** MAX_MERGE_PENDING * where phi ~= 1.618. 85 is ridiculously large enough, * good for an array with 2**64 elements. *\/ #define MAX_MERGE_PENDING 85 merge_collapse(MergeState *ms) { struct s_slice *p = ms->pending; assert(ms); while (ms->n > 1) { Py_ssize_t n = ms->n — 2; if (n > 0 && p[n-1].len <= p[n].len + p[n+1].len) { if (p[n-1].len < p[n+1].len) —n; if (merge_at(ms, n) < 0) return -1; } else if (p[n].len <= p[n+1].len) { if (merge_at(ms, n) < 0) return -1; } else break; } return 0; }
\n 3.2 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f merge_collapse (Python)
\n merge_collapse(MergeState *ms) { struct s_slice *p = ms->pending; assert(ms); while (ms->n > 1) { Py_ssize_t n = ms->n — 2; if ( n > 0 && p[n-1].len <= p[n].len + p[n+1].len || (n-1 > 0 && p[n-2].len <= p[n].len + p[n-1].len)) { if (p[n-1].len < p[n+1].len) —n; if (merge_at(ms, n) < 0) return -1; } else if (p[n].len <= p[n+1].len) { if (merge_at(ms, n) < 0) return -1; } else break; } return 0; }
\n 3.3 \u041d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f mergeCollapse (Java\/Android)
\n \u041e\u0448\u0438\u0431\u043a\u0430 \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u0430\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u0430 \u043e\u0448\u0438\u0431\u043a\u0435 \u0432 Python:
\n private void mergeCollapse() { while (stackSize > 1) { int n = stackSize — 2; if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) { if (runLen[n — 1] < runLen[n + 1]) n—; mergeAt(n); } else if (runLen[n] <= runLen[n + 1]) { mergeAt(n); } else { break; \/\/ \u0418\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d } } }
\n 3.4 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f mergeCollapse (Java\/Android)
\n \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0430\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u043e \u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d\u043d\u043e\u043c\u0443 \u0432\u044b\u0448\u0435 \u0434\u043b\u044f Python.
\n [UPDATE 26\/2: \u043c\u044b \u0438\u0437\u043c\u0435\u043d\u0438\u043b\u0438 \u043a\u043e\u0434 \u043f\u043e \u0441\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044e \u0441 \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0439 \u0432\u0435\u0440\u0441\u0438\u0435\u0439 \u0441\u0442\u0430\u0442\u044c\u0438. \u0421\u0442\u0430\u0440\u044b\u0439 \u043a\u043e\u0434 \u0431\u044b\u043b \u044d\u043a\u0432\u0438\u0432\u0430\u043b\u0435\u043d\u0442\u0435\u043d, \u043d\u043e \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u043b \u0438\u0437\u0431\u044b\u0442\u043e\u0447\u043d\u0443\u044e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0443 \u0438 \u043e\u0442\u043b\u0438\u0447\u0430\u043b\u0441\u044f \u043f\u043e \u0441\u0442\u0438\u043b\u044e. \u0421\u043f\u0430\u0441\u0438\u0431\u043e \u0432\u0441\u0435\u043c, \u043a\u0442\u043e \u043e\u0431\u0440\u0430\u0442\u0438\u043b \u0432\u043d\u0438\u043c\u0430\u043d\u0438\u0435!]
\n private void newMergeCollapse() { while (stackSize > 1) { int n = stackSize — 2; if ( (n >= 1 && runLen[n-1] <= runLen[n] + runLen[n+1]) || (n >= 2 && runLen[n-2] <= runLen[n] + runLen[n-1])) { if (runLen[n — 1] < runLen[n + 1]) n—; } else if (runLen[n] > runLen[n + 1]) { break; \/\/ \u0418\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d } mergeAt(n); } }
\n 4. \u0417\u0430\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435: \u043a\u0430\u043a\u0438\u0435 \u0438\u0437 \u044d\u0442\u043e\u0433\u043e \u0441\u043b\u0435\u0434\u0443\u044e\u0442 \u0432\u044b\u0432\u043e\u0434\u044b?
\n \u041f\u0440\u0438 \u043f\u043e\u043f\u044b\u0442\u043a\u0435 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c Timsort \u043d\u0430\u043c \u043d\u0435 \u0443\u0434\u0430\u043b\u043e\u0441\u044c \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u044c \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u043e\u0431\u044a\u0435\u043a\u0442\u0430 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438. \u0410\u043d\u0430\u043b\u0438\u0437\u0438\u0440\u0443\u044f \u043f\u0440\u0438\u0447\u0438\u043d\u044b \u043d\u0435\u0443\u0434\u0430\u0447\u0438, \u043c\u044b \u043e\u0431\u043d\u0430\u0440\u0443\u0436\u0438\u043b\u0438 \u0432 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 Timsort \u043e\u0448\u0438\u0431\u043a\u0443, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 \u043a ArrayOutOfBoundsException \u0434\u043b\u044f \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0451\u043d\u043d\u044b\u0445 \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u0434\u0430\u043d\u043d\u044b\u0445. \u041c\u044b \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0438\u043b\u0438 \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u043e\u0448\u0438\u0431\u043e\u0447\u043d\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430 (\u0431\u0435\u0437 \u043e\u0449\u0443\u0442\u0438\u043c\u043e\u0433\u043e \u0441\u043d\u0438\u0436\u0435\u043d\u0438\u044f \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438) \u0438 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u043b\u0438, \u0447\u0442\u043e \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e \u0438 \u043e\u0448\u0438\u0431\u043a\u0438 \u0431\u043e\u043b\u044c\u0448\u0435 \u043d\u0435\u0442.<\/p>\n

\u0418\u0437 \u044d\u0442\u043e\u0439 \u0438\u0441\u0442\u043e\u0440\u0438\u0438, \u043f\u043e\u043c\u0438\u043c\u043e \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u043e \u043d\u0430\u0439\u0434\u0435\u043d\u043d\u043e\u0439 \u043e\u0448\u0438\u0431\u043a\u0438, \u043c\u043e\u0436\u043d\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u043d\u0430\u0431\u043b\u044e\u0434\u0435\u043d\u0438\u0439.
\n \u0417\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0441\u0442\u044b \u0441\u0447\u0438\u0442\u0430\u044e\u0442 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0435 \u043c\u0435\u0442\u043e\u0434\u044b \u043d\u0435\u043f\u0440\u0430\u043a\u0442\u0438\u0447\u043d\u044b\u043c\u0438 \u0438\/\u0438\u043b\u0438 \u0434\u0430\u043b\u0451\u043a\u0438\u043c\u0438 \u043e\u0442 \u0440\u0435\u0430\u043b\u044c\u043d\u044b\u0445 \u0437\u0430\u0434\u0430\u0447. \u042d\u0442\u043e \u043d\u0435 \u0442\u0430\u043a: \u043c\u044b \u043d\u0430\u0448\u043b\u0438 \u0438 \u0438\u0441\u043f\u0440\u0430\u0432\u0438\u043b\u0438 \u043e\u0448\u0438\u0431\u043a\u0443 \u0432 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u043d\u043e\u043c \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0435\u043d\u0438\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u043c \u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u043c\u0438\u043b\u043b\u0438\u0430\u0440\u0434\u044b \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0435\u0439 \u043a\u0430\u0436\u0434\u044b\u0439 \u0434\u0435\u043d\u044c. \u041a\u0430\u043a \u043f\u043e\u043a\u0430\u0437\u0430\u043b \u043d\u0430\u0448 \u0430\u043d\u0430\u043b\u0438\u0437, \u043d\u0430\u0439\u0442\u0438 \u0438 \u0438\u0441\u043f\u0440\u0430\u0432\u0438\u0442\u044c \u0442\u0430\u043a\u043e\u0439 \u0431\u0430\u0433 \u0431\u0435\u0437 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0430\u043d\u0430\u043b\u0438\u0437\u0430 \u0438 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u0430 \u0434\u043b\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0431\u044b\u043b\u043e \u0431\u044b \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u043d\u0435\u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e. \u041e\u0448\u0438\u0431\u043a\u0430 \u0434\u043e\u043b\u0433\u0438\u0435 \u0433\u043e\u0434\u044b \u0436\u0438\u043b\u0430 \u0432 \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u043e\u0439 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 \u044f\u0437\u044b\u043a\u043e\u0432 Java \u0438 Python. \u0415\u0451 \u043f\u0440\u043e\u044f\u0432\u043b\u0435\u043d\u0438\u044f \u0437\u0430\u043c\u0435\u0447\u0430\u043b\u0438 \u0440\u0430\u043d\u0435\u0435 \u0438 \u0434\u0430\u0436\u0435 \u0434\u0443\u043c\u0430\u043b\u0438, \u0447\u0442\u043e \u0438\u0441\u043f\u0440\u0430\u0432\u0438\u043b\u0438, \u043d\u043e \u0432 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0434\u043e\u0431\u0438\u043b\u0438\u0441\u044c \u0442\u043e\u043b\u044c\u043a\u043e \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043e\u0448\u0438\u0431\u043a\u0430 \u0441\u0442\u0430\u043b\u0430 \u0432\u043e\u0437\u043d\u0438\u043a\u0430\u0442\u044c \u0440\u0435\u0436\u0435. \u0425\u043e\u0442\u044f \u043c\u0430\u043b\u043e\u0432\u0435\u0440\u043e\u044f\u0442\u043d\u043e, \u0447\u0442\u043e \u0442\u0430\u043a\u0430\u044f \u043e\u0448\u0438\u0431\u043a\u0430 \u0432\u043e\u0437\u043d\u0438\u043a\u043d\u0435\u0442 \u0441\u043b\u0443\u0447\u0430\u0439\u043d\u043e, \u043b\u0435\u0433\u043a\u043e \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u0442\u044c, \u043a\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u0435\u0451 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0434\u043b\u044f \u0430\u0442\u0430\u043a\u0438. \u0412\u0435\u0440\u043e\u044f\u0442\u043d\u043e, \u0432 \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u044b\u0445 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430\u0445 \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u044b\u0445 \u044f\u0437\u044b\u043a\u043e\u0432 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u043a\u0440\u043e\u044e\u0442\u0441\u044f \u0438 \u0434\u0440\u0443\u0433\u0438\u0435 \u043d\u0435\u0437\u0430\u043c\u0435\u0447\u0435\u043d\u043d\u044b\u0435 \u043e\u0448\u0438\u0431\u043a\u0438. \u041c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c, \u0441\u0442\u043e\u0438\u0442 \u0437\u0430\u043d\u044f\u0442\u044c\u0441\u044f \u0438\u0445 \u043f\u043e\u0438\u0441\u043a\u043e\u043c \u0434\u043e \u0442\u043e\u0433\u043e \u043a\u0430\u043a \u043e\u043d\u0438 \u043f\u0440\u0438\u0447\u0438\u043d\u044f\u0442 \u0432\u0440\u0435\u0434 \u0438\u043b\u0438 \u0431\u0443\u0434\u0443\u0442 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u044b \u0437\u043b\u043e\u0443\u043c\u044b\u0448\u043b\u0435\u043d\u043d\u0438\u043a\u0430\u043c\u0438? \u0420\u0435\u0430\u043a\u0446\u0438\u044f \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a\u043e\u0432 Java \u043d\u0430 \u043d\u0430\u0448 \u043e\u0442\u0447\u0451\u0442 \u0432 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u043c \u0441\u043c\u044b\u0441\u043b\u0435 \u0440\u0430\u0437\u043e\u0447\u0430\u0440\u043e\u0432\u044b\u0432\u0430\u0435\u0442. \u0412\u043c\u0435\u0441\u0442\u043e \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u043d\u0430\u0448\u0443 \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0443\u044e (\u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u0443\u044e!) \u0432\u0435\u0440\u0441\u0438\u044e mergeCollapse(), \u043e\u043d\u0438 \u043f\u0440\u0435\u0434\u043f\u043e\u0447\u043b\u0438 \u0443\u0432\u0435\u043b\u0438\u0447\u0438\u0442\u044c \u0432\u044b\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0439 \u0440\u0430\u0437\u043c\u0435\u0440 runLen \u0434\u043e \u00ab\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0433\u043e\u00bb \u0440\u0430\u0437\u043c\u0435\u0440\u0430. \u041a\u0430\u043a \u043c\u044b \u043f\u043e\u043a\u0430\u0437\u0430\u043b\u0438, \u0432\u043e\u0432\u0441\u0435 \u043d\u0435 \u043e\u0431\u044f\u0437\u0430\u0442\u0435\u043b\u044c\u043d\u043e \u0431\u044b\u043b\u043e \u0442\u0430\u043a \u0434\u0435\u043b\u0430\u0442\u044c. \u041d\u043e \u0442\u0435\u043f\u0435\u0440\u044c \u043a\u0430\u0436\u0434\u044b\u0439, \u043a\u0442\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442 java.utils.Collection.sort() \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u043d\u0443\u0436\u0434\u0435\u043d \u0442\u0440\u0430\u0442\u0438\u0442\u044c \u0431\u043e\u043b\u044c\u0448\u0435 \u043f\u0430\u043c\u044f\u0442\u0438. \u0423\u0447\u0438\u0442\u044b\u0432\u0430\u044f \u0430\u0441\u0442\u0440\u043e\u043d\u043e\u043c\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u0447\u0438\u0441\u043b\u043e \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0449\u0438\u0445 \u043d\u0430\u0441\u0442\u043e\u043b\u044c\u043a\u043e \u0431\u0430\u0437\u043e\u0432\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e, \u044d\u0442\u043e \u043f\u0440\u0438\u0432\u0435\u0434\u0451\u0442 \u043a \u0437\u0430\u043c\u0435\u0442\u043d\u044b\u043c \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u043c \u0437\u0430\u0442\u0440\u0430\u0442\u0430\u043c \u044d\u043d\u0435\u0440\u0433\u0438\u0438. \u041c\u044b \u043c\u043e\u0436\u0435\u043c \u0442\u043e\u043b\u044c\u043a\u043e \u0434\u043e\u0433\u0430\u0434\u044b\u0432\u0430\u0442\u044c\u0441\u044f, \u043f\u043e\u0447\u0435\u043c\u0443 \u043d\u0435 \u0431\u044b\u043b\u043e \u043f\u0440\u0438\u043d\u044f\u0442\u043e \u043d\u0430\u0448\u0435 \u0440\u0435\u0448\u0435\u043d\u0438\u0435: \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a\u0438 JDK \u043d\u0435 \u0443\u0434\u043e\u0441\u0443\u0436\u0438\u043b\u0438\u0441\u044c \u043f\u0440\u043e\u0447\u0438\u0442\u0430\u0442\u044c \u043d\u0430\u0448 \u043e\u0442\u0447\u0451\u0442 \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u0438 \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043d\u0435 \u043f\u043e\u043d\u044f\u043b\u0438 \u0441\u0443\u0442\u044c \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u0438 \u0440\u0435\u0448\u0438\u043b\u0438 \u043d\u0435 \u043f\u043e\u043b\u0430\u0433\u0430\u0442\u044c\u0441\u044f \u043d\u0430 \u043d\u0435\u0433\u043e. \u0412 \u043a\u043e\u043d\u0446\u0435 \u043a\u043e\u043d\u0446\u043e\u0432, OpenJDK \u0440\u0430\u0437\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u0435\u0442 \u0441\u043e\u043e\u0431\u0449\u0435\u0441\u0442\u0432\u043e, \u0432 \u0437\u043d\u0430\u0447\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u0442\u0435\u043f\u0435\u043d\u0438 \u0441\u043e\u0441\u0442\u043e\u044f\u0449\u0435\u0435 \u0438\u0437 \u0434\u043e\u0431\u0440\u043e\u0432\u043e\u043b\u044c\u0446\u0435\u0432, \u0443 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043d\u0435 \u0442\u0430\u043a \u043c\u043d\u043e\u0433\u043e \u0432\u0440\u0435\u043c\u0435\u043d\u0438. <\/p>\n

\u041a\u0430\u043a\u0438\u0435 \u0438\u0437 \u044d\u0442\u043e\u0433\u043e \u0441\u043b\u0435\u0434\u0443\u044e\u0442 \u0432\u044b\u0432\u043e\u0434\u044b? \u041c\u044b \u0431\u044b\u043b\u0438 \u0431\u044b \u0441\u0447\u0430\u0441\u0442\u043b\u0438\u0432\u044b, \u0435\u0441\u043b\u0438 \u0431\u044b \u043d\u0430\u0448\u0430 \u0440\u0430\u0431\u043e\u0442\u0430 \u043f\u043e\u0441\u043b\u0443\u0436\u0438\u043b\u0430 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0439 \u0442\u043e\u0447\u043a\u043e\u0439 \u0434\u043b\u044f \u0431\u043e\u043b\u0435\u0435 \u0442\u0435\u0441\u043d\u043e\u0433\u043e \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u043c\u0435\u0436\u0434\u0443 \u0438\u0441\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044f\u043c\u0438 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0445 \u043c\u0435\u0442\u043e\u0434\u043e\u0432 \u0438 \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a\u0430\u043c\u0438 \u043e\u0442\u043a\u0440\u044b\u0442\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u043d\u044b\u0445 \u043f\u043b\u0430\u0442\u0444\u043e\u0440\u043c. \u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0435 \u043c\u0435\u0442\u043e\u0434\u044b \u0443\u0436\u0435 \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u044e\u0442\u0441\u044f \u0432 Amazon \u0438 Facebook. \u0421\u043e\u0432\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u044f\u0437\u044b\u043a\u0438 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0438 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043d\u0435 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0442\u0430\u043a\u0438\u043c\u0438 \u0443\u0436 \u0437\u0430\u043f\u0443\u0442\u0430\u043d\u043d\u044b\u043c\u0438 \u0438 \u0441\u0443\u043f\u0435\u0440\u0441\u043b\u043e\u0436\u043d\u044b\u043c\u0438 \u0432 \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u0438. \u041f\u043e\u0441\u0442\u043e\u044f\u043d\u043d\u043e \u0443\u043b\u0443\u0447\u0448\u0430\u0435\u0442\u0441\u044f \u0438\u0445 \u044e\u0437\u0430\u0431\u0438\u043b\u0438\u0442\u0438 \u0438 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0437\u0430\u0446\u0438\u044f. \u041d\u043e \u043d\u0430\u043c \u043d\u0443\u0436\u043d\u043e \u0431\u043e\u043b\u044c\u0448\u0435 \u043b\u044e\u0434\u0435\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0431\u044b \u043f\u0440\u043e\u0431\u043e\u0432\u0430\u043b\u0438, \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043b\u0438 \u0438 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043b\u0438 \u043d\u0430\u0448\u0438 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b. \u0414\u0430, \u043f\u043e\u0442\u0440\u0435\u0431\u0443\u044e\u0442\u0441\u044f \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0443\u0441\u0438\u043b\u0438\u044f, \u0447\u0442\u043e\u0431\u044b \u043d\u0430\u0447\u0430\u0442\u044c \u043f\u0438\u0441\u0430\u0442\u044c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0435 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043a\u043e\u0434, \u043d\u043e \u044d\u0442\u043e \u043d\u0435 \u0441\u043b\u043e\u0436\u043d\u0435\u0435, \u0447\u0435\u043c, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0440\u0430\u0437\u043e\u0431\u0440\u0430\u0442\u044c\u0441\u044f, \u043a\u0430\u043a \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440 \u0438\u043b\u0438 \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e \u0441\u0431\u043e\u0440\u043a\u0438 \u043f\u0440\u043e\u0435\u043a\u0442\u043e\u0432. \u041d\u043e \u0440\u0435\u0447\u044c \u0438\u0434\u0451\u0442 \u043e \u0434\u043d\u044f\u0445 \u0438\u043b\u0438 \u043d\u0435\u0434\u0435\u043b\u044f\u0445, \u0430 \u043d\u0435 \u043c\u0435\u0441\u044f\u0446\u0430\u0445 \u0438\u043b\u0438 \u0433\u043e\u0434\u0430\u0445. \u041d\u0443 \u043a\u0430\u043a, \u0432\u044b \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442\u0435 \u0432\u044b\u0437\u043e\u0432?<\/p>\n

\u0421 \u043d\u0430\u0438\u043b\u0443\u0447\u0448\u0438\u043c\u0438 \u043f\u043e\u0436\u0435\u043b\u0430\u043d\u0438\u044f\u043c\u0438,
\n \u0421\u0442\u0430\u0439\u043d \u0434\u0435 \u0413\u0443\u0432, \u042e\u0440\u0438\u0430\u043d \u0420\u043e\u0442, \u0424\u0440\u0430\u043d\u043a \u0434\u0435 \u0411\u0443\u0440, \u0420\u0438\u0447\u0430\u0440\u0434 \u0411\u0443\u0431\u0435\u043b\u044c \u0438 \u0420\u0430\u0439\u043d\u0435\u0440 \u0425\u0435\u043d\u043b\u0435.<\/p>\n

\u0411\u043b\u0430\u0433\u043e\u0434\u0430\u0440\u043d\u043e\u0441\u0442\u0438
\n \u0420\u0430\u0431\u043e\u0442\u0430 \u0447\u0430\u0441\u0442\u0438\u0447\u043d\u043e \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0430\u043d\u0430 \u043f\u0440\u043e\u0435\u043a\u0442\u043e\u043c \u0441\u0435\u0434\u044c\u043c\u043e\u0439 \u0440\u0430\u043c\u043e\u0447\u043d\u043e\u0439 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0415\u0432\u0440\u043e\u0441\u043e\u044e\u0437\u0430 FP7-610582 ENVISAGE: Engineering Virtualized Services.
\n \u042d\u0442\u0430 \u0441\u0442\u0430\u0442\u044c\u044f \u043d\u0435 \u0431\u044b\u043b\u0430 \u0431\u044b \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0430 \u0431\u0435\u0437 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u043a\u0438 \u0438 \u0432\u0435\u0436\u043b\u0438\u0432\u044b\u0445 \u043d\u0430\u043f\u043e\u043c\u0438\u043d\u0430\u043d\u0438\u0439 \u0410\u043c\u0443\u043d\u0434\u0430 \u0422\u0432\u0435\u0439\u0442\u0430! \u0422\u0430\u043a\u0436\u0435 \u043c\u044b \u0445\u043e\u0442\u0438\u043c \u043f\u043e\u0431\u043b\u0430\u0433\u043e\u0434\u0430\u0440\u0438\u0442\u044c \u0411\u0435\u0440\u0443\u0437\u0430 \u041d\u043e\u0431\u0430\u043a\u0442\u0430 \u0437\u0430 \u0442\u043e, \u0447\u0442\u043e \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u0438\u043b \u043d\u0430\u043c \u0432\u0438\u0434\u0435\u043e, \u0434\u0435\u043c\u043e\u043d\u0441\u0442\u0440\u0438\u0440\u0443\u044e\u0449\u0435\u0435 \u043e\u0448\u0438\u0431\u043a\u0443.<\/p>\n

\t http:\/\/habrahabr.ru\/post\/251751\/<\/p>\n","protected":false},"excerpt":{"rendered":"

\u0422\u0438\u043c \u041f\u0435\u0442\u0435\u0440\u0441 \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043b \u0433\u0438\u0431\u0440\u0438\u0434\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 Timsort \u0432 2002 \u0433\u043e\u0434\u0443. \u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0438\u0441\u043a\u0443\u0441\u043d\u0443\u044e \u043a\u043e\u043c\u0431\u0438\u043d\u0430\u0446\u0438\u044e \u0438\u0434\u0435\u0439 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u0441\u043b\u0438\u044f\u043d\u0438\u0435\u043c \u0438 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u0432\u0441\u0442\u0430\u0432\u043a\u0430\u043c\u0438 \u0438 \u0437\u0430\u0442\u043e\u0447\u0435\u043d \u043d\u0430 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u0443\u044e \u0440\u0430\u0431\u043e\u0442\u0443 \u0441 \u0440\u0435\u0430\u043b\u044c\u043d\u044b\u043c\u0438 \u0434\u0430\u043d\u043d\u044b\u043c\u0438. \u0412\u043f\u0435\u0440\u0432\u044b\u0435 Timsort \u0431\u044b\u043b \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d \u0434\u043b\u044f Python, \u043d\u043e \u0437\u0430\u0442\u0435\u043c \u0414\u0436\u043e\u0448\u0443\u0430 \u0411\u043b\u043e\u0445 (\u0441\u043e\u0437\u0434\u0430\u0442\u0435\u043b\u044c \u043a\u043e\u043b\u043b\u0435\u043a\u0446\u0438\u0439 Java, \u0438\u043c\u0435\u043d\u043d\u043e \u043e\u043d, \u043a\u0441\u0442\u0430\u0442\u0438, \u043e\u0442\u043c\u0435\u0442\u0438\u043b, \u0447\u0442\u043e \u0431\u043e\u043b\u044c\u0448\u0438\u043d\u0441\u0442\u0432\u043e \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432 \u0434\u0432\u043e\u0438\u0447\u043d\u043e\u0433\u043e \u043f\u043e\u0438\u0441\u043a\u0430 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043e\u0448\u0438\u0431\u043a\u0443) \u043f\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043b \u0435\u0433\u043e \u043d\u0430 Java (\u043c\u0435\u0442\u043e\u0434\u044b java.util.Collections.sort \u0438 java.util.Arrays.sort). \u0421\u0435\u0433\u043e\u0434\u043d\u044f Timsort \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u044b\u043c \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u043c \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u0432 Android SDK, Oracle JDK \u0438 OpenJDK. \u0423\u0447\u0438\u0442\u044b\u0432\u0430\u044f \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u043e\u0441\u0442\u044c \u044d\u0442\u0438\u0445 \u043f\u043b\u0430\u0442\u0444\u043e\u0440\u043c, \u043c\u043e\u0436\u043d\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u0432\u044b\u0432\u043e\u0434, \u0447\u0442\u043e \u0441\u0447\u0451\u0442 \u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440\u043e\u0432, \u043e\u0431\u043b\u0430\u0447\u043d\u044b\u0445 \u0441\u0435\u0440\u0432\u0438\u0441\u043e\u0432 \u0438 \u043c\u043e\u0431\u0438\u043b\u044c\u043d\u044b\u0445 \u0443\u0441\u0442\u0440\u043e\u0439\u0441\u0442\u0432, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0449\u0438\u0445 Timsort \u0434\u043b\u044f \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438, \u0438\u0434\u0451\u0442 \u043d\u0430 \u043c\u0438\u043b\u043b\u0438\u0430\u0440\u0434\u044b.<\/p>\n

\u041d\u043e \u0432\u0435\u0440\u043d\u0451\u043c\u0441\u044f \u0432 2015-\u0439 \u0433\u043e\u0434. \u041f\u043e\u0441\u043b\u0435 \u0442\u043e\u0433\u043e \u043a\u0430\u043a \u043c\u044b \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043b\u0438 Java-\u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u043f\u043e\u0434\u0441\u0447\u0451\u0442\u043e\u043c \u0438 \u043f\u043e\u0440\u0430\u0437\u0440\u044f\u0434\u043d\u043e\u0439 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 (J. Autom. Reasoning 53(2), 129-139) \u043d\u0430\u0448\u0438\u043c \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u043e\u0434 \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u0435\u043c KeY, \u043c\u044b \u0438\u0441\u043a\u0430\u043b\u0438 \u043d\u043e\u0432\u044b\u0439 \u043e\u0431\u044a\u0435\u043a\u0442 \u0434\u043b\u044f \u0438\u0437\u0443\u0447\u0435\u043d\u0438\u044f. Timsort \u043a\u0430\u0437\u0430\u043b\u0441\u044f \u043f\u043e\u0434\u0445\u043e\u0434\u044f\u0449\u0435\u0439 \u043a\u0430\u043d\u0434\u0438\u0434\u0430\u0442\u0443\u0440\u043e\u0439, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u043e\u043d \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u0441\u043b\u043e\u0436\u043d\u044b\u0439 \u0438 \u0448\u0438\u0440\u043e\u043a\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f. \u041a \u0441\u043e\u0436\u0430\u043b\u0435\u043d\u0438\u044e, \u043c\u044b \u043d\u0435 \u0441\u043c\u043e\u0433\u043b\u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u0435\u0433\u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c. \u041f\u0440\u0438\u0447\u0438\u043d\u0430 \u044d\u0442\u043e\u0433\u043e \u043f\u0440\u0438 \u0434\u0435\u0442\u0430\u043b\u044c\u043d\u043e\u043c \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0435\u043d\u0438\u0438 \u043e\u043a\u0430\u0437\u0430\u043b\u0430\u0441\u044c \u043f\u0440\u043e\u0441\u0442\u0430: \u0432 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 Timsort \u0435\u0441\u0442\u044c \u0431\u0430\u0433. \u041d\u0430\u0448\u0438 \u0442\u0435\u043e\u0440\u0435\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u0438\u0441\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u043d\u0438\u044f \u0443\u043a\u0430\u0437\u0430\u043b\u0438 \u043d\u0430\u043c, \u0433\u0434\u0435 \u0438\u0441\u043a\u0430\u0442\u044c \u043e\u0448\u0438\u0431\u043a\u0443 (\u043b\u044e\u0431\u043e\u043f\u044b\u0442\u043d\u043e, \u0447\u0442\u043e \u043e\u0448\u0438\u0431\u043a\u0430 \u0431\u044b\u043b\u0430 \u0443\u0436\u0435 \u0432 \u043f\u0438\u0442\u043e\u043d\u043e\u0432\u0441\u043a\u043e\u0439 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438). \u0412 \u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f, \u043a\u0430\u043a \u043c\u044b \u044d\u0442\u043e\u0433\u043e \u0434\u043e\u0431\u0438\u043b\u0438\u0441\u044c.<\/p>\n

\u0421\u0442\u0430\u0442\u044c\u044f \u0441 \u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u043b\u043d\u044b\u043c \u0430\u043d\u0430\u043b\u0438\u0437\u043e\u043c, \u0430 \u0442\u0430\u043a\u0436\u0435 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0442\u0435\u0441\u0442\u043e\u0432\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b \u043d\u0430 \u043d\u0430\u0448\u0435\u043c \u0441\u0430\u0439\u0442\u0435.<\/p>\n

\u0421\u043e\u0434\u0435\u0440\u0436\u0430\u043d\u0438\u0435
\n \u0411\u0430\u0433 \u0432 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 Timsort \u043d\u0430 Android, Java \u0438 Python
\n 1.1 \u0412\u043e\u0441\u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u043c \u0431\u0430\u0433 Timsort \u043d\u0430 Java
\n 1.2 \u041a\u0430\u043a \u0432 \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u0435 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 Timsort?
\n 1.3 \u0411\u0430\u0433 Timsort \u0448\u0430\u0433 \u0437\u0430 \u0448\u0430\u0433\u043e\u043c \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e (\u043d\u0435)\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 Timsort
\n 2.1 \u0421\u0438\u0441\u0442\u0435\u043c\u0430 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 KeY
\n 2.2 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0438 \u0435\u0433\u043e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f
\n 2.3 \u0410\u043d\u0430\u043b\u0438\u0437 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u043e\u0432 \u0440\u0430\u0431\u043e\u0442\u044b KeY \u041f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u043d\u044b\u0435 \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u0431\u0430\u0433\u0430 \u043a \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f\u043c Timsort \u043d\u0430 Python \u0438 Android\/Java
\n 3.1 \u041d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f merge_collapse (Python)
\n 3.2 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f merge_collapse (Python)
\n 3.3 \u041d\u0435\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f mergeCollapse (Java\/Android)
\n 3.4 \u0418\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f mergeCollapse (Java\/Android) \u0417\u0430\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435: \u043a\u0430\u043a\u0438\u0435 \u0438\u0437 \u044d\u0442\u043e\u0433\u043e \u0441\u043b\u0435\u0434\u0443\u044e\u0442 \u0432\u044b\u0432\u043e\u0434\u044b?
\n 1. \u0411\u0430\u0433 \u0432 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 Timsort \u043d\u0430 Android, Java \u0438 Python
\n \u0422\u0430\u043a \u0432 \u0447\u0451\u043c \u0436\u0435 \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0431\u0430\u0433? \u0418 \u043f\u043e\u0447\u0435\u043c\u0443 \u0431\u044b \u0432\u0430\u043c \u043d\u0435 \u043f\u043e\u043f\u0440\u043e\u0431\u043e\u0432\u0430\u0442\u044c \u0432\u043e\u0441\u043f\u0440\u043e\u0438\u0437\u0432\u0435\u0441\u0442\u0438 \u0435\u0433\u043e \u0441\u0430\u043c\u0438\u043c?<\/p>\n

1.1 \u0412\u043e\u0441\u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u043c \u0431\u0430\u0433 Timsort \u043d\u0430 Java
\n git clone https:\/\/github.com\/abstools\/java-timsort-bug.git cd java-timsort-bug javac *.java java TestTimSort 67108864
\n \u0415\u0441\u043b\u0438 \u0431\u0430\u0433 \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442, \u0432\u044b \u0443\u0432\u0438\u0434\u0438\u0442\u0435 \u0442\u0430\u043a\u043e\u0439 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442
\n Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: 40 at java.util.TimSort.pushRun(TimSort.java:413) at java.util.TimSort.sort(TimSort.java:240) at java.util.Arrays.sort(Arrays.java:1438) at TestTimSort.main(TestTimSort.java:18)
\n \u0412\u0438\u0434\u0435\u043e\u0437\u0430\u043f\u0438\u0441\u044c \u0432\u043e\u0441\u043f\u0440\u043e\u0438\u0437\u0432\u0435\u0434\u0435\u043d\u0438\u044f \u043e\u0448\u0438\u0431\u043a\u0438<\/p>\n

1.2 \u041a\u0430\u043a \u0432 \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u0435 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 Timsort?
\n \u0422imsort \u2014 \u044d\u0442\u043e \u0433\u0438\u0431\u0440\u0438\u0434\u043d\u044b\u0439 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0443 \u0432\u0441\u0442\u0430\u0432\u043a\u043e\u0439 \u0438 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0443 \u0441\u043b\u0438\u044f\u043d\u0438\u0435\u043c.<\/p>\n

\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c \u043f\u0435\u0440\u0435\u0443\u043f\u043e\u0440\u044f\u0434\u043e\u0447\u0438\u0432\u0430\u0435\u0442 \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432 \u0441\u043b\u0435\u0432\u0430 \u043d\u0430\u043f\u0440\u0430\u0432\u043e, \u043d\u0430\u0445\u043e\u0434\u044f \u0432 \u043d\u0451\u043c \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u0435 (\u043d\u0435\u043f\u0435\u0440\u0435\u043a\u0440\u044b\u0432\u0430\u044e\u0449\u0438\u0435\u0441\u044f) \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0435 \u0441\u0435\u0433\u043c\u0435\u043d\u0442\u044b (\u00ab\u0441\u0435\u0440\u0438\u0438\u00bb, \u0438\u043b\u0438 runs). \u0415\u0441\u043b\u0438 \u0441\u0435\u0440\u0438\u044f \u043a\u043e\u0440\u043e\u0447\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0451\u043d\u043d\u043e\u0439 \u043c\u0438\u043d\u0438\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0434\u043b\u0438\u043d\u044b, \u043e\u043d\u0430 \u0434\u043e\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c\u0438 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u0430\u043c\u0438 \u0438 \u0441\u043e\u0440\u0442\u0438\u0440\u0443\u0435\u0442\u0441\u044f \u0432\u0441\u0442\u0430\u0432\u043a\u043e\u0439. \u0414\u043b\u0438\u043d\u044b \u0441\u043e\u0437\u0434\u0430\u043d\u043d\u044b\u0445 \u0441\u0435\u0440\u0438\u0439 \u0434\u043e\u0431\u0430\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0432 \u043a\u043e\u043d\u0435\u0446 \u043c\u0430\u0441\u0441\u0438\u0432\u0430 runLen. \u041a\u043e\u0433\u0434\u0430 \u043d\u043e\u0432\u0430\u044f \u0441\u0435\u0440\u0438\u044f \u0434\u043e\u0431\u0430\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0432 runLen, \u043c\u0435\u0442\u043e\u0434 mergeCollapse \u0441\u043b\u0438\u0432\u0430\u0435\u0442 \u0441\u0435\u0440\u0438\u0438, \u043f\u043e\u043a\u0430 \u0442\u0440\u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u0430 \u0432 runLen \u043d\u0435 \u0431\u0443\u0434\u0443\u0442 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u0442\u044c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0439 \u043f\u0430\u0440\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u00ab\u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u043c\u00bb:<\/p>\n

runLen [n-2] > runLen [n-1] + runLen [n] runLen [n-1] > runLen [n]
\n \u0417\u0434\u0435\u0441\u044c n \u2014 \u044d\u0442\u043e \u0438\u043d\u0434\u0435\u043a\u0441 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0435\u0439 \u0441\u0435\u0440\u0438\u0438 \u0432 runLen. \u0418\u0434\u0435\u044f \u0431\u044b\u043b\u0430 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u044d\u0442\u043e\u0433\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0430 \u0434\u043b\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0442\u0440\u0451\u0445 \u0441\u0435\u0440\u0438\u0439 \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u0435\u0442, \u0447\u0442\u043e \u0432\u0441\u0435 \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u0442\u0440\u043e\u0439\u043a\u0438 \u0441\u0435\u0440\u0438\u0439 \u0431\u0443\u0434\u0443\u0442 \u0435\u043c\u0443 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u0442\u044c. \u0412 \u043a\u043e\u043d\u0446\u0435 \u0441\u043b\u0438\u0432\u0430\u044e\u0442\u0441\u044f \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438, \u0447\u0442\u043e \u0434\u0430\u0451\u0442 \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u043e\u0442\u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432.<\/p>\n

\u0418\u0437 \u0441\u043e\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u0439 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0441\u0442\u0438 \u0436\u0435\u043b\u0430\u0442\u0435\u043b\u044c\u043d\u043e \u0432\u044b\u0434\u0435\u043b\u0438\u0442\u044c \u043a\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u043c\u0435\u043d\u044c\u0448\u0435 \u043f\u0430\u043c\u044f\u0442\u0438 \u043f\u043e\u0434 runLen, \u043d\u043e \u0435\u0451 \u0434\u043e\u043b\u0436\u043d\u043e \u0431\u044b\u0442\u044c \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u0447\u0442\u043e\u0431\u044b \u0442\u0443\u0434\u0430 \u0437\u0430\u0432\u0435\u0434\u043e\u043c\u043e \u043f\u043e\u043c\u0435\u0441\u0442\u0438\u043b\u0438\u0441\u044c \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438. \u0415\u0441\u043b\u0438 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u0432\u0441\u0435\u0445 \u0441\u0435\u0440\u0438\u0439, \u0434\u043b\u0438\u043d\u0430 \u0441\u0435\u0440\u0438\u0439 \u0431\u0443\u0434\u0435\u0442 \u0440\u0430\u0441\u0442\u0438 \u044d\u043a\u0441\u043f\u043e\u043d\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e (\u0434\u0430\u0436\u0435 \u0431\u044b\u0441\u0442\u0440\u0435\u0435, \u0447\u0435\u043c \u0447\u0438\u0441\u043b\u0430 \u0424\u0438\u0431\u043e\u043d\u0430\u0447\u0447\u0438: \u0434\u043b\u0438\u043d\u0430 \u043a\u0430\u0436\u0434\u043e\u0439 \u0441\u0435\u0440\u0438\u0438 \u0441\u0442\u0440\u043e\u0433\u043e \u0431\u043e\u043b\u044c\u0448\u0435 \u0441\u0443\u043c\u043c\u044b \u0434\u043b\u0438\u043d \u0434\u0432\u0443\u0445 \u043f\u043e\u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0445). \u0422\u0430\u043a \u043a\u0430\u043a \u0441\u0435\u0440\u0438\u0438 \u043d\u0435 \u043f\u0435\u0440\u0435\u043a\u0440\u044b\u0432\u0430\u044e\u0442\u0441\u044f, \u0438\u0445 \u043f\u043e\u0442\u0440\u0435\u0431\u0443\u0435\u0442\u0441\u044f \u043d\u0435 \u0442\u0430\u043a \u043c\u043d\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u043e\u0442\u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0434\u0430\u0436\u0435 \u043e\u0433\u0440\u043e\u043c\u043d\u044b\u0439 \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432.<\/p>\n

1.3 \u0411\u0430\u0433 Timsort \u0448\u0430\u0433 \u0437\u0430 \u0448\u0430\u0433\u043e\u043c
\n \u0418\u0437 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0433\u043e \u0444\u0440\u0430\u0433\u043c\u0435\u043d\u0442\u0430 \u043a\u043e\u0434\u0430 \u0432\u0438\u0434\u043d\u043e, \u0447\u0442\u043e \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f mergeCollapse \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0434\u043b\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0442\u0440\u0451\u0445 \u0441\u0435\u0440\u0438\u0439 \u0432 runLen:
\n private void mergeCollapse() { while (stackSize > 1) { int n = stackSize — 2; if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) { if (runLen[n — 1] < runLen[n + 1]) n—; mergeAt(n); } else if (runLen[n] <= runLen[n + 1]) { mergeAt(n); } else { break; \/\/ \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d } } }
\n \u041a \u0441\u043e\u0436\u0430\u043b\u0435\u043d\u0438\u044e, \u044d\u0442\u043e\u0433\u043e \u043d\u0435 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u0447\u0442\u043e\u0431\u044b \u0432\u0441\u0435 \u0441\u0435\u0440\u0438\u0438 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u043b\u0438 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443. \u041f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0438\u043c, \u0447\u0442\u043e runLen \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0442\u0430\u043a\u043e\u0439 \u043d\u0430\u0431\u043e\u0440 \u0434\u043b\u0438\u043d \u043f\u0435\u0440\u0435\u0434 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435\u043c mergeCollapse (n=4):
\n 120, 80, 25, 20, 30
\n \u041d\u0430 \u043f\u0435\u0440\u0432\u043e\u043c \u043f\u0440\u043e\u0445\u043e\u0434\u0435 \u0446\u0438\u043a\u043b\u0430 while \u0431\u0443\u0434\u0443\u0442 \u043e\u0431\u044a\u0435\u0434\u0438\u043d\u0435\u043d\u044b \u0441\u0435\u0440\u0438\u0438 \u0434\u043b\u0438\u043d\u043e\u0439 25 \u0438 20 (\u0442\u0430\u043a \u043a\u0430\u043a 25 < 20 + 30 \u0438 25 < 30):
\n 120, 80, 45, 30
\n \u041d\u0430 \u0432\u0442\u043e\u0440\u043e\u043c \u043f\u0440\u043e\u0445\u043e\u0434\u0435 \u0446\u0438\u043a\u043b\u0430 (\u0442\u0435\u043f\u0435\u0440\u044c n=3), \u043c\u044b \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u043c, \u0447\u0442\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043b\u0435\u043d \u0434\u043b\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0445 \u0442\u0440\u0451\u0445 \u0441\u0435\u0440\u0438\u0439, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e 80 > 45 + 30 \u0438 45 > 30, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 mergeCollapse \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u0442 \u0440\u0430\u0431\u043e\u0442\u0443. \u041d\u043e mergeCollapse \u043d\u0435 \u0432\u043e\u0441\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u043b \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0434\u043b\u044f \u0432\u0441\u0435\u0433\u043e \u043c\u0430\u0441\u0441\u0438\u0432\u0430: \u043e\u043d \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f \u0432 \u043f\u0435\u0440\u0432\u043e\u0439 \u0442\u0440\u043e\u0439\u043a\u0435, \u0442\u0430\u043a \u043a\u0430\u043a 120 < 80 + 45.<\/p>\n

\u0413\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440 \u0442\u0435\u0441\u0442\u043e\u0432 \u043d\u0430 \u043d\u0430\u0448\u0435\u043c \u0441\u0430\u0439\u0442\u0435 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0432\u044b\u044f\u0432\u0438\u0442\u044c \u044d\u0442\u0443 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0443. \u041e\u043d \u0441\u043e\u0437\u0434\u0430\u0451\u0442 \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432 \u0441 \u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e\u043c \u043a\u043e\u0440\u043e\u0442\u043a\u0438\u0445 \u0441\u0435\u0440\u0438\u0439, \u043f\u0440\u0438 \u044d\u0442\u043e\u043c \u0438\u0445 \u0434\u043b\u0438\u043d\u044b \u043d\u0435 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0443, \u0447\u0442\u043e \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 \u043a \u043f\u0430\u0434\u0435\u043d\u0438\u044e Timsort. \u0418\u0441\u0442\u0438\u043d\u043d\u0430\u044f \u043f\u0440\u0438\u0447\u0438\u043d\u0430 \u043e\u0448\u0438\u0431\u043a\u0438 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0438\u0437-\u0437\u0430 \u043d\u0430\u0440\u0443\u0448\u0435\u043d\u0438\u044f \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u0430 \u0434\u043b\u0438\u043d\u044b \u0441\u0435\u0440\u0438\u0439 \u0440\u0430\u0441\u0442\u0443\u0442 \u043c\u0435\u0434\u043b\u0435\u043d\u043d\u0435\u0435, \u0447\u0435\u043c \u043e\u0436\u0438\u0434\u0430\u043b\u043e\u0441\u044c, \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u0447\u0435\u0433\u043e \u0438\u0445 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u043f\u0440\u0435\u0432\u044b\u0448\u0430\u0435\u0442 runLen.length \u0438 \u044d\u0442\u043e \u043f\u0440\u0438\u0432\u043e\u0434\u0438\u0442 \u043a ArrayOutOfBoundsException.<\/p>\n

2. \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e (\u043d\u0435)\u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 Timsort
\n \u041c\u044b \u043e\u0431\u043d\u0430\u0440\u0443\u0436\u0438\u043b\u0438, \u0447\u0442\u043e \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 mergeCollapse \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f, \u043a\u043e\u0433\u0434\u0430 \u043f\u044b\u0442\u0430\u043b\u0438\u0441\u044c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c Timsort. \u041a \u0441\u0447\u0430\u0441\u0442\u044c\u044e, \u043c\u044b \u0442\u0430\u043a\u0436\u0435 \u043f\u043e\u043d\u044f\u043b\u0438, \u043a\u0430\u043a \u0435\u0433\u043e \u0438\u0441\u043f\u0440\u0430\u0432\u0438\u0442\u044c. \u0412 \u0438\u0442\u043e\u0433\u0435 \u043d\u0430\u043c \u0434\u0430\u0436\u0435 \u0443\u0434\u0430\u043b\u043e\u0441\u044c \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0438\u0441\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0443\u044e \u0432\u0435\u0440\u0441\u0438\u044e, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0441\u043e\u0431\u043b\u044e\u0434\u0430\u0435\u0442\u0441\u044f. \u041d\u043e \u043d\u0435 \u0431\u0443\u0434\u0435\u043c \u0441\u043f\u0435\u0448\u0438\u0442\u044c. \u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u0440\u0430\u0437\u0431\u0435\u0440\u0451\u043c\u0441\u044f, \u0447\u0442\u043e \u0442\u0430\u043a\u043e\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438 \u043a\u0430\u043a \u043e\u043d\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f.<\/p>\n

2.1 \u0421\u0438\u0441\u0442\u0435\u043c\u0430 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 KeY
\n KeY \u2014 \u044d\u0442\u043e \u043f\u043b\u0430\u0442\u0444\u043e\u0440\u043c\u0430 \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043e\u0434\u043d\u043e\u043f\u043e\u0442\u043e\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043d\u0430 Java \u0438 JavaCard. \u041e\u043d\u0430 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043f\u043e \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438. \u0413\u0440\u0443\u0431\u043e \u0433\u043e\u0432\u043e\u0440\u044f, \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0441\u043e\u0441\u0442\u043e\u0438\u0442 \u0438\u0437 \u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u0439 (\u0432 \u0442\u0435\u0440\u043c\u0438\u043d\u0430\u0445 KeY \u2014 requires) \u0438 \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0439 (\u0432 \u0442\u0435\u0440\u043c\u0438\u043d\u0430\u0445 KeY \u2014 ensures). \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0437\u0430\u0434\u0430\u044e\u0442\u0441\u044f \u043f\u0435\u0440\u0435\u0434 \u043c\u0435\u0442\u043e\u0434\u0430\u043c\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0438\u0445 \u0440\u0435\u0430\u043b\u0438\u0437\u0443\u044e\u0442 (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u043f\u0435\u0440\u0435\u0434 \u0443\u043f\u043e\u043c\u044f\u043d\u0443\u0442\u044b\u043c \u0432\u044b\u0448\u0435 mergeCollapse()). \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043c\u0435\u0442\u043e\u0434\u0430 \u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u0435\u0433\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u043c.<\/p>\n

\u0412 \u0441\u043b\u0443\u0447\u0430\u0435 \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u043a\u0438 \u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u043f\u0440\u043e\u0441\u0442\u043e \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u0435\u0442, \u0447\u0442\u043e \u043d\u0430 \u0432\u0445\u043e\u0434 \u043f\u043e\u0434\u0430\u0451\u0442\u0441\u044f \u043d\u0435\u043f\u0443\u0441\u0442\u043e\u0439 \u043c\u0430\u0441\u0441\u0438\u0432, \u0430 \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0435 \u0442\u0440\u0435\u0431\u0443\u0435\u0442, \u0447\u0442\u043e\u0431\u044b \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0438\u0440\u0443\u044e\u0449\u0438\u0439 \u043c\u0430\u0441\u0441\u0438\u0432 \u0431\u044b\u043b \u0441\u043e\u0440\u0442\u0438\u0440\u043e\u0432\u0430\u043d \u0438 \u044f\u0432\u043b\u044f\u043b\u0441\u044f \u043f\u0435\u0440\u0435\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u043e\u0439 \u0432\u0445\u043e\u0434\u043d\u043e\u0433\u043e. \u0421\u0438\u0441\u0442\u0435\u043c\u0430 KeY \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u0432\u044b\u0437\u0432\u0430\u0442\u044c \u0441 \u0432\u0445\u043e\u0434\u043d\u044b\u043c\u0438 \u0434\u0430\u043d\u043d\u044b\u043c\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u044e\u0442 \u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u044f\u043c, \u0442\u043e \u043c\u0435\u0442\u043e\u0434 \u0437\u0430\u0432\u0435\u0440\u0448\u0438\u0442\u0441\u044f \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0438 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0438\u0440\u0443\u044e\u0449\u0435\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0431\u0443\u0434\u0435\u0442 \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u0442\u044c \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u044e. \u042d\u0442\u043e \u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u043f\u043e\u043b\u043d\u043e\u0439 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c\u044e, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u0438 \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0435 \u0437\u0430\u0432\u0435\u0440\u0448\u0435\u043d\u0438\u0435 \u043c\u0435\u0442\u043e\u0434\u0430. \u041a\u0430\u043a \u043c\u044b \u0443\u0432\u0438\u0434\u0435\u043b\u0438, \u043c\u0435\u0442\u043e\u0434 java.utils.Array.sort() \u0438\u0437 OpenJDK \u043d\u0435 \u0441\u043e\u0431\u043b\u044e\u0434\u0430\u0435\u0442 \u044d\u0442\u043e\u0442 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0434\u043b\u044f \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0451\u043d\u043d\u044b\u0445 \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u0434\u0430\u043d\u043d\u044b\u0445 \u043e\u043d \u0437\u0430\u0432\u0435\u0440\u0448\u0430\u0435\u0442\u0441\u044f \u0438\u0441\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435\u043c.<\/p>\n

\u0414\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u043a\u043b\u0430\u0441\u0441\u043e\u0432 \u0438 \u043e\u0431\u044a\u0435\u043a\u0442\u043e\u0432, \u0447\u0442\u043e\u0431\u044b \u0443\u043a\u0430\u0437\u0430\u0442\u044c \u043e\u0431\u0449\u0438\u0435 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u0438\u044f \u043d\u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u043f\u043e\u043b\u0435\u0439. \u041e\u0431\u044b\u0447\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442\u0441\u044f \u0441\u043e\u0433\u043b\u0430\u0441\u043e\u0432\u0430\u043d\u043d\u043e\u0441\u0442\u044c \u0434\u0430\u043d\u043d\u044b\u0445 \u0438\u043b\u0438 \u0433\u0440\u0430\u043d\u0438\u0447\u043d\u044b\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u044f:
\n \/*@ private invariant @ runBase.length == runLen.length && runBase != runLen; @*\/
\n \u042d\u0442\u043e\u0442 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442 \u0433\u043e\u0432\u043e\u0440\u0438\u0442, \u0447\u0442\u043e \u0434\u043b\u0438\u043d\u044b \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432 runBase \u0438 runLen \u0434\u043e\u043b\u0436\u043d\u044b \u0441\u043e\u0432\u043f\u0430\u0434\u0430\u0442\u044c, \u043d\u043e \u0432 \u0442\u043e \u0436\u0435 \u0432\u0440\u0435\u043c\u044f \u044d\u0442\u043e \u0434\u043e\u043b\u0436\u043d\u044b \u0431\u044b\u0442\u044c \u0434\u0432\u0430 \u0440\u0430\u0437\u043d\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u0430. \u0421\u0435\u043c\u0430\u043d\u0442\u0438\u043a\u0430 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043e\u0432 \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u0435\u0442, \u0447\u0442\u043e \u043a\u0430\u0436\u0434\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u043d\u0430 \u0432\u044b\u0445\u043e\u0434\u0435 \u0434\u043e\u043b\u0436\u0435\u043d \u043d\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u0442\u044c \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u044f \u0441\u0432\u043e\u0435\u0433\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430, \u043d\u043e \u0438 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u044b \u0435\u0433\u043e \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0433\u043e \u043e\u0431\u044a\u0435\u043a\u0442\u0430 \u201cthis\u201d.<\/p>\n

\u0412 \u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u044f\u0437\u044b\u043a\u0430 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0439 KeY \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442 Java Modeling Language (JML). \u0412\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u043d\u0430 \u043d\u0451\u043c \u043f\u0438\u0448\u0443\u0442\u0441\u044f \u043a\u0430\u043a \u043d\u0430 \u043e\u0431\u044b\u0447\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 Java, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 Java-\u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0441\u0442\u044b \u0435\u0433\u043e \u043b\u0435\u0433\u043a\u043e \u043e\u0441\u0432\u043e\u044f\u0442. \u0413\u043b\u0430\u0432\u043d\u043e\u0435 \u0440\u0430\u0441\u0448\u0438\u0440\u0435\u043d\u0438\u0435 JML \u2014 \u044d\u0442\u043e \u043a\u0432\u0430\u043d\u0442\u043e\u0440\u044b (\\forall T x \u2014 \u0434\u043b\u044f \u043b\u044e\u0431\u043e\u0433\u043e T, \\exists T x \u2014 \u0441\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 T) \u0438, \u043a\u043e\u043d\u0435\u0447\u043d\u043e, \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u0435 \u043a\u043b\u044e\u0447\u0435\u0432\u044b\u0435 \u0441\u043b\u043e\u0432\u0430 \u0434\u043b\u044f \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0421\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 JML \u043f\u0440\u0438\u0432\u043e\u0434\u044f\u0442\u0441\u044f \u0432 \u043a\u043e\u043c\u043c\u0435\u043d\u0442\u0430\u0440\u0438\u044f\u0445 java-\u0444\u0430\u0439\u043b\u043e\u0432 \u043f\u0435\u0440\u0435\u0434 \u043a\u043e\u0434\u043e\u043c, \u043a \u043a\u043e\u0442\u043e\u0440\u043e\u043c\u0443 \u043e\u043d\u0438 \u043e\u0442\u043d\u043e\u0441\u044f\u0442\u0441\u044f. \u041d\u0438\u0436\u0435 \u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u043f\u0440\u0438\u043c\u0435\u0440 Java-\u043c\u0435\u0442\u043e\u0434\u0430 \u0441 JML-\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0435\u0439:<\/p>\n

\/*@ private normal_behavior @ requires @ n >= MIN_MERGE; @ ensures @ \\result >= MIN_MERGE\/2; @*\/ private static int \/*@ pure @*\/ minRunLength(int n) { assert n >= 0; int r = 0; \/\/ \u0421\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u0441\u044f 1 \u0435\u0441\u043b\u0438 \u0445\u043e\u0442\u044f \u0431\u044b \u043e\u0434\u0438\u043d \u0435\u0434\u0438\u043d\u0438\u0447\u043d\u044b\u0439 \u0431\u0438\u0442 \u0431\u044b\u043b \u0443\u0434\u0430\u043b\u0451\u043d \u0441\u0434\u0432\u0438\u0433\u043e\u043c \/*@ loop_invariant n >= MIN_MERGE\/2 && r >=0 && r<=1; @ decreases n; @ assignable \\nothing; @*\/ while (n >= MIN_MERGE) { r |= (n & 1); n >>= 1; } return n + r; }
\n \u041a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 minRunLength() \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u043e\u0434\u043d\u043e \u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u0435: \u0432\u0445\u043e\u0434\u043d\u043e\u0439 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440 \u0434\u043e\u043b\u0436\u0435\u043d \u0431\u044b\u0442\u044c \u043d\u0435 \u043c\u0435\u043d\u044c\u0448\u0435, \u0447\u0435\u043c MIN_MERGE. \u0412 \u044d\u0442\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 (\u0438 \u0442\u043e\u043b\u044c\u043a\u043e \u0432 \u044d\u0442\u043e\u043c) \u043c\u0435\u0442\u043e\u0434 \u043e\u0431\u0435\u0449\u0430\u0435\u0442 \u0437\u0430\u0432\u0435\u0440\u0448\u0438\u0442\u044c\u0441\u044f \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e (\u043d\u0435 \u0437\u0430\u0446\u0438\u043a\u043b\u0438\u0442\u044c\u0441\u044f \u0438 \u043d\u0435 \u0432\u044b\u0431\u0440\u043e\u0441\u0438\u0442\u044c \u0438\u0441\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435) \u0438 \u0432\u0435\u0440\u043d\u0443\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0431\u043e\u043b\u044c\u0448\u0435 \u0438\u043b\u0438 \u0440\u0430\u0432\u043d\u043e MIN_MERGE\/2. \u0414\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u043c\u0435\u0442\u043e\u0434 \u043f\u043e\u043c\u0435\u0447\u0435\u043d \u043a\u0430\u043a pure (\u0447\u0438\u0441\u0442\u044b\u0439). \u042d\u0442\u043e \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u043c\u0435\u0442\u043e\u0434 \u043d\u0435 \u043c\u043e\u0434\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u0442 \u043a\u0443\u0447\u0443.<\/p>\n

\u041a\u043b\u044e\u0447\u0435\u0432\u043e\u0439 \u043c\u043e\u043c\u0435\u043d\u0442 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0441\u0438\u0441\u0442\u0435\u043c\u0430 KeY \u0441\u043f\u043e\u0441\u043e\u0431\u043d\u0430 \u0441\u0442\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u044b \u043f\u043e\u0434\u043e\u0431\u043d\u044b\u0445 \u043c\u0435\u0442\u043e\u0434\u043e\u0432 \u0434\u043b\u044f \u043b\u044e\u0431\u044b\u0445 \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u043e\u0432. \u041a\u0430\u043a \u044d\u0442\u043e \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e? KeY \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442 \u0441\u0438\u043c\u0432\u043e\u043b\u044c\u043d\u043e\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-252135","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/252135","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=252135"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/252135\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=252135"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=252135"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=252135"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}