{"id":1240,"date":"2012-12-11T13:12:48","date_gmt":"2012-12-11T13:12:48","guid":{"rendered":"http:\/\/www.navision-blog.de\/?p=1240"},"modified":"2012-12-11T14:32:38","modified_gmt":"2012-12-11T14:32:38","slug":"testing-proving-checking-code-properties","status":"publish","type":"post","link":"http:\/\/www.navision-blog.de\/blog\/2012\/12\/11\/testing-proving-checking-code-properties\/","title":{"rendered":"Testing, proving, checking &ndash; How to verify code properties"},"content":{"rendered":"<p>As programmers we often want to express that a special property holds for a method, e.g. we want to say that the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Associative_property\">associativity law<\/a> holds for list concatenation. In F# we could define a concat method like this:<\/p>\n<p> <script src=\"https:\/\/gist.github.com\/4258217.js\"> <\/script>  <\/p>\n<p>As programmers we could write a couple of unit tests which try to check the associativity law. With <a href=\"http:\/\/www.nunit.org\/\">NUnit<\/a> enabled we could write this:<\/p>\n<p> <script src=\"https:\/\/gist.github.com\/4258254.js\"> <\/script>  <\/p>\n<p>But the question is: did we cover all interesting cases? In computer science we have a method to prove that the property holds for all lists. This methods is called <a href=\"http:\/\/en.wikipedia.org\/wiki\/Structural_induction\">structural induction<\/a> (see also this <a href=\"https:\/\/class.coursera.org\/progfun-2012-001\/lecture\/97\">video lecture<\/a> by Martin Odersky) and would look like this:<\/p>\n<h5>1) Rewrite the code as equations<\/h5>\n<pre>concat ([],ys)    = ys                  [CON1]\nconcat (x::xs,ys) = x :: concat(xs,ys)  [CON2]<\/pre>\n<h5>2) Rewrite the property as an equation<\/h5>\n<pre>concat(concat(xs,ys),zs) = concat(xs,concat(ys,zs))<\/pre>\n<h5>3) Check the base case<\/h5>\n<pre>concat(concat([],ys),zs) <br \/>= concat ([],zs)                 \/\/ using CON1\n= []                             \/\/ using CON1<\/pre>\n<pre>concat([],concat(ys,zs))\n<br \/>= concat (ys,zs)                 \/\/ using CON1<br \/>= []                             \/\/ using CON1<\/pre>\n<h5>3) Show the inductive step<\/h5>\n<pre>concat(concat(x::xs,ys),zs) \n<br \/>= concat (x::concat(xs,ys),zs))  \/\/ using CON2<br \/>= x :: concat(concat(xs,ys),zs)  \/\/ using CON2 <br \/>= x :: concat(xs,concat(ys,zs))  \/\/ induction hypothesis<br \/>= concat(x::xs,concat(ys,zs))    \/\/ using CON2<br \/><\/pre>\n<p>This math is very clean and shows that the associativity law holds for all lists. Unfortunately even with a slightly more complicated sample this gets at least tricky. Try to prove that <em>reverse(reverse(xs)) = xs<\/em> with <strong>reversed<\/strong> defined as:<\/p>\n<p><script src=\"https:\/\/gist.github.com\/4258343.js\"> <\/script><\/p>\n<p>As you will see the na\u00efve approach with structural induction will fail (for a nice solution see <a href=\"https:\/\/class.coursera.org\/progfun-2012-001\/lecture\/101\">this video lecture<\/a>).<\/p>\n<p>There is even a bigger problem with the proof: one assumption of induction is referential transparency of the given functions. We can\u2019t always assume this.<\/p>\n<p>So we can\u2019t always (easily) proof code properties and we don\u2019t want to write too many unit tests &#8211; then what can we do?<\/p>\n<p>One compromise solution is to use a tool which systematically generates instances for our tests. There are a couple of tools out there, e.g. there is <a href=\"http:\/\/en.wikipedia.org\/wiki\/QuickCheck\">QuickCheck<\/a> for Haskell or <a href=\"http:\/\/research.microsoft.com\/en-us\/projects\/pex\/\">PEX<\/a> for .NET. In F# we can use a tool called <a href=\"http:\/\/fscheck.codeplex.com\/\">FsCheck<\/a>:<\/p>\n<p><script src=\"https:\/\/gist.github.com\/4258422.js\"> <\/script><\/p>\n<p>Of course a test like this doesn\u2019t prove that the property holds for all lists, but at least it verifies all bases cases and probably a lot more cases than one would manually do.<\/p>\n<p>If you introduce a bug you get a nice report, which even shows a counterexample:<\/p>\n<p><a href=\"http:\/\/www.navision-blog.de\/images\/Proving-code-properties_ADEB\/fscheck.png\"><img loading=\"lazy\" style=\"background-image: none; border-right-width: 0px; padding-left: 0px; padding-right: 0px; display: inline; border-top-width: 0px; border-bottom-width: 0px; border-left-width: 0px; padding-top: 0px\" title=\"fscheck\" border=\"0\" alt=\"fscheck\" src=\"http:\/\/www.navision-blog.de\/images\/Proving-code-properties_ADEB\/fscheck_thumb.png\" width=\"520\" height=\"455\" \/><\/a><\/p>\n<p>It&#8217;s even possible to add these tests to your test suite and to run them during the CI build. So don&#8217;t stop at classical unit test &#8211; check code properties!<\/p>\n","protected":false},"excerpt":{"rendered":"<p>As programmers we often want to express that a special property holds for a method, e.g. we want to say that the associativity law holds for list concatenation. In F# we could define a concat method like this: As programmers we could write a couple of unit tests which try to check the associativity law. [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[448,8],"tags":[664],"_links":{"self":[{"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/posts\/1240"}],"collection":[{"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/comments?post=1240"}],"version-history":[{"count":5,"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/posts\/1240\/revisions"}],"predecessor-version":[{"id":1245,"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/posts\/1240\/revisions\/1245"}],"wp:attachment":[{"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/media?parent=1240"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/categories?post=1240"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.navision-blog.de\/blog\/wp-json\/wp\/v2\/tags?post=1240"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}