{"id":8984,"date":"2015-04-10T11:53:26","date_gmt":"2015-04-10T11:53:26","guid":{"rendered":"http:\/\/www.lexicalscope.com\/blog\/?p=8984"},"modified":"2015-04-11T14:17:09","modified_gmt":"2015-04-11T14:17:09","slug":"dafny-sum-and-max-solution","status":"publish","type":"post","link":"https:\/\/www.lexicalscope.com\/blog\/2015\/04\/10\/dafny-sum-and-max-solution\/","title":{"rendered":"Dafny Sum and Max solution"},"content":{"rendered":"<p>A Dafny solution to the <a href=\"http:\/\/www.verifythis.org\/post?pid=sum-and-maximum\" title=\"sum and maximum verification\">Sum and Max<\/a> verification benchmark. I added some additional specification to verify that the result <code>max<\/code> is really the maximum and the <code>sum<\/code> is really the sum.<\/p>\n<pre lang=\"Dafny\">\r\nmethod SumMax(a: array<int>) returns (sum:int, max:int)\r\n requires a != null;\r\n requires a.Length >= 0;\r\n requires forall i :: 0 <= i < a.Length ==> a[i] >= 0;\r\n ensures sum <= a.Length*max;\r\n ensures forall i :: 0 <= i < a.Length ==> a[i] <= max;\r\n ensures a.Length == 0 || \r\n         (exists i :: 0 <= i < a.Length &#038;&#038; a[i] == max);\r\n ensures sum == Sum(a);\r\n{\r\n max := 0;\r\n sum := 0;\r\n\r\n var idx:int := 0;\r\n while idx<a.Length \r\n  invariant idx <= a.Length;\r\n  invariant forall i :: 0 <= i < idx ==> a[i] <= max;\r\n  invariant (idx==0 &#038;&#038; max==0) || \r\n            exists i :: 0 <= i < idx &#038;&#038; a[i] == max;\r\n  invariant sum <= idx*max;\r\n  invariant sum == Sum'(a, 0, idx);\r\n {\r\n  if (max < a[idx])\r\n  {\r\n   max := a[idx];\r\n  }\r\n  sum := sum + a[idx];\r\n  idx := idx + 1;\r\n }\r\n}\r\n\r\nfunction Sum(a: array<int>) : int\r\n reads a;\r\n requires a != null;\r\n{\r\n Sum'(a, 0, a.Length)\r\n}\r\n\r\nfunction Sum'(a: array<int>, i:int, j:int) : int\r\n reads a;\r\n requires a != null;\r\n requires 0 <= i <= j <= a.Length;\r\n{\r\n if j == i then 0 else Sum'(a, i, j-1) + a[j-1]\r\n}\r\n\r\nlemma SumOfIntervalOneIsElement(a: array<int>, i:int)\r\n requires a != null;\r\n requires 0 <= i < a.Length;\r\n ensures a.Length > 0;\r\n ensures Sum'(a, i, i+1) == a[i];\r\n{ }\r\n\r\nlemma SumOfIntervalIsSumOfSubIntervals\r\n  (a: array<int>, i:int, j:int, k:int)\r\n requires a != null;\r\n requires 0 <= i <= j <= k <= a.Length;\r\n ensures Sum'(a, i, j) + Sum'(a, j, k) == Sum'(a, i, k);\r\n{ }\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>A Dafny solution to the Sum and Max verification benchmark. I added some additional specification to verify that the result max is really the maximum and the sum is really the sum. method SumMax(a: array) returns (sum:int, max:int) requires a &hellip; <a href=\"https:\/\/www.lexicalscope.com\/blog\/2015\/04\/10\/dafny-sum-and-max-solution\/\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_feature_clip_id":0,"_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},"jetpack_post_was_ever_published":false},"categories":[15],"tags":[],"class_list":["post-8984","post","type-post","status-publish","format-standard","hentry","category-dafny"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p2e3P7-2kU","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/8984","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/comments?post=8984"}],"version-history":[{"count":3,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/8984\/revisions"}],"predecessor-version":[{"id":8989,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/8984\/revisions\/8989"}],"wp:attachment":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/media?parent=8984"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/categories?post=8984"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/tags?post=8984"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}