For those who have never been in one of my spec# talks one of the largest benefits I like to tout about spec# is that it offers the possibility of removing runtime checks through the use of static verification.

 If I have proven that a condition could never possibly fail and that all of my code is covered by the prover why on earth would I need to emit runtime code other than to test that the prover was correct?


While not sounding like a huge benefit this would be one of the largest performance benefits of recent times as all validation code could feasibly be removed from runtime execution (pipelines are still small and branches can be expensive).

There is however one area which I have recently run into where this is not the case.

       static void RequiresValueOfFive(int val, string! str)
            requires val == 5;
       {
           Console.WriteLine(val.ToString() + " " + str);
       }

       static IEnumerable<string!>! YieldGetIEnumerable()
           ensures Foo == 5 ;
       {
           yield return "test";
           Foo = 5;
           yield return "test2";
       }

       static IEnumerable<string!>! GetIEnumerable()
       ensures Foo == 5 ;
       {
           List<string!> ret = new List<string!>();
           ret.Add("test");
           ret.Add("test2");
           Foo = 5;
           return ret;
       }
 
then …

       Foo = 0;
       IEnumerable<string!> somethingelse = YieldGetIEnumerable();
       foreach(string! s in somethingelse) {
         RequiresValueOfFive(Foo, s);
        }
In this example there is a significant difference between the way that iterators and a normal IEnumerable<T> work with post-conditions; iterators are a leaky abstraction. While it is not a big deal to change your code to handle these circumstances the spec# compiler does not know how to deal with them during proving.

At the outset this may not seem like too big of a deal but what happens when I decide to refactor from the first case to the second? All of my code will still compile, still run, but will fail with runtime assertions. Unless the compiler becomes smart enough to move the post-condition to the MoveNext (when it returns false) this nullifies the hope of removing runtime checks in a purely statically validated environment. Even with this change, I believe there are still runtime failures that can occur.

Given this information are iterators something that are THAT desirable? Iterators are syntactical sugar, I can duplicate what an iterator does rather simply in code that does not use an iterator … Are they worth me giving up the possibility of removing all of my runtime checks or introducing this complexity?

Note to self: check out how JML approaches this.