Sponsored By Aspose - File Format APIs for .NET

Aspose are the market leader of .NET APIs for file business formats – natively work with DOCX, XLSX, PPT, PDF, MSG, MPP, images formats and many more!

DbC and Iterators

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.
 

This entry was posted in contracts, dbc, spec#. Bookmark the permalink. Follow any comments here with the RSS feed for this post.

5 Responses to DbC and Iterators

  1. Greg says:

    Jeff:

    I would agree with this not being a reason to not use C# for game development

    per proving … spec#’s proving is truely amazing … If you havn’t checked it out yet I would. As an example though of how it might work … if I have a set of pre conditions I don’t actually need to prove the program’s flow. I only need to prove that in any location that it is called (in non-self modifying code) that its preconditions are met.

  2. Jeff Tucker says:

    @Rob runtime check removal does not strike me as a reason why c# is bad for commercial game development, I would argue that managed languages in general are not suitable for commercial games, but that I think needs a blog post for me to truly justify.

    @Greg
    I understand where you’re going with this, but how does this idea get around the halting problem? I see your iterators problem above as being a direct consequence of this and while technically it’s solvable given that a computer has a finite amount of memory and therefore a finite number of states, but it would still be practically impossible to actually create a prover that could check each one. It would also be impossible to write a prover that can prove itself (based on the proof of the halting problem as I understand it). How are you getting around this problem?

  3. Greg says:

    gtr this isn’t C# is is spec# code … ! after a type means that it can’t be null

  4. Rob says:

    I have to admit, the possibility of using a language on the .NET platform that could allow for the removal of runtime checks is very exciting. It is my understanding that this is one of the things that has caused C# to not perform well enough for commercial game development. If I can use spec# or some derivative to do this one day, that would rock my world.

  5. gtr36 says:

    What does ‘!’ after type name mean? I couldn’t compile it.

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>