pragma\u00a0Spark_Mode\u00a0(On);\r\npackage Sorters is\r\n type Array_Type is array ( Positive range <> ) of Integer;\r\n function Perm (A: in Array_Type,\r\n B: in Array_Type) return Boolean\r\n with Global -> null,\r\n Ghost => True,\r\n Import => True;\r\n procedure Selection_Sort (Values : in out Array_Type)\r\n with Depends => (Values => Values),\r\n Pre => Values'Length >= 1 and then\r\n Values'Last <= Positive'Last,\r\n Post => (for all J in Values'First .. Values'Last - 1 =>\r\n Values (J) <= Values (J + 1)) and then\r\n Perm (Values'Old, Values);\r\nend Sortes;\u00a0\u00a0\r\n<\/code><\/pre>\n\u4e0a\u8a18\u306f\uff0c\u30d1\u30c3\u30b1\u30fc\u30b8 Sorters \u306e\u4ed5\u69d8\u90e8\u3067\u3059\uff0e\u3053\u306e\u30d1\u30c3\u30b1\u30fc\u30b8\u3067\u306f\uff0cArray_Type \u3068\u95a2\u6570 Perm \u304a\u3088\u3073 Selection_Sort \u624b\u7d9a\u304d\u3092\u5ba3\u8a00\u3057\u3066\u3044\u307e\u3059\uff0e<\/p>\n \u6700\u521d\u306b\uff0cpragma \u3067\uff0c\u3053\u306e\u4ed5\u69d8\u90e8\u304c SPARK \u8a00\u8a9e\u3067\u3042\u308b\u3053\u3068\u3092\u5ba3\u8a00\u3057\u3066\u3044\u307e\u3059\uff0e\u4ee5\u4e0b\u306f\uff0cSPARK \u7279\u6709\u306e\u8868\u73fe\u3067\u3059\uff0e<\/p>\n \u95a2\u6570 Perm \u306e with \u7bc0\u306b\u3042\u308b Global \u306f\uff0c\u5f15\u6570\u4ee5\u5916\u3067\uff0c\u5916\u90e8\u304b\u3089\u3075\u308b\u307e\u3044\u306b\u5f71\u97ff\u3092\u4e0e\u3048\u308b\u5909\u6570\u306e\u6709\u7121\u3092\u8a18\u8ff0\u3059\u308b\u7b87\u6240\u3067\u3059\uff0e\u3053\u3053\u3067\u306f\uff0cnull \u3067\u3059\u304b\u3089\uff0c\u305d\u306e\u3088\u3046\u306a\u5909\u6570\u306f\u5b58\u5728\u3057\u306a\u3044\u3068\u4e91\u3046\u3053\u3068\u3092\u5ba3\u8a00\u3057\u3066\u3044\u307e\u3059\uff0e\u6b21\u306e Ghost \u306f\uff0c\u8a3c\u660e\u306e\u52a9\u3051\u3068\u306a\u308b\u4e00\u6642\u7684\u306a\u5b58\u5728\uff08\u305d\u308c\u304c Ghost \u3068\u3044\u3046\u540d\u524d\u306e\u7531\u6765\u3067\u3059\uff09\u3067\u3042\u308b\u3053\u3068\u3092\u793a\u3057\u3066\u3044\u307e\u3059\uff0eGhost \u95a2\u6570\u306e\u5b9f\u4f53\u306f\uff0c\u3082\u3061\u308d\u3093\u4e0e\u3048\u308b\u5fc5\u8981\u304c\u3042\u308a\u307e\u3059\uff0e\u6b21\u306e\uff0cImport \u306f\u66f4\u306b\u8208\u5473\u6df1\u3044\u5ba3\u8a00\u306b\u306a\u3063\u3066\u3044\u307e\u3059\uff0e\u3053\u306e\u95a2\u6570\u306e\u5b9f\u4f53\u306f\uff0cSPARK\u3067\u306f\u4e0e\u3048\u305a\uff0c\u3053\u306e\u8a3c\u660e\u306b\u95a2\u3057\u3066\u3088\u308a\u9069\u3057\u305f\u8868\u73fe\u5f62\u5f0f\u3092\u5229\u7528\u3059\u308b\u3068\u3044\u3046\u3053\u3068\u3092\u5ba3\u8a00\u3057\u3066\u3044\u307e\u3059\uff0e<\/p>\n \u6b21\u306e\u624b\u7d9a\u304d Selection_Sort \u306f\uff0c\u3082\u3046\u5c11\u3057\u4e00\u822c\u7684\u306a SPARK \u8a18\u8ff0\u3067\u3059\uff0ewith\u7bc0\u306e\u6700\u521d\u306e Depends \u306f\uff0c\u5909\u6570\u306e\u4f9d\u5b58\u95a2\u4fc2\u3092\u793a\u3057\u3066\u3044\u307e\u3059\uff0eValues \u306f\uff0cin out \u30e2\u30fc\u30c9\u3067\u3059\u304b\u3089\uff0c\u81ea\u5206\u81ea\u8eab\u306b\u4f9d\u5b58\u3057\u3066\u3044\u308b\u3053\u3068\u306b\u306a\u308a\u307e\u3059\uff0e\u3053\u3053\u3067\u306f\uff0c\u4f59\u308a\u306b\u5358\u7d14\u306a\u4f8b\u306a\u306e\u3067\uff0c\u8a18\u8ff0\u306e\u91cd\u8907\u306e\u3088\u3046\u306b\u3082\u898b\u3048\u307e\u3059\u304c\uff0c\u305d\u3046\u3067\u306a\u3044\u5834\u5408\u3082\u591a\u304f\uff0c\u8a3c\u660e\u306e\u305f\u3081\u306b\u8a18\u8ff0\u306f\u5e38\u306b\u5fc5\u8981\u3067\u3059\uff0e\u6b21\u306e pre \u304a\u3088\u3073 post \u306f\uff0c\u8868\u660e\uff08assertion\uff09\u3068\u3057\u3066\u3088\u304f\u77e5\u3089\u308c\u305f\u8a18\u8ff0\u3067\u3059\uff0e\u305d\u308c\u305e\u308c\uff0c\u4e8b\u524d\u6761\u4ef6\u3068\u4e8b\u5f8c\u6761\u4ef6\u3092\u793a\u3057\u3066\u3044\u307e\u3059\uff0e\u8ff0\u8a9e\u8ad6\u7406\u3067\u8a18\u8ff0\u304c\u3067\u304d\uff0c\u4e8b\u5f8c\u6761\u4ef6\u306b\u306f\uff0c\u5168\u79f0\u9650\u91cf\u5b50\uff08for all\uff09\u3092\u7528\u3044\u3066\u3044\u307e\u3059\uff0e<\/p>\n \u3053\u308c\u3089\u306e\u8a18\u8ff0\u306f\uff0c\u8a3c\u660e\u5668\uff08prover\uff09\u306b\u3088\u3063\u3066\u8a3c\u660e\u3055\u308c\u307e\u3059\uff0e\u8a3c\u660e\u5668\u81ea\u8eab\u306f\uff0c\u3082\u3061\u308d\u3093\uff0cSPARK \u306e\u7bc4\u56f2\u5916\u3067\u3059\u304c\uff0c\u73fe\u5728\u306f Community \u7248\u306b\u304a\u3044\u3066\u3082\uff0cSMT\uff08Satisfiable Modulo Theories\uff09\u30bd\u30eb\u30d0\u30fc\u306e Alt-Ergo\/CVC4\/Z3\u304c\uff0c\u540c\u68b1\u3055\u308c\u3066\u3044\u307e\u3059\uff0e<\/p>\n \u3055\u3066\uff0c\u5168\u3066\u304c\u8a3c\u660e\u3067\u304d\u308b\u308f\u3051\u3067\u306f\u306a\u3044\u3053\u3068\u306b\u6ce8\u610f\u304c\u5fc5\u8981\u3067\u3059\uff0e\u8a3c\u660e\u4e0d\u80fd\u306e\u554f\u984c\u304c\u3042\u308a\u307e\u3059\u3057\uff0c\u8907\u96d1\u306a\u7b97\u8853\u6f14\u7b97\u306f\u6271\u3048\u307e\u305b\u3093\uff08\u57fa\u672c\u7684\u306b\u306f\u7dda\u5f62\u306b\u9650\u3089\u308c\u307e\u3059\uff09\uff0e\u3057\u305f\u304c\u3063\u3066\uff0c\u5b9f\u52d9\u7684\u306b\u306f\u30c6\u30b9\u30c8\u3068\u4f75\u7528\u3068\u3044\u3046\u3053\u3068\u306b\u306a\u308a\u307e\u3059\uff0e<\/p>\n \u305d\u308c\u3067\u3082\u306a\u304a\uff0c\u8a3c\u660e\u3092\u884c\u3046\u3053\u3068\u306f\u304d\u308f\u3081\u3066\u6709\u52b9\u306a\u624b\u6bb5\u3067\u3059\uff0e\u30c6\u30b9\u30c8\u3068\u3044\u3046\u306e\u306f\uff0c\u6642\u9593\u3082\u624b\u9593\u3082\u5927\u5e45\u306b\u5fc5\u8981\u3068\u3057\u307e\u3059\uff0e\u4e00\u90e8\u3067\u3082\u8a3c\u660e\u304c\u53ef\u80fd\u3067\u3042\u308c\u3070\uff0c\u5168\u4f53\u306e\u6642\u9593\u3084\u624b\u9593\u3092\u5927\u5e45\u306b\u6e1b\u3089\u3059\u3053\u3068\u304c\u3067\u304d\u308b\u304b\u3089\u3067\u3059\uff0e<\/p>\n \u500b\u4eba\u7684\u306b\u306f\u8a3c\u660e\u3092\u610f\u8b58\u3057\u3066\u30d7\u30ed\u30b0\u30e9\u30e0\u3092\u4f5c\u308b\u3068\u4e91\u3046\u3053\u3068\u304c\uff0c\u4f55\u306b\u3082\u307e\u3057\u3066\u6709\u52b9\u3067\u3042\u308b\u6c17\u304c\u3057\u307e\u3059\uff0e<\/p>\n (NIL)<\/p>\n\n\n<\/div>\n\n\u00a0Barnes, J. G. P., Spark: The Proven Approach to High Integrity Software<\/i>. Altran Praxis: p. xi, 2012. ↵<\/a><\/span><\/li>\n \u3044\u308f\u3086\u308b\u6b21\u306e\u683c\u8a00\u201d\u30d7\u30ed\u30b0\u30e9\u30e0\u304c\u8aa4\u308a\u3092\u6301\u305f\u306a\u3044\u3053\u3068\u3092\u8a3c\u660e\u3059\u308b\u3053\u3068\u306f\u3067\u304d\u306a\u3044\u201d\u306b\u306a\u308a\u307e\u3059 ↵<\/a><\/span><\/li>\n \u3044\u308f\u3086\u308b\u30bc\u30ed\u5272\u306e\u3088\u3046\u306a\u5b9f\u884c\u6642\u30a8\u30e9\u30fc\u306f\u5e38\u306b\u201d\u60aa\u201d\u3067\u3059\u304b\u3089\uff0c\u305d\u3046\u3044\u3046\u3053\u3068\u304c\u751f\u3058\u306a\u3044\uff0c\u3068\u3044\u3046\u3053\u3068\u306f\u6539\u3081\u3066\u8a18\u8f09\u3059\u308b\u5fc5\u8981\u304c\u3042\u308a\u307e\u305b\u3093 ↵<\/a><\/span><\/li>\n J. W. McCormick and P. C. Chapin. Building High Integrity Applications with SPARK. Cambridge University Press, 2015 ↵<\/a><\/span><\/li>\n<\/ol>\n<\/div>","protected":false},"excerpt":{"rendered":"\u73fe\u5728\u306e SPARK 2014 \u306f\uff0cAda\u8a00\u8a9e\u306e\u30b5\u30d6\u30bb\u30c3\u30c8\u3067\u3059\uff0e\u3057\u304b\u3057\uff0c\u5225\u306e\u8a00\u8a9e\u3068\u3057\u3066\u8003\u3048\u308b\u3053\u3068\u304c\u671b\u307e\u3057\u305d\u3046\u3067\u30591\uff0e\u305d\u308c\u306f\uff0c\u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u6b63\u3057\u3055\u3092\u793a\u3059\u8a00\u8a9e\u3068\u3057\u3066\uff0c\u6349\u3048\u308b\u3079\u304d\u3068\u4e91\u3046\u3053\u3068\u306b\u306a\u308a\u307e\u3059\uff0e \u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u6b63\u3057\u3055\u3092\u793a\u305d\u3046\u3068…<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[6],"tags":[],"class_list":["post-118","post","type-post","status-publish","format-standard","hentry","category-spark-language"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_shortlink":"https:\/\/wp.me\/pa1llS-1U","_links":{"self":[{"href":"https:\/\/ada.jp\/index.php?rest_route=\/wp\/v2\/posts\/118","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/ada.jp\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/ada.jp\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/ada.jp\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/ada.jp\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=118"}],"version-history":[{"count":5,"href":"https:\/\/ada.jp\/index.php?rest_route=\/wp\/v2\/posts\/118\/revisions"}],"predecessor-version":[{"id":123,"href":"https:\/\/ada.jp\/index.php?rest_route=\/wp\/v2\/posts\/118\/revisions\/123"}],"wp:attachment":[{"href":"https:\/\/ada.jp\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=118"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/ada.jp\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=118"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/ada.jp\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=118"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}