Geeks With Blogs

News Disclaimer
The views expressed on this weblog are mine and do not necessarily reflect the views of my employer.

All postings are provided "AS IS" with no warranties, and confer no rights.

 Subscribe in a reader


I'm test-driven!
Locations of visitors to this page

Post Categories

Blog Moved to http://podwysocki.codebetter.com/ Blog Moved to http://podwysocki.codebetter.com/
Updates:
Part 4: Object Ownership/Assertions & Assumptions
Part 5: Frame Conditions/Inheritance/Boogie
Part 6: Implementing a non-null string collection
Part7: Spec# Wrapup

In my previous posts regarding Spec#, I have discussed some of the general concepts.  Let's review each one before we move onto today's topic, because each one builds upon another.

Part 1: Spec# introduction
Part 2: Method Contracts (Preconditions/Postconditions)

Now that we're caught up, let's move on.  Today's topic is going to look at Invariants.  On the first post, I mentioned that Design by Contract we have three parts. 

They are as follows:
  • What do we expect?
  • What do we guarantee?
  • What do we maintain?
Now that we covered the first two with preconditions and postconditions, it's time to move onto "What do we maintain?" and that's where invariants come into play. 

Invariants are somewhat similar to postconditions in that they ensure that your code is correct when it returns.  They are used in the context of a class and specify what conditions must hold throughout the classes lifetime.  They refer to class methods and private fields, but not part of the public interface.  We'll talk about two types of them, the class invariant and the loop inviariant.

The invariants are specified in Spec# by the invariant keyword.

Class Invariants

When using class invariants, Spec# adds a boolean field called inv to classes which tells the runtime whether the invariant currently holds.  If it does hold, then the object is said to be in a consistent state.  While the inv field is true, the fields within the object cannot be modified due to the possibility of breaking any of the invariants. 

If you need to update any of the invariant fields, Spec# makes you expose the object inside of an expose block.  At the beginning of the expose block, the inv field is set to false, and at the end it is checked.  If the invariant still holds, then the inv field is set to true again, else an exception is thrown and you were indeed a naughty programmer.  You cannot also add a return statement inside of an expose block, nor can you call any method that requires a consistent state.  The runtime system makes sure that the object is always in a consistent state and the invariants hold.

Let's look at a simple invariant class.  Let's start with a simple Date class:

public class Date
{
    int day;
    int month;
    int year;

    invariant day >= 1 && day <= 31;
    invariant month >= 1 && month <= 12;
    invariant year >= 1;
   
    public Date()
    {
        // Fields must be initialized in the constructor
        day = 14;
        month = 12;
        year = 2007;
    }
}

As you can note from the above class, I specified that the day cannot be less than 1 nor greater than 31, the month cannot be less than 1 nor greater than 12 and the year must be greater than 0.  We must initialize our fields inside of the constructor in order for this to be valid.  Now let's move onto another sample which includes the expose block.

public class Date
{
    int daysLeft;
    int daysPassed;

    invariant daysLeft + daysPassed == 365;
   
    public Date()
    {
        // Fields must be initialized in the constructor
        daysLeft = 16;
        daysPassed = 349;
    }

    public void AddOneDay()
    {
         expose(this)
         {
              daysLeft--;
              daysPassed++;
         }
    }
}

Since incrementing the daysPassed and decrementing the daysLeft would break the invariant, we had to expose it so that it can be checked.  At the end, the runtime checks to see that sure enough, we haven't broken the invariant. 

Loop Invariants

The second type of invariant I'll cover today is the loop invariant.  This invariant specifies conditions that must hold during the execution of a loop.  One important note is that these loop invariants are checked before the loop conditions are checked.  The loop condition itself cannot be an invariant due to the last iteration of the loop must return false and that would break an invariant.

Now let's walk through a code example of something using a loop invariant.  This code will take in an array of 32-bit integers and add them together and return the sum.  The code should look like this:

public static int SumAllNumbers(int[]! numArray)
    ensures result == sum{int i in (0: numArray.Length); numArray[i]};
{
    int sumValue = 0;
    for (int idx = 0; idx < numArray.Length; idx++)
      invariant idx <= numArray.Length;
      invariant sumValue == sum{int i in (0: idx); numArray[i]};
    {
        sumValue += numArray[idx];
    }
    return sumValue;
}

From the above code, we have a function called SumAllNumbers.  We must pass in a non-null array of 32-bit integers, and the postcondition states that the result must be the sum of all numbers.  We are using a built-in function call sum in the postcondition to ensure the numbers add up.  There are many of these built-in functions such as count, product, forall and so on.  There is a lot to learn and not much documentation to learn by, so that's why I'm bringing this material to you.  But, let's continue with the code.

As you will note, we specify a loop invariant for the idx to make sure we do not go outside the bounds of the incoming numArray. We also specify a loop invariant to specify that the sumValue will be the sum of all numbers by using the built-in sum function.

Wrapup

We learned quite a bit about invariants, and really, we only scratched the surface of what they can do and what they are used for.  Most of these concepts are taught in many CS courses, or at least should be.  We still have a lot to go!

Upcoming posts to include:
  • Object Ownership
  • Assertions
  • Spec# Attributes
  • Boogie static verifier
  • And much much more!
So, stay tuned.  Develop, mentor and inspire!

kick it on DotNetKicks.com Posted on Sunday, December 16, 2007 12:00 AM Microsoft , C# , Test Driven Development , Spec# | Back to top


Comments on this post: .NET 3.5, Design by contract and Spec# Part 3

# Problem with invariant in spec#/z3
Requesting Gravatar...
Hello,

I have a problem with invariant in spec#. My code is follow:

public static int somme(int n)
requires n >= 0;
ensures 2*result == n*(n+1);
{
int i = 0;
int s = 0;
while(i <= n)
invariant i <= n + 1 ;
invariant s*2 == (i-1)*i;
{
s = s + i;
i = i + 1;
}
return s;
}

I write this function to count numbers from 1 to n and the result = n*(n+1)/2.

But when I compile this by the command :
ssc /t:library /debug sum.ssc

and use sscboogie to verify this (sscboogie sum.dll /trace), it shows me this message :

Spec# program verifier version 2.00, Copyright (c) 2003-2008, Microsoft.

Running abstract interpretation...
[0,140625 s]

Verifying Sum.somme$System.Int32 ...
sum.ssc(14,13): Error: After loop iteration: Loop invariant might not hold: s*2 == (i-1)*i
sum.ssc(16,4): Related information: (trace position)
Error: Method Sum.somme(int n), unsatisfied postcondition: 2*result == n*(n+1)
sum.ssc(19,3): Related information: (trace position)
[0,46875 s] errors

Verifying Sum.SumAllNumbers$System.Int32.array$notnull ...
[0,03125 s] verified

Verifying Sum..ctor ...
[0,03125 s] verified

Spec# program verifier finished with 2 verified, 2 errors

I've tried my program by hand and this works well. I don't think that my code is incorrect. Could you explain this to me ?

Thanks a lot,
Le Vinh
Left by Le Vinh on Feb 16, 2010 9:31 AM

Your comment:
 (will show your gravatar)


Copyright © Matthew Podwysocki | Powered by: GeeksWithBlogs.net