{"id":10003,"date":"2016-03-09T23:18:57","date_gmt":"2016-03-09T23:18:57","guid":{"rendered":"http:\/\/www.lexicalscope.com\/blog\/?p=10003"},"modified":"2016-03-09T23:19:46","modified_gmt":"2016-03-09T23:19:46","slug":"notes-on-structured-programming-section-5-remark-3","status":"publish","type":"post","link":"https:\/\/www.lexicalscope.com\/blog\/2016\/03\/09\/notes-on-structured-programming-section-5-remark-3\/","title":{"rendered":"Notes on Structured Programming &#8211; Section 5, Remark 3"},"content":{"rendered":"<p>Here is a <a href=\"http:\/\/rise4fun.com\/Dafny\/07h\">Dafny proof<\/a> of the &#8220;exercise for the reader&#8221; from section 5 of E.W.Dijkstra&#8217;s &#8220;Notes on Structured Programming&#8221; monograph in the book &#8220;Structured Programming (1972)&#8221;.<\/p>\n<pre lang=\"dafny\">\r\nmethod Section5RemarkThree(A:int, B:int) returns (z:int) \r\n  requires A > 0\r\n  requires B >= 0\r\n  ensures z == power(A,B)\r\n{\r\n  var x := A;\r\n  var y := B;\r\n  z := 1;\r\n  \r\n  while y != 0\r\n    invariant x > 0\r\n    invariant y >= 0\r\n    invariant power(A, B) == z * power(x, y)\r\n  {\r\n    halfExponentSquareBase(x, if odd(y) then y-1 else y);\r\n    \r\n    if odd(y)\r\n    {\r\n      y := y - 1;\r\n      z := z * x;\r\n    }\r\n    y := y\/2;\r\n    x := x * x;\r\n  }\r\n}\r\n\r\nlemma halfExponentSquareBase(x:int,y:int)\r\n  requires x > 0\r\n  requires y >= 0\r\n  requires even(y)\r\n  ensures power(x, y) == power(x*x, y\/2)\r\n {\r\n   if y != 0 {\r\n     halfExponentSquareBase(x,y-2);\r\n   }\r\n }\r\n\r\npredicate method even(n: nat)\r\n   ensures even(n) <==> n % 2 == 0\r\n{\r\n   if n == 0 then true else odd(n-1)\r\n}\r\n\r\npredicate method odd(n: nat)\r\n   ensures odd(n) <==> n % 2 != 0\r\n{\r\n   if n == 0 then false else even(n-1)\r\n}\r\n\r\nfunction power(x:int, n:int):int\r\n{\r\n  if n <= 0 then 1\r\n  else x * power(x, n-1)\r\n}\r\n<\/pre>\n<p><!-- Detailed Version: http:\/\/rise4fun.com\/Dafny\/Vhm4 --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Here is a Dafny proof of the &#8220;exercise for the reader&#8221; from section 5 of E.W.Dijkstra&#8217;s &#8220;Notes on Structured Programming&#8221; monograph in the book &#8220;Structured Programming (1972)&#8221;. method Section5RemarkThree(A:int, B:int) returns (z:int) requires A > 0 requires B >= 0 &hellip; <a href=\"https:\/\/www.lexicalscope.com\/blog\/2016\/03\/09\/notes-on-structured-programming-section-5-remark-3\/\">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-10003","post","type-post","status-publish","format-standard","hentry","category-dafny"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p2e3P7-2Bl","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/10003","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=10003"}],"version-history":[{"count":3,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/10003\/revisions"}],"predecessor-version":[{"id":10006,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/10003\/revisions\/10006"}],"wp:attachment":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/media?parent=10003"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/categories?post=10003"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/tags?post=10003"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}